start working on hz

diff --git a/examples/hz.ctt b/examples/hz.ctt
new file mode 100644 (file)
index 0000000..2805204
--- /dev/null
+++ b/examples/hz.ctt
@@ -0,0 +1,23 @@
+module hz where
+
+import nat
+import setquot
+
+-- shorthand for nat x nat
+nat2 : U = and nat nat
+
+rel : eqrel nat2 = (r,rem)
+  where
+  r : hrel nat2) = \(x y : nat2) -> 
+    (Id nat (add x.1 y.2) (add x.2 y.1),natSet (add x.1 y.2) (add x.2 y.1))
+    
+  rem : iseqrel nat2 r = ((rem1,refl nat2),rem2)
+   where
+   rem1 : istrans nat2 r = undefined
+   rem2 : issymm nat2 r = undefined
+
+hz : U = setquot nat2 rel
+zeroz : hz = setquotpr nat2 rel (zero,zero)
+onez : hz = setquotpr nat2 rel (one,zero)
+
+test : neg (Id hz zeroz onez) = undefined
\ No newline at end of file

diff --git a/examples/setquot.ctt b/examples/setquot.ctt
index c4b4974523198db2ea5a3b72347405f9e62c5a7e..49f9149118933f2a5946c05cfb18433711a49870 100644 (file)
--- a/examples/setquot.ctt
+++ b/examples/setquot.ctt
@@ -202,7 +202,7 @@ test : (P' true').1 = hdisj_in1 (Id bool' true' true')
                                 (Id bool' true' false') (<_> true')
 test' : (P' true').1 = K' true'
 
-test'' : Id (P' true').1 test test' = (P' true').2 test test'
+-- test'' : Id (P' true').1 test test' = (P' true').2 test test'
 
 -- These two terms are not convertible:
 -- test' : Id (P' true').1 (K' true')