From: Simon Huber Date: Sun, 12 Apr 2015 08:37:17 +0000 (+0200) Subject: added thierrys examples (funext from univalence,helix) X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=304e4e48b80bf99ba9006ad90a7934207f719408;p=cubicaltt.git added thierrys examples (funext from univalence,helix) --- diff --git a/examples/funext.ctt b/examples/funext.ctt new file mode 100644 index 0000000..f2ed6f1 --- /dev/null +++ b/examples/funext.ctt @@ -0,0 +1,97 @@ +module funext where + +import prelude + +homotopies (A B :U) : U = + (fg : (_:A->B) * (A->B)) * (x:A) -> Id B (fg.1 x) (fg.2 x) + +Paths (A:U) : U = (x y:A) * Id A x y + +lemPaths (A:U) : Id U (Paths A) A = isoId (Paths A) A f g rems remt + where + f (z: Paths A) : A = z.1 + g (x:A) : Paths A = (x,(x,refl A x)) + rems (y:A) : Id A (f (g y)) y = refl A y + rem1t (x y:A) (p:Id A x y) : Id (Paths A) (x,(x,refl A x)) (x,(y,p)) = + (x,(p@ i, p@ (i/\j))) + remt (z:Paths A) : Id (Paths A) (g (f z)) z = rem1t z.1 z.2.1 z.2.2 + +lem1 (A B :U) : Id U (A -> Paths B) (homotopies A B) = isoId T0 T1 f g t s + where T0 : U = A -> Paths B + T1 : U = homotopies A B + f (h:T0) : T1 = ((\ (x:A) -> (h x).1,\ (x:A) -> (h x).2.1),\ (x:A) -> (h x).2.2) + g (h : T1) : T0 = \ (x:A) -> (h.1.1 x,(h.1.2 x,h.2 x)) + s (h:T0) : Id T0 (g (f h)) h = refl T0 h + t (h : T1) : Id T1 (f (g h)) h = refl T1 h + +lem2 (A B : U) : Id U (A->B) (homotopies A B) = + compId U (A->B) (A-> Paths B) (homotopies A B) rem (lem1 A B) + where + rem1 : Id U B (Paths B) = inv U (Paths B) B (lemPaths B) + rem : Id U (A->B) (A-> Paths B) = A -> rem1 @ i + +thm (A B:U) : Id U (Paths (A->B)) (homotopies A B) = + compId U (Paths (A->B)) (A->B) (homotopies A B) (lemPaths (A->B)) (lem2 A B) + +test (A B:U) (f:A->B) : Id (A->B) (transport (thm A B) (f,(f,refl (A->B) f))).1.2 f = + refl (A->B) f + +funDepTr (A0 A1 :U) (p:Id U A0 A1) (u0:A0) (u1:A1) : + Id U (IdP p u0 u1) (Id A1 (transport p u0) u1) = + IdP ( p @ (i\/l)) (transport ( p @ (i/\l)) u0) u1 + +lem3 (A B:U) (f:A->B) (h:homotopies A B) : Id U (IdP (thm A B) (f,(f,refl (A->B) f)) h) + (Id (homotopies A B) (transport (thm A B) (f,(f,refl (A->B) f))) h) + = funDepTr A0 A1 p u0 u1 + where A0 : U = Paths (A -> B) + A1 : U = homotopies A B + p : Id U A0 A1 = thm A B + u0 : A0 = (f,(f,refl (A->B) f)) + u1 : A1 = h + +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) + : Id (A->B) f h.1.1 = + rem h (transport (IdP (thm A B) (f,(p@-i,p@(-i/\j))) h) h1) + where + rem1 (h:homotopies A B) (h1: IdP (thm A B) (f,(f,refl (A->B) f)) h) : + Id (homotopies A B) (transport (thm A B) (f,(f,refl (A->B) f))) h = transport (lem3 A B f h) h1 + rem (h:homotopies A B) (h1: IdP (thm A B) (f,(f,refl (A->B) f)) h) : + Id (A->B) f h.1.1 = ((rem1 h h1) @ i).1.1 + +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) + : Id (A->B) g h.1.2 = + rem h (transport (IdP (thm A B) (p@i,(g,p@(i\/j))) h) h1) + where + rem1 (h:homotopies A B) (h1: IdP (thm A B) (g,(g,refl (A->B) g)) h) : + Id (homotopies A B) (transport (thm A B) (g,(g,refl (A->B) g))) h = transport (lem3 A B g h) h1 + + rem (h:homotopies A B) (h1: IdP (thm A B) (g,(g,refl (A->B) g)) h) : + Id (A->B) g h.1.2 = ((rem1 h h1) @ i).1.2 + +funDepTrInv (A0 A1 :U) (p:Id U A0 A1) (u1:A1) : + IdP p (transport (p@-i) u1) u1 = transport ( p @ (i\/-l)) u1 + +homToP (A B:U) (h: homotopies A B) : Paths (A->B) = transport ((thm A B)@-i) h + +lem6 (A B:U) : (h:homotopies A B) -> IdP (thm A B) (homToP A B h) h = + funDepTrInv (Paths (A->B)) (homotopies A B) (thm A B) + +lem7 (A B:U) (h:homotopies A B) : Id (A->B) (homToP A B h).1 h.1.1 = + lem4 A B p.1 p.2.1 p.2.2 h (lem6 A B h) + where p : Paths (A->B) = homToP A B h + +lem8 (A B:U) (h:homotopies A B) : Id (A->B) (homToP A B h).2.1 h.1.2 = + lem5 A B p.1 p.2.1 p.2.2 h (lem6 A B h) + where p : Paths (A->B) = homToP A B h + +funext (A B:U) (f g :A -> B) (pe : (x:A) -> Id B (f x) (g x)) : Id (A->B) f g = + \ (x:A) -> ((transport rem4 rem3) @ i) x + where + h : homotopies A B = ((f,g),pe) + p : Paths (A->B) = homToP A B h + rem1 : Id (A->B) p.1 f = lem7 A B h + rem2 : Id (A->B) p.2.1 g = lem8 A B h + rem3 : Id (A->B) p.1 p.2.1 = p.2.2 + rem4 : Id U (Id (A->B) p.1 p.2.1) (Id (A->B) f g) = Id (A->B) (rem1@i) (rem2@i) + + diff --git a/examples/helix.ctt b/examples/helix.ctt new file mode 100644 index 0000000..26988fb --- /dev/null +++ b/examples/helix.ctt @@ -0,0 +1,202 @@ +module helix where + +import circle +import hedberg +import retract + +loop1 : loopS1 = loop' +triv : loopS1 = base + +compS1 : loopS1 -> loopS1 -> loopS1 = compId S1 base base base + +encode (x:S1) (p:Id S1 base x) : helix x = subst S1 helix base x p zeroZ + +itLoop : nat -> loopS1 = split + zero -> triv + suc n -> compS1 (itLoop n) loop1 + +invLoop : loopS1 = inv S1 base base loop1 + +itLoopNeg : nat -> loopS1 = split + zero -> invLoop + suc n -> compS1 (itLoopNeg n) invLoop + +loopIt : Z -> loopS1 = split + inl n -> itLoopNeg n + inr n -> itLoop n + +lemItNat (n:nat) : Id loopS1 (itLoop (suc n)) (transport (Id S1 base (loop{S1} @ i)) (itLoop n)) = + refl loopS1 (itLoop (suc n)) + +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 = + comp A (comp A (p @ i) [(i=1) -> q @ (-j /\ k)]) [(i=1) -> q @ (-j /\ - k)] + +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) = + comp A (p @ (-i \/ j)) [(i=1) -> p @ (j \/ k)] + +lemItNeg : (n:nat) -> Id loopS1 (transport (Id S1 base (loop{S1} @ i)) (loopIt (inl n))) (loopIt (sucZ (inl n))) = split + zero -> lemInv S1 base base loop1 + suc n -> lemCompInv S1 base base base (itLoopNeg n) invLoop + +oneTurn (l: loopS1) : loopS1 = transport (Id S1 base (loop{S1} @ i)) l + +lemItPos : (n:nat) -> Id loopS1 (oneTurn (loopIt (predZ (inr n)))) (loopIt (inr n)) = split + zero -> lemInv S1 base base loop1 + suc n -> refl loopS1 (loopIt (inr (suc n))) + +lemItNeg (n:nat) : Id loopS1 (oneTurn (loopIt (predZ (inl n)))) (loopIt (inl n)) = + lemCompInv S1 base base base (loopIt (inl n)) invLoop + +lemIt : (n:Z) -> Id loopS1 (oneTurn (loopIt (predZ n))) (loopIt n) = split + inl n -> lemItNeg n + inr n -> lemItPos n + +funDepTr (A0 A1:U) (p:Id U A0 A1) (u0:A0) (u1:A1) : + Id U (IdP p u0 u1) (Id A1 (transport p u0) u1) = + IdP (p @ (i\/l)) (transport (p @ (i/\l)) u0) u1 + +decode : (x:S1) -> helix x -> Id S1 base x = split + base -> loopIt + loop @ i -> rem @ i + where T : U = Z -> loopS1 + p : Id U T T = helix (loop{S1}@j) -> Id S1 base (loop{S1}@j) + rem1 : Id (Z -> loopS1) (transport p loopIt) loopIt = + funExt Z (\ (n:Z) -> loopS1) (transport ( helix (loop{S1}@j) -> Id S1 base (loop{S1}@j)) loopIt) loopIt lemIt + rem : IdP p loopIt loopIt = transport ( (funDepTr T T p loopIt loopIt)@-j) rem1 + +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 = + (pP (p @ i) (transport (P (p@i /\ j)) b0) (transport (P (p@i \/ -j)) b1)) @ i + +lemPropFib (P:S1 -> U) (pP:(x:S1) -> prop (P x)) (bP: P base) : (x:S1) -> P x = split + base -> bP + loop @ i -> (lemPropF S1 P pP base base loop1 bP bP) @ i + +-- other proof? + +propIsProp (A:U) (f g:prop A) : Id (prop A) f g = + \ (a b :A) -> (propSet A f a b (f a b) (g a b)) @ i + +setIsProp (A:U) (f g:set A) : Id (set A) f g = + \ (a b :A) -> (propIsProp (Id A a b) (f a b) (g a b)) @ i + +helixSet : (x:S1) -> set (helix x) = lemPropFib (\ (x:S1) -> set (helix x)) rem ZSet + where rem (x:S1) : prop (set (helix x)) = setIsProp (helix x) + +retHelix (x:S1) (p : Id S1 base x) : Id (Id S1 base x) (decode x (encode x p)) p = + transport (Id (Id S1 base p@i) (decode p@i (encode p@i (p@(i/\j)))) (p@(i/\j))) (refl loopS1 triv) + +setLoop : set loopS1 = retractSet loopS1 Z (encode base) (decode base) (retHelix base) ZSet + +-- S1 is a groupoid + +groupoid (A:U) : U = (x y:A) -> set (Id A x y) + +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 + = \ (x:A) -> (h x (f0 x) (f1 x)) @ i + +isGroupoidS1 : groupoid S1 = lem + where + lem2 : (y : S1) -> set (Id S1 base y) + = lemPropFib (\ (y:S1) -> set (Id S1 base y)) (\ (y:S1) -> setIsProp (Id S1 base y)) setLoop + + lem : (x y : S1) -> set (Id S1 x y) + = lemPropFib (\ (x:S1) -> (y : S1) -> set (Id S1 x y)) pP lem2 + where + pP (x:S1) : prop ((y:S1) -> set (Id S1 x y)) = + propPi S1 (\ (y:S1) -> set (Id S1 x y)) (\ (y:S1) -> setIsProp (Id S1 x y)) + +substInv (A : U) (P : A -> U) (a x : A) (p : Id A a x) : P x -> P a = + subst A P x a (p @ -i) + +lemSetTorus (E : S1 -> S1 -> U) (sE : set (E base base)) + (f : (y:S1) -> E base y) (g : (x:S1) -> E x base) + (efg : Id (E base base) (f base) (g base)) : (x y:S1) -> E x y = split + base -> f + loop @ i -> lem2 @ i + where + F (x:S1) : U = (y:S1) -> E x y + + G (y x:S1) : U = E x y + + lem1 : (y:S1) -> IdS S1 (G y) base base loop1 (f y) (f y) = lemPropFib P pP bP + where + P (y:S1) : U = IdS S1 (G y) base base loop1 (f y) (f y) + + sbE : (y : S1) -> set (E base y) + = lemPropFib (\ (y:S1) -> set (E base y)) (\ (y:S1) -> setIsProp (E base y)) sE + + pP (y:S1) : prop (P y) = rem3 + where + rem1 : Id U (P y) (Id (E base y) (subst S1 (G y) base base loop1 (f y)) (f y)) + = funDepTr (G y base) (G y base) (G y loop{S1}@j) (f y) (f y) + + rem2 : prop (Id (E base y) (subst S1 (G y) base base loop1 (f y)) (f y)) + = sbE y (subst S1 (G y) base base loop1 (f y)) (f y) + + rem3 : prop (P y) + = substInv U prop (P y) (Id (E base y) (subst S1 (G y) base base loop1 (f y)) (f y)) rem1 rem2 + + lem2 : IdS S1 (G base) base base loop1 (g base) (g base) + = g (loop1 @ j) + + bP : P base + = substInv (E base base) (\ (u:E base base) -> IdS S1 (G base) base base loop1 u u) (f base) (g base) efg lem2 + + lem2 : IdS S1 F base base loop1 f f = \ (y:S1) -> (lem1 y) @ j + +-- commutativity of mult, at last + +idL : (x : S1) -> Id S1 (mult base x) x = split + base -> refl S1 base + loop @ i -> loop1 @ i + +multCom : (x y : S1) -> Id S1 (mult x y) (mult y x) = + lemSetTorus E sE idL g efg + where + E (x y: S1) : U = Id S1 (mult x y) (mult y x) + sE : set (E base base) = isGroupoidS1 base base + g (x : S1) : E x base = inv S1 (mult base x) (mult x base) (idL x) + efg : Id (E base base) (idL base) (g base) = refl (E base base) (idL base) + +-- associativity + +multAssoc (x :S1) : (y z : S1) -> Id S1 (mult x (mult y z)) (mult (mult x y) z) = + lemSetTorus E sE f g efg + where + E (y z : S1) : U = Id S1 (mult x (mult y z)) (mult (mult x y) z) + sE : set (E base base) = isGroupoidS1 x x + f (z : S1) : E base z = rem + where + rem1 : Id S1 (mult base z) z = multCom base z + + rem : Id S1 (mult x (mult base z)) (mult x z) = mult x (rem1 @ i) + g (y : S1) : E y base = refl S1 (mult x y) + efg : Id (E base base) (f base) (g base) = refl (E base base) (f base) + +-- inverse law + +lemPropRel (P:S1 -> S1 -> U) (pP:(x y:S1) -> prop (P x y)) (bP:P base base) : (x y:S1) -> P x y = + lemPropFib (\ (x:S1) -> (y:S1) -> P x y) + (\ (x:S1) -> propPi S1 (P x) (pP x)) + (lemPropFib (P base) (pP base) bP) + +invLaw : (x y : S1) -> + Id (Id S1 (mult x y) (mult x y)) (refl S1 (mult x y)) + (compId S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x)) = lemPropRel P pP bP + where + P (x y : S1) : U + = Id (Id S1 (mult x y) (mult x y)) (refl S1 (mult x y)) + (compId S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x)) + + pP (x y : S1) : prop (P x y) = + isGroupoidS1 (mult x y) (mult x y) (refl S1 (mult x y)) + (compId S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x)) + + bP : P base base = refl (Id S1 base base) (refl S1 base) + + +-- homotopy + +aLoop : loopS1 = loop{S1}@(i/\-i) + +test : Id loopS1 triv aLoop = loop{S1}@(j/\i/\-i)