added thierrys adapted files

diff --git a/examples/discor.ctt b/examples/discor.ctt
new file mode 100644 (file)
index 0000000..ecfc665
--- /dev/null
+++ b/examples/discor.ctt
@@ -0,0 +1,64 @@
+module discor where\r
+\r
+import prelude\r
+\r
+data or (A B:U) = inl (a:A) | inr (b:B)\r
+\r
+data Unit = tt\r
+\r
+data N0 = \r
+\r
+efq (A:U) : N0 -> A = split{}\r
+\r
+neg (A:U) : U = A -> N0\r
+\r
+dec (A:U) : U = or A (neg A)\r
+\r
+discrete (A:U) : U = (a b:A) -> dec (Id A a b)\r
+\r
+inlNotinr (A B:U) (a:A) (b:B) (h: Id (or A B) (inl a) (inr b)) : N0 = \r
+ subst (or A B) T (inl a) (inr b) h tt\r
+ where\r
+  T : or A B -> U = split\r
+       inl _ -> Unit\r
+       inr _ -> N0\r
+\r
+inrNotinl (A B:U) (a:A) (b:B) (h : Id (or A B) (inr b) (inl a)) : N0 = \r
+ subst (or A B) T (inr b) (inl a) h tt\r
+ where\r
+  T : or A B -> U = split\r
+       inl _ -> N0\r
+       inr _ -> Unit\r
+\r
+injective (A B:U) (f:A->B) : U = (a0 a1:A) -> Id B (f a0) (f a1) -> Id A a0 a1\r
+\r
+injInl (A B :U) (x0 x1:A) (h : Id (or A B) (inl x0) (inl x1)) : Id A x0 x1 = \r
+ subst (or A B) T (inl x0) (inl x1) h (refl A x0)\r
+ where\r
+   T : or A B -> U = split\r
+         inl x -> Id A x0 x\r
+         inr _ -> N0\r
+\r
+injInr (A B :U) (x0 x1:B) (h: Id (or A B) (inr x0) (inr x1)) : Id B x0 x1 = \r
+ subst (or A B) T (inr x0) (inr x1) h (refl B x0)\r
+ where\r
+   T : or A B -> U = split\r
+         inl _ -> N0\r
+         inr x -> Id B x0 x\r
+\r
+orDisc (A B : U) (dA: discrete A) (dB: discrete B) : (z z1 : or A B) -> dec (Id (or A B) z z1) = split\r
+  inl a -> rem1\r
+    where rem1 : (z1:or A B) -> dec (Id (or A B) (inl a) z1) = split\r
+            inl a1 -> rem (dA a a1)\r
+               where rem : dec (Id A a a1) -> dec (Id (or A B) (inl a) (inl a1)) = split\r
+                            inl p -> inl (<i> inl (p @ i))\r
+                            inr h -> inr (\ (p:Id (or A B) (inl a) (inl a1)) -> h (injInl A B a a1 p))\r
+            inr b -> inr (inlNotinr A B a b)\r
+  inr b -> rem1\r
+   where rem1 : (z1:or A B) -> dec (Id (or A B) (inr b) z1) = split\r
+            inl a -> inr (inrNotinl A B a b)\r
+            inr b1 -> rem (dB b b1)\r
+               where rem : dec (Id B b b1) -> dec (Id (or A B) (inr b) (inr b1)) = split\r
+                            inl p -> inl (<i> inr (p @ i))\r
+                            inr h -> inr (\ (p:Id (or A B) (inr b) (inr b1)) -> h (injInr A B b b1 p))\r
+\r

