added thierrys examples (funext from univalence,helix)

diff --git a/examples/funext.ctt b/examples/funext.ctt
new file mode 100644 (file)
index 0000000..f2ed6f1
--- /dev/null
+++ b/examples/funext.ctt
@@ -0,0 +1,97 @@
+module funext where\r
+\r
+import prelude\r
+\r
+homotopies (A B :U) : U =\r
+ (fg : (_:A->B) * (A->B)) * (x:A) -> Id B (fg.1 x) (fg.2 x)\r
+\r
+Paths (A:U) : U = (x y:A) * Id A x y\r
+\r
+lemPaths (A:U) : Id U (Paths A) A = isoId (Paths A) A f g  rems remt\r
+ where\r
+  f (z: Paths A) :  A = z.1\r
+  g (x:A) : Paths A   = (x,(x,refl A x))\r
+  rems (y:A) : Id A (f (g y)) y = refl A y\r
+  rem1t (x y:A) (p:Id A x y) : Id (Paths A) (x,(x,refl A x)) (x,(y,p)) =\r
+     <i> (x,(p@ i, <j>p@ (i/\j)))\r
+  remt (z:Paths A) : Id (Paths A) (g (f z)) z = rem1t z.1 z.2.1 z.2.2\r
+\r
+lem1 (A B :U) : Id U (A -> Paths B) (homotopies A B) = isoId T0 T1 f g t s\r
+ where T0 : U = A -> Paths B\r
+       T1 : U = homotopies A B\r
+       f (h:T0) : T1 = ((\ (x:A) -> (h x).1,\ (x:A) -> (h x).2.1),\ (x:A) -> (h x).2.2)\r
+       g (h : T1) : T0 = \ (x:A) ->  (h.1.1 x,(h.1.2 x,h.2 x))\r
+       s (h:T0) : Id T0 (g (f h)) h = refl T0 h\r
+       t (h : T1) : Id T1 (f (g h)) h = refl T1 h\r
+\r
+lem2 (A B : U)  : Id U (A->B) (homotopies A B) =\r
+  compId U (A->B) (A-> Paths B) (homotopies A B) rem (lem1 A B)\r
+ where \r
+   rem1 : Id U B (Paths B) = inv U (Paths B) B (lemPaths B)\r
+   rem : Id U (A->B) (A-> Paths B) = <i> A -> rem1 @ i\r
+\r
+thm (A B:U) : Id U (Paths (A->B)) (homotopies A B) =\r
+ compId U (Paths (A->B)) (A->B) (homotopies A B) (lemPaths (A->B)) (lem2 A B)\r
+\r
+test (A B:U) (f:A->B) : Id (A->B) (transport (thm A B) (f,(f,refl (A->B) f))).1.2 f = \r
+ refl (A->B) f\r
+\r
+funDepTr (A0 A1 :U) (p:Id U A0 A1) (u0:A0) (u1:A1) :\r
+             Id U (IdP p u0 u1) (Id A1 (transport p u0) u1) =\r
+ <i> IdP (<l> p @ (i\/l)) (transport (<l> p @ (i/\l)) u0) u1\r
+\r
+lem3 (A B:U) (f:A->B) (h:homotopies A B) : Id U (IdP (thm A B) (f,(f,refl (A->B) f)) h)\r
+                       (Id (homotopies A B) (transport (thm A B) (f,(f,refl (A->B) f))) h)\r
+              = funDepTr A0 A1 p u0 u1\r
+         where A0 : U = Paths (A -> B)\r
+               A1 : U = homotopies A B\r
+               p : Id U A0 A1 = thm A B\r
+               u0 : A0 = (f,(f,refl (A->B) f)) \r
+               u1 : A1 = h\r
+\r
+lem4 (A B:U) (f g : A -> B) (p:Id (A->B) f g) (h:homotopies A B) (h1: IdP (thm A B) (f,(g,p)) h)\r
+     : Id (A->B) f h.1.1 =\r
+ rem h (transport (<i>IdP (thm A B) (f,(p@-i,<j>p@(-i/\j))) h) h1)\r
+  where \r
+    rem1 (h:homotopies A B) (h1: IdP (thm A B) (f,(f,refl (A->B) f)) h) :\r
+              Id (homotopies A B) (transport (thm A B) (f,(f,refl (A->B) f))) h = transport (lem3 A B f h) h1\r
+    rem (h:homotopies A B) (h1: IdP (thm A B) (f,(f,refl (A->B) f)) h) :\r
+            Id (A->B) f h.1.1 = <i> ((rem1 h h1) @ i).1.1\r
+\r
+lem5 (A B:U) (f g: A -> B) (p:Id (A->B) f g) (h:homotopies A B) (h1: IdP (thm A B) (f,(g,p)) h)\r
+     : Id (A->B) g h.1.2 =\r
+ rem h (transport (<i>IdP (thm A B) (p@i,(g,<j>p@(i\/j))) h) h1)\r
+  where \r
+    rem1 (h:homotopies A B) (h1: IdP (thm A B) (g,(g,refl (A->B) g)) h) :\r
+              Id (homotopies A B) (transport (thm A B) (g,(g,refl (A->B) g))) h = transport (lem3 A B g h) h1\r
+\r
+    rem (h:homotopies A B) (h1: IdP (thm A B) (g,(g,refl (A->B) g)) h) :\r
+            Id (A->B) g h.1.2 = <i> ((rem1 h h1) @ i).1.2\r
+\r
+funDepTrInv (A0 A1 :U) (p:Id U A0 A1) (u1:A1) :\r
+             IdP p (transport (<i>p@-i) u1) u1 = <i> transport (<l> p @ (i\/-l)) u1\r
+\r
+homToP (A B:U) (h: homotopies A B) : Paths (A->B) = transport (<i>(thm A B)@-i) h\r
+\r
+lem6 (A B:U) : (h:homotopies A B) -> IdP (thm A B) (homToP A B h) h = \r
+ funDepTrInv (Paths (A->B)) (homotopies A B) (thm A B)\r
+\r
+lem7 (A B:U) (h:homotopies A B) : Id (A->B) (homToP A B h).1 h.1.1 =\r
+ lem4 A B p.1 p.2.1 p.2.2 h (lem6 A B h) \r
+  where p : Paths (A->B) = homToP A B h\r
+\r
+lem8 (A B:U) (h:homotopies A B) : Id (A->B) (homToP A B h).2.1 h.1.2 =\r
+ lem5 A B p.1 p.2.1 p.2.2 h (lem6 A B h) \r
+  where p : Paths (A->B) = homToP A B h\r
+\r
+funext (A B:U) (f g :A -> B) (pe : (x:A) -> Id B (f x) (g x)) :   Id (A->B) f g =\r
+   <i> \ (x:A) -> ((transport rem4 rem3) @ i) x\r
+  where\r
+    h : homotopies A B = ((f,g),pe)\r
+    p : Paths (A->B)   = homToP A B h\r
+    rem1 : Id (A->B) p.1 f   = lem7 A B h\r
+    rem2 : Id (A->B) p.2.1 g = lem8 A B h\r
+    rem3 : Id (A->B) p.1 p.2.1 = p.2.2\r
+    rem4 : Id U (Id (A->B) p.1 p.2.1) (Id (A->B) f g) = <i>Id (A->B) (rem1@i) (rem2@i)\r
+\r
+\r

