From: Anders <mortberg@chalmers.se>
Date: Wed, 15 Apr 2015 09:47:38 +0000 (+0200)
Subject: Finish example of integers as a HIT
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=87bac07cee90de290e9f3060d6e57939cbb363aa;p=cubicaltt.git

Finish example of integers as a HIT
---

diff --git a/examples/integer.ctt b/examples/integer.ctt
index 58e8d99..308525a 100644
--- a/examples/integer.ctt
+++ b/examples/integer.ctt
@@ -40,26 +40,13 @@ toZK : (a : Z) -> Id Z (toZ (fromZ a)) a = split
   inl n -> refl Z (inl n)
   inr n -> refl Z (inr n)
 
--- fromZ (toZ (neg zero)) = fromZ (fun zero)
---                        = fromZ zeroZ
---			  = fromZ (inr zero)
---			  = pos zero
-
--- fromZ (toZ (neg (suc n)) = fromZ (fun (suc n))
--- 	      	   	    = fromZ (inl n)
---			    = neg (suc n)
-
-sq : Square int (pos zero) (pos zero) (refl int (pos zero))
-                (pos zero) (neg zero) zeroP'
-		(refl int (pos zero)) zeroP' = undefined
-		
 fromZK : (a : int) -> Id int (fromZ (toZ a)) a = split
   pos n -> refl int (pos n)
   neg n -> rem n
     where rem : (n : nat) -> Id int (fromZ (toZ (neg n))) (neg n) = split
       zero -> zeroP'
       suc n -> refl int (neg (suc n))
-  zeroP @ i -> sq @ i
+  zeroP @ i -> <j> zeroP' @ i /\ j
 
 isoIntZ : Id U Z int = isoId Z int fromZ toZ fromZK toZK