Finish example of integers as a HIT

diff --git a/examples/integer.ctt b/examples/integer.ctt
index 58e8d99f5b0afa276a88e6a212ef9306fc07aeca..308525a0cb6f5a90a91e6a52c8665a432c11975c 100644 (file)
--- 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