diff --git a/examples/helix.ctt b/examples/helix.ctt
new file mode 100644 (file)
index 0000000..26988fb
--- /dev/null
+++ b/examples/helix.ctt
@@ -0,0 +1,202 @@
+module helix where\r
+\r
+import circle\r
+import hedberg\r
+import retract\r
+\r
+loop1 : loopS1 = loop'\r
+triv : loopS1 = <i>base\r
+\r
+compS1 : loopS1 -> loopS1 -> loopS1 = compId S1 base base base\r
+\r
+encode (x:S1) (p:Id S1 base x) : helix x = subst S1 helix base x p zeroZ\r
+\r
+itLoop : nat -> loopS1 = split\r
+ zero -> triv\r
+ suc n -> compS1 (itLoop n) loop1\r
+\r
+invLoop : loopS1 = inv S1 base base loop1\r
+\r
+itLoopNeg : nat -> loopS1 = split \r
+ zero -> invLoop\r
+ suc n -> compS1 (itLoopNeg n) invLoop\r
+\r
+loopIt : Z -> loopS1 = split\r
+ inl n -> itLoopNeg n\r
+ inr n -> itLoop n\r
+\r
+lemItNat (n:nat) : Id loopS1 (itLoop (suc n)) (transport (<i>Id S1 base (loop{S1} @ i)) (itLoop n)) = \r
+ refl loopS1 (itLoop (suc n))\r
+\r
+lemCompInv (A:U) (a b c:A) (p:Id A a b) (q:Id A b c) : Id (Id A a b) (compId A a c b (compId A a b c p q) (inv A b c q)) p =\r
+ <j i> comp A (comp A (p @ i) [(i=1) -> <k> q @ (-j /\ k)]) [(i=1) -> <k> q @ (-j /\ - k)]\r
+\r
+lemInv (A:U) (a b:A) (p:Id A a b) : Id (Id A b b) (compId A b a b (inv A a b p) p)  (refl A b) =\r
+  <j i> comp A (p @ (-i \/ j)) [(i=1) -> <k> p @ (j \/ k)]\r
+\r
+lemItNeg : (n:nat) -> Id loopS1  (transport (<i>Id S1 base (loop{S1} @ i)) (loopIt (inl n))) (loopIt (sucZ (inl n))) = split\r
+ zero ->  lemInv S1 base base loop1\r
+ suc n -> lemCompInv S1 base base base (itLoopNeg n) invLoop\r
+\r
+oneTurn (l: loopS1) : loopS1 = transport (<i>Id S1 base (loop{S1} @ i)) l\r
+\r
+lemItPos : (n:nat) -> Id loopS1 (oneTurn (loopIt (predZ (inr n)))) (loopIt (inr n)) = split\r
+ zero -> lemInv S1 base base loop1\r
+ suc n -> refl loopS1 (loopIt (inr (suc n)))\r
+\r
+lemItNeg (n:nat) : Id loopS1  (oneTurn (loopIt (predZ (inl n)))) (loopIt (inl n)) = \r
+ lemCompInv S1 base base base (loopIt (inl n)) invLoop\r
+\r
+lemIt : (n:Z) -> Id loopS1 (oneTurn (loopIt (predZ n)))  (loopIt n) = split\r
+ inl n -> lemItNeg n\r
+ inr n -> lemItPos n\r
+\r
+funDepTr (A0 A1:U) (p:Id U A0 A1) (u0:A0) (u1:A1) :\r
+             Id U (IdP p u0 u1) (Id A1 (transport p u0) u1) =\r
+ <i> IdP (<l>p @ (i\/l)) (transport (<l>p @ (i/\l)) u0) u1\r
+\r
+decode : (x:S1) -> helix x -> Id S1 base x = split\r
+ base -> loopIt\r
+ loop @ i -> rem @ i\r
+   where T : U = Z -> loopS1\r
+         p : Id U T T = <j> helix (loop{S1}@j) -> Id S1 base (loop{S1}@j)\r
+         rem1 : Id (Z -> loopS1) (transport p loopIt) loopIt =\r
+          funExt Z (\ (n:Z) -> loopS1) (transport (<j> helix (loop{S1}@j) -> Id S1 base (loop{S1}@j)) loopIt) loopIt lemIt\r
+         rem : IdP p loopIt loopIt = transport (<j> (funDepTr T T p loopIt loopIt)@-j) rem1\r
+\r
+lemPropF (A:U)(P:A->U)(pP:(x:A) -> prop (P x))(a0 a1:A)(p:Id A a0 a1)(b0:P a0)(b1:P a1): IdS A P a0 a1 p b0 b1 =\r
+ <i> (pP (p @ i) (transport (<j>P (p@i /\ j)) b0) (transport (<j>P (p@i \/ -j)) b1)) @ i\r
+\r
+lemPropFib (P:S1 -> U) (pP:(x:S1) -> prop (P x)) (bP: P base) : (x:S1) -> P x = split\r
+ base -> bP\r
+ loop @ i -> (lemPropF S1 P pP base base loop1 bP bP) @ i\r
+\r
+-- other proof?\r
+\r
+propIsProp (A:U) (f g:prop A) : Id (prop A) f g =\r
+ <i> \ (a b :A) -> (propSet A f a b (f a b) (g a b)) @ i\r
+\r
+setIsProp (A:U) (f g:set A) : Id (set A) f g =\r
+ <i> \ (a b :A) -> (propIsProp (Id A a b) (f a b) (g a b)) @ i\r
+\r
+helixSet : (x:S1) -> set (helix x) = lemPropFib (\ (x:S1) -> set (helix x)) rem ZSet\r
+ where rem (x:S1) : prop (set (helix x)) = setIsProp (helix x)\r
+\r
+retHelix (x:S1) (p : Id S1 base x) : Id (Id S1 base x) (decode x (encode x p)) p = \r
+ transport (<i>Id (Id S1 base p@i) (decode p@i (encode p@i (<j>p@(i/\j)))) (<j>p@(i/\j))) (refl loopS1 triv)\r
+\r
+setLoop : set loopS1 = retractSet loopS1 Z (encode base) (decode base) (retHelix base) ZSet\r
+\r
+-- S1 is a groupoid\r
+\r
+groupoid (A:U) : U = (x y:A) -> set (Id A x y)\r
+\r
+propPi (A : U) (B : A -> U) (h:(x : A) -> prop (B x)) (f0 f1:(x : A) -> B x) : Id ((x:A)-> B x) f0 f1 \r
+  = <i> \ (x:A) -> (h x (f0 x) (f1 x)) @ i\r
+\r
+isGroupoidS1 : groupoid S1 = lem\r
+ where\r
+  lem2 : (y : S1) -> set (Id S1 base y)\r
+    = lemPropFib (\ (y:S1) -> set (Id S1 base y)) (\ (y:S1) -> setIsProp (Id S1 base y)) setLoop\r
+\r
+  lem : (x y : S1) -> set (Id S1 x y)\r
+   = lemPropFib (\ (x:S1) -> (y : S1) -> set (Id S1 x y)) pP lem2\r
+     where \r
+       pP (x:S1) : prop ((y:S1) -> set (Id S1 x y)) =\r
+        propPi S1 (\ (y:S1) -> set (Id S1 x y)) (\ (y:S1) -> setIsProp (Id S1 x y))\r
+\r
+substInv (A : U) (P : A -> U) (a x : A) (p : Id A a x) : P x -> P a =\r
+ subst A P x a (<i>p @ -i)\r
+\r
+lemSetTorus (E : S1 -> S1 -> U) (sE : set (E base base))\r
+            (f : (y:S1) -> E base y) (g : (x:S1) -> E x base)\r
+            (efg : Id (E base base) (f base) (g base)) : (x y:S1) -> E x y = split\r
+ base -> f\r
+ loop @ i -> lem2 @ i\r
+   where\r
+    F (x:S1) : U = (y:S1) -> E x y\r
+\r
+    G (y x:S1) : U = E x y\r
+\r
+    lem1 : (y:S1) -> IdS S1 (G y) base base loop1 (f y) (f y) = lemPropFib P pP bP\r
+     where\r
+      P (y:S1) : U = IdS S1 (G y) base base loop1 (f y) (f y)\r
+\r
+      sbE : (y : S1) -> set (E base y)\r
+         = lemPropFib (\ (y:S1) -> set (E base y)) (\ (y:S1) -> setIsProp (E base y)) sE\r
+\r
+      pP (y:S1) : prop (P y) = rem3\r
+        where\r
+          rem1 : Id U (P y) (Id (E base y) (subst S1 (G y) base base loop1 (f y)) (f y))\r
+            = funDepTr (G y base) (G y base) (<j>G y loop{S1}@j) (f y) (f y)\r
+\r
+          rem2 : prop (Id (E base y) (subst S1 (G y) base base loop1 (f y)) (f y))\r
+            = sbE y (subst S1 (G y) base base loop1 (f y)) (f y)\r
+\r
+          rem3 : prop (P y)\r
+           = substInv U prop (P y) (Id (E base y) (subst S1 (G y) base base loop1 (f y)) (f y)) rem1 rem2\r
+          \r
+      lem2 : IdS S1 (G base) base base loop1 (g base) (g base)\r
+        = <j> g (loop1 @ j)\r
+\r
+      bP : P base\r
+        = substInv (E base base) (\ (u:E base base) -> IdS S1 (G base) base base loop1 u u) (f base) (g base) efg lem2\r
+\r
+    lem2 : IdS S1 F base base loop1 f f =  <j> \ (y:S1) -> (lem1 y) @ j\r
+\r
+-- commutativity of mult, at last\r
+\r
+idL : (x : S1) -> Id S1 (mult base x) x = split\r
+       base -> refl S1 base\r
+       loop @ i -> <j> loop1 @ i\r
+\r
+multCom : (x y : S1) -> Id S1 (mult x y) (mult y x) =\r
+ lemSetTorus E sE idL g efg\r
+  where\r
+    E (x y: S1) : U = Id S1 (mult x y) (mult y x)\r
+    sE : set (E base base) = isGroupoidS1 base base\r
+    g (x : S1) : E x base = inv S1 (mult base x) (mult x base) (idL x)\r
+    efg : Id (E base base) (idL base) (g base) = refl (E base base) (idL base)\r
+\r
+-- associativity\r
+\r
+multAssoc (x :S1) : (y z : S1) -> Id S1 (mult x (mult y z)) (mult (mult x y) z) = \r
+ lemSetTorus E sE f g efg\r
+ where\r
+   E (y z : S1) : U = Id S1 (mult x (mult y z)) (mult (mult x y) z)\r
+   sE : set (E base base) = isGroupoidS1 x x\r
+   f (z : S1) : E base z = rem\r
+     where \r
+        rem1 : Id S1 (mult base z) z = multCom base z\r
+\r
+        rem : Id S1 (mult x (mult base z)) (mult x z) = <i> mult x (rem1 @ i)\r
+   g (y : S1) : E y base = refl S1 (mult x y)\r
+   efg : Id (E base base) (f base) (g base) = refl (E base base) (f base)\r
+\r
+-- inverse law\r
+\r
+lemPropRel (P:S1 -> S1 -> U) (pP:(x y:S1) -> prop (P x y)) (bP:P base base) : (x y:S1) -> P x y = \r
+ lemPropFib (\ (x:S1) -> (y:S1) -> P x y)\r
+            (\ (x:S1) -> propPi S1 (P x) (pP x))\r
+            (lemPropFib (P base) (pP base) bP)                   \r
+\r
+invLaw : (x y : S1) ->\r
+          Id (Id S1 (mult x y) (mult x y)) (refl S1 (mult x y))\r
+             (compId S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x)) = lemPropRel P pP bP \r
+ where\r
+  P (x y : S1) : U\r
+    = Id (Id S1 (mult x y) (mult x y)) (refl S1 (mult x y))\r
+         (compId S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x))\r
+\r
+  pP (x y : S1) : prop (P x y) =\r
+   isGroupoidS1 (mult x y) (mult x y) (refl S1 (mult x y))\r
+                (compId S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x))\r
+\r
+  bP : P base base = refl (Id S1 base base) (refl S1 base)\r
+\r
+\r
+-- homotopy\r
+\r
+aLoop : loopS1 = <i>loop{S1}@(i/\-i)\r
+\r
+test : Id loopS1 triv aLoop = <j i>loop{S1}@(j/\i/\-i)\r