From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Fri, 11 Dec 2015 21:39:35 +0000 (-0500)
Subject: start working on hz
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=0b9c712d49e2077287b2cef9f15f781baed73bee;p=cubicaltt.git

start working on hz
---

diff --git a/examples/hz.ctt b/examples/hz.ctt
new file mode 100644
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 c4b4974..49f9149 100644
--- 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')