Start defining integers as a HIT and proving that they are a set

diff --git a/examples/int.ctt b/examples/int.ctt
index 3d12f3239f8f0ce327b9430781777c580ac3b5ab..dc4ccc0e5114a9a1e0110c6e2c834342c99dc61f 100644 (file)
--- a/examples/int.ctt
+++ b/examples/int.ctt
@@ -3,9 +3,10 @@ module int where
 import nat\r
 import discor\r
 \r
+-- inl = neg, inr = pos\r
 Z : U = or nat nat\r
 \r
-zeroZ : Z =  inr zero\r
+zeroZ : Z = inr zero\r
 \r
 sucZ : Z -> Z = split\r
   inl u -> auxsucZ u\r

diff --git a/examples/integer.ctt b/examples/integer.ctt
index e8b6ba9e10f80ae817362f243131f7659ffec1ed..da9b4b31277f27d96423e3219b5ca00c647dabe0 100644 (file)
--- a/examples/integer.ctt
+++ b/examples/integer.ctt
@@ -1,42 +1,67 @@
 module integer where
 
-import nat
-
-data Z = zeroZ | posZ (n : nat) | negZ (n : nat)
-
-caseNat (A : U) (a : A) (f : nat -> A) : nat -> A = split
-  zero -> a
-  suc n -> f n
-
-sucZ : Z -> Z = split
-  zeroZ -> posZ zero
-  posZ n -> posZ (suc n)
-  negZ n -> caseNat Z zeroZ (\(x : nat) -> negZ x) n
-
-predZ : Z -> Z = split
-  zeroZ -> negZ zero
-  posZ n -> caseNat Z zeroZ (\(x : nat) -> posZ x) n
-  negZ n -> negZ (suc n)
-
-sucpredZ : (n : Z) -> Id Z (sucZ (predZ n)) n = split
-  zeroZ  -> refl Z zeroZ
-  posZ n -> lem n
-   where
-    lem : (n : nat) -> Id Z (sucZ (predZ (posZ n))) (posZ n) = split
-      zero  -> refl Z (posZ zero)
-      suc n -> refl Z (posZ (suc n))
-  negZ n -> refl Z (negZ n)
-
-predsucZ : (n : Z) -> Id Z (predZ (sucZ n)) n = split
-  zeroZ -> refl Z zeroZ
-  posZ n -> refl Z (posZ n)
-  negZ n -> lem n
-   where
-    lem : (n : nat) -> Id Z (predZ (sucZ (negZ n))) (negZ n) = split
-      zero  -> refl Z (negZ zero)
-      suc n -> refl Z (negZ (suc n))
-
-sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ
-
-sucIdZ2 : Id U Z Z = compId U Z Z Z sucIdZ sucIdZ
-test : Z = predZ (transport sucIdZ2 zeroZ)
\ No newline at end of file
+import int
+
+data int = pos (n : nat)
+         | neg (n : nat)
+         | zeroP @ pos zero ~ neg zero
+
+zeroP' : Id int (pos zero) (neg zero) = <i> zeroP {int} @ i
+
+sucInt : int -> int = split
+  pos n -> pos (suc n)
+  neg n -> sucNat n
+    where sucNat : nat -> int = split
+            zero -> pos one
+            suc n -> neg n
+  zeroP @ i -> pos one
+
+predInt : int -> int = split
+  pos n -> predNat n
+    where predNat : nat -> int = split
+           zero -> neg one
+           suc n -> pos n
+  neg n -> neg (suc n)
+  zeroP @ i -> neg one
+
+toZ : int -> Z = split
+  pos n -> inr n
+  neg n -> fun n
+    where fun : nat -> Z = split
+      zero -> zeroZ
+      suc n -> inl n
+  zeroP @ i -> zeroZ
+
+fromZ : Z -> int = split
+  inl n -> neg (suc n)
+  inr n -> pos n
+
+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 -> temp
+    where temp : Id int (pos zero) (zeroP{int} @ i) = undefined
+
+isoIntZ : Id U Z int = isoId Z int fromZ toZ fromZK toZK
+
+intSet : set int = subst U set Z int isoIntZ ZSet