diff --git a/examples/hedberg.ctt b/examples/hedberg.ctt
new file mode 100644 (file)
index 0000000..a9443f3
--- /dev/null
+++ b/examples/hedberg.ctt
@@ -0,0 +1,88 @@
+module hedberg where\r
+\r
+import bool\r
+import discor\r
+import int\r
+\r
+const (A : U) (f : A -> A) : U = (x y : A) -> Id A (f x) (f y)\r
+\r
+decEqCong (A B : U) (f : A -> B) (g : B -> A) : dec A -> dec B = split\r
+  inl a -> inl (f a)\r
+  inr h -> inr (\ (b:B) -> h (g b))\r
+\r
+pred : nat -> nat = split\r
+  zero  -> zero\r
+  suc n -> n\r
+\r
+sucInj (n m : nat) (p:Id nat (suc n) (suc m)) : Id nat n m = \r
+ <i> pred (p @ i)\r
+\r
+caseNat (A:U) (a0 aS : A) : nat -> A = split\r
+ zero -> a0\r
+ suc n -> aS\r
+\r
+caseDNat (P:nat -> U) (a0 :P zero) (aS : (n:nat) -> P (suc n)) \r
+            : (n:nat) -> P n = split\r
+ zero -> a0\r
+ suc n -> aS n\r
+\r
+znots (n : nat) : neg (Id nat zero (suc n)) =\r
+ \ (h:Id nat zero (suc n)) -> subst nat (caseNat U nat N0) zero (suc n) h zero\r
+\r
+snotz (n : nat) : neg (Id nat (suc n) zero) =\r
+ \ (h:Id nat (suc n) zero) -> znots n (inv nat (suc n) zero h)\r
+\r
+natDec : (n m:nat) -> dec (Id nat n m) = split\r
+ zero -> caseDNat (\ (m:nat) -> dec (Id nat zero m)) (inl (refl nat zero)) (\ (m:nat) -> inr (znots m))\r
+ suc n -> caseDNat (\ (m:nat) -> dec (Id nat (suc n) m)) (inr (snotz n))\r
+   (\ (m:nat) -> decEqCong (Id nat n m) (Id nat (suc n) (suc m)) (\ (p:Id nat n m) -> <i> suc (p @ i))\r
+                 (sucInj n m) (natDec n m))\r
+\r
+prop (A:U) : U = (a b:A) -> Id A a b\r
+\r
+set (A:U) : U = (a b:A) -> prop (Id A a b)\r
+\r
+exConst (A : U) :U = (f:A -> A) * const A f\r
+\r
+decConst (A : U) : dec A -> exConst A = split\r
+  inl a -> (\ (x:A)  -> a, \ (x y:A) -> refl A a)\r
+  inr h -> (\ (x:A) -> x, \ (x y:A) -> efq (Id A x y) (h x))\r
+\r
+hedbergLemma (A: U) (f : (a b : A) -> Id A a b -> Id A a b) (a :A) : \r
+  (b : A) (p : Id A a b) ->\r
+            Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p) = \r
+  J A a (\ (b:A) (p:Id A a b) -> Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p)) \r
+    (refl (Id A a a) (f a a (refl A a)))\r
+\r
+compUp (A : U) (a a' b b' : A) \r
+       (p : Id A a a') (q: Id A b b') (r:Id A a b) : Id A a' b' =\r
+ <i> comp A (r@i) [(i=0) -> p, (i=1) -> q]\r
+\r
+compDown (A : U) (a a' b b' : A) \r
+         (p : Id A a a') (q: Id A b b') : Id A a' b' -> Id A a b =\r
+ compUp A a' a b' b (inv A a a' p) (inv A b b' q)\r
+\r
+hedberg (A : U) (h:discrete A) (a b :A) (p q:Id A a b) : Id (Id A a b) p q = \r
+   lemSimpl A a a b r p q rem5\r
+  where\r
+    rem1 (x y : A) : exConst (Id A x y) = decConst (Id A x y) (h x y)\r
+\r
+    f (x y : A) : Id A x y -> Id A x y = (rem1 x y).1\r
+\r
+    fIsConst (x y : A) : const (Id A x y) (f x y) = (rem1 x y).2\r
+\r
+    r : Id A a a = f a a (refl A a)\r
+\r
+    rem2 : Id (Id A a b) (compId A a a b r p) (f a b p) = hedbergLemma A f a b p\r
+\r
+    rem3 : Id (Id A a b) (compId A a a b r q) (f a b q) = hedbergLemma A f a b q\r
+\r
+    rem4 : Id (Id A a b) (f a b p) (f a b q) = fIsConst a b p q\r
+\r
+    rem5 : Id (Id A a b) (compId A a a b r p) (compId A a a b r q) = \r
+     compDown (Id A a b) (compId A a a b r p) (f a b p) (compId A a a b r q)\r
+                (f a b q) rem2 rem3 rem4\r
+\r
+natSet : set nat = hedberg nat natDec\r
+\r
+ZSet : set Z = hedberg Z (orDisc nat nat natDec natDec)
\ No newline at end of file

diff --git a/examples/int.ctt b/examples/int.ctt
new file mode 100644 (file)
index 0000000..3ff9691
--- /dev/null
+++ b/examples/int.ctt
@@ -0,0 +1,42 @@
+module int where\r
+\r
+import nat\r
+import discor\r
+\r
+Z : U = or nat nat\r
+\r
+zeroZ : Z =  inr zero\r
+\r
+sucZ : Z -> Z = split\r
+  inl u -> auxsucZ u\r
+    where\r
+    auxsucZ : nat -> Z = split\r
+      zero  -> inr zero\r
+      suc n -> inl n\r
+  inr v -> inr (suc v)\r
+\r
+predZ : Z -> Z = split\r
+  inl u -> inl (suc u)\r
+  inr v -> auxpredZ v\r
+    where\r
+    auxpredZ : nat -> Z = split\r
+      zero  -> inl zero\r
+      suc n -> inr n\r
+\r
+sucpredZ : (x : Z) -> Id Z (sucZ (predZ x)) x = split\r
+  inl u -> refl Z (inl u)\r
+  inr v -> lem v\r
+   where\r
+    lem : (u : nat) -> Id Z (sucZ (predZ (inr u))) (inr u) = split\r
+      zero  -> refl Z (inr zero)\r
+      suc n -> refl Z (inr (suc n))\r
+\r
+predsucZ : (x : Z) -> Id Z (predZ (sucZ x)) x = split\r
+  inl u -> lem u\r
+   where\r
+    lem : (u : nat) -> Id Z (predZ (sucZ (inl u))) (inl u) = split\r
+      zero  -> refl Z (inl zero)\r
+      suc n -> refl Z (inl (suc n))\r
+  inr v -> refl Z (inr v)\r
+\r
+sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ\r

diff --git a/examples/retract.ctt b/examples/retract.ctt
new file mode 100644 (file)
index 0000000..66a0bb8
--- /dev/null
+++ b/examples/retract.ctt
@@ -0,0 +1,36 @@
+module retract where\r
+\r
+import prelude\r
+import hedberg\r
+\r
+\r
+section (A B : U) (f : A -> B) (g : B -> A) :U = (b : B) -> Id B (f (g b)) b\r
+\r
+retract (A B : U) (f : A -> B) (g : B -> A) : U = section B A g f\r
+\r
+lemRetract (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g) (x y:A) :\r
+             Id A (g (f x)) (g (f y)) -> Id A x y\r
+  = compUp A (g (f x)) x (g (f y)) y (rfg x) (rfg y)\r
+\r
+retractProp (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g) (pB :prop B) (x y:A) \r
+  : Id A x y = lemRetract A B f g rfg x y (<i> g (pB (f x) (f y)) @ i)\r
+\r
+retractInv (A B : U)  (f : A -> B) (g : B -> A) (rfg : retract A B f g)\r
+           (x y : A) (q: Id B (f x) (f y)) : Id A x y = \r
+  compUp A (g (f x)) x (g (f y)) y (rfg x) (rfg y) (<i> (g (q @ i)))\r
+\r
+lemRSquare (A B : U)  (f : A -> B) (g : B -> A) (rfg: retract A B f g)(x y:A) (p : Id A x y) :\r
+  Square A (g (f x)) (g (f y)) (<i> g (f (p @ i))) x y\r
+    (retractInv A B f g rfg x y (<i> f (p@ i))) (rfg x) (rfg y) =\r
+  <j i> comp A (g (f (p @ j))) [(j=0) -> <l> (rfg x) @ (i/\l), (j=1) -> <l> (rfg y) @ (i/\l)]\r
+\r
+retractId (A B : U)(f : A -> B) (g : B -> A) (rfg : retract A B f g) (x y :A) (p:Id A x y) :\r
+      Id (Id A x y) (retractInv A B f g rfg x y (<i> f (p@ i))) p =\r
+  <i j> comp A (g (f (p @ j))) [(j=0) -> rfg x,(j=1) -> rfg y,\r
+             (i=0) -> (lemRSquare A B f g rfg x y p) @ j,(i=1) -> rfg (p @ j)]\r
+\r
+retractSet (A B : U) (f : A -> B) (g : B -> A) (rfg : retract A B f g)\r
+           (sB : set B) (x y : A) : prop (Id A x y) =\r
+  retractProp (Id A x y) (Id B (f x) (f y)) (mapOnPath A B f x y)\r
+    (retractInv A B f g rfg x y) (retractId A B f g rfg x y) (sB (f x) (f y))\r
+\r

diff --git a/examples/susp.ctt b/examples/susp.ctt
new file mode 100644 (file)
index 0000000..905cbc9
--- /dev/null
+++ b/examples/susp.ctt
@@ -0,0 +1,114 @@
+module susp where\r
+\r
+-- import helix\r
+import circle\r
+\r
+data susp (A:U) = north | south | merid (a:A) @ north ~ south\r
+\r
+-- n-spheres\r
+sphere : nat -> U = split\r
+  zero  -> bool\r
+  suc n -> susp (sphere n)\r
+\r
+-- The circle (S1) is equal to the 1-sphere (aka the suspension of Bool).\r
+-- (Similar to HoTT Book, Lemma 6.5.1)\r
+one : nat = suc zero\r
+\r
+sone : U = sphere one\r
+\r
+s1ToCircle : sone -> S1 = split\r
+  north   -> base\r
+  south   -> base\r
+  merid b @ i -> (path b) @ i\r
+    where path : bool ->Id S1 base base = split\r
+            false -> loop'\r
+            true  -> refl S1 base\r
+\r
+m0 : Id sone north south = <i> (merid{sone} false) @ i\r
+\r
+m1 : Id sone north south = <i> (merid{sone} true) @ i\r
+\r
+invm1 : Id sone south north = inv sone north south m1\r
+\r
+circleToS1 : S1 -> sone = split\r
+  base -> north\r
+  loop @ i -> (compId sone north south north m0 invm1) @ i\r
+\r
+merid1 (b:bool) : Id sone north south = <i>(merid{sone} b)@ i\r
+\r
+oc (x:S1) : S1 = s1ToCircle (circleToS1 x)\r
+\r
+ocid : (x : S1) -> Id S1 (oc x) x = split\r
+    base -> refl S1 base\r
+    loop @ i -> <j> oc (loop' @ i)\r
+\r
+co (x: sone) : sone = circleToS1 (s1ToCircle x)\r
+\r
+lemSquare (A:U) (a b : A) (m0 m1 : Id A a b) : \r
+  Square A a a (compId A a b a m0 (inv A a b m1)) a b m0 (refl A a) m1 = \r
+ <j i> comp A (m0 @ j) [(j=1) -> <k> m1 @ (i \/ -k)\r
+                       ,(i=0) -> <k> comp A (m0 @ j) [(j=1) -> <l> m1 @ (-k \/ -l)]]\r
+\r
+coid : (x : sone) -> Id sone (co x) x = split\r
+ north -> refl sone north\r
+ south -> m1\r
+ merid b @ i  -> (ind b) @ i\r
+  where\r
+    F (x:sone) : U = Id sone (co x) x\r
+\r
+    ind : (b:bool) -> IdS sone F north south (merid1 b) (refl sone north) m1 = split\r
+      false -> lemSquare sone north south m0 m1\r
+      true -> <j k> m1 @ (j /\ k)\r
+\r
+s1EqCircle : Id U sone S1 = isoId sone S1 s1ToCircle circleToS1 ocid coid\r
+\r
+s1EqS1 : Id U S1 S1 = compId U S1 sone S1 (inv U sone S1 s1EqCircle) s1EqCircle \r
+\r
+-- pointed sets\r
+\r
+ptU : U = (X : U) * X\r
+\r
+lemPt1 (A :U) : (B:U) (p:Id U A B) (a:A) -> Id ptU (A,a) (B,transport p a)\r
+ = J U A (\ (B:U) (p:Id U A B) -> (a:A) -> Id ptU (A,a) (B,transport p a))\r
+   (\ (a:A) -> refl ptU (A,a))\r
+\r
+s1PtCircle1 : Id ptU (sone,north) (S1,base) = lemPt1 sone S1 s1EqCircle north\r
+\r
+lemPt (A :U) (B:U) (p:Id U A B) (a:A) : Id ptU (A,a) (B,transport p a) =\r
+ <i> (p @ i,transport (<j>p @ (i/\j)) a)\r
+\r
+Omega (X:ptU) : ptU = (Id X.1 X.2 X.2,refl X.1 X.2)\r
+\r
+s1PtCircle : Id ptU (sone,north) (S1,base) = lemPt sone S1 s1EqCircle north\r
+\r
+s1PtS1 : Id ptU (S1,base) (S1,base) = lemPt S1 S1 s1EqS1 base\r
+\r
+windingS : Id sone north north -> Z = rem1\r
+ where\r
+  G (X:ptU) : U = (Omega X).1 -> Z\r
+  rem : G (S1,base) = winding\r
+  rem1 : G (sone,north) = subst ptU G (S1,base) (sone,north) (<i> s1PtCircle @ -i) rem\r
+\r
+windingT : loopS1 -> Z = rem1\r
+ where\r
+  G (X: ptU): U = (Omega X).1 -> Z\r
+  rem : G (S1,base) = winding\r
+  rem1 : G (S1,base) = subst ptU G (S1,base) (S1,base) s1PtS1 rem\r
+\r
+s1ToCId (p: Id sone north north) : Id S1 base base\r
+ = <i> transport s1EqCircle (p @ i) \r
+\r
+s1ToCIdInv (p : Id S1 base base) : Id sone north north\r
+ = <i> (transport (<j> s1EqCircle @(-j)) (p @ i))\r
+\r
+loop1S :  Id sone north north = s1ToCIdInv loop'\r
+\r
+loop2S : Id sone north north = compId sone north north north loop1S loop1S\r
+\r
+test0S : Z = windingS (refl sone north)\r
+\r
+test2S : Z = windingS loop2S\r
+\r
+winding' (l : Id sone north north) : Z = winding (s1ToCId l)\r
+\r
+testS : Id sone north north = <i> comp sone (m0 @ i) [ (i=1) -> <k> m1 @ (-k)]\r