From: coquand Date: Fri, 3 Jul 2015 11:17:10 +0000 (+0200) Subject: added some examples X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=829b5cd999d1ec5cc3e80bb0f6c79c95ca9f9529;p=cubicaltt.git added some examples --- diff --git a/examples/collection.ctt b/examples/collection.ctt index 606b269..984f6e2 100644 --- a/examples/collection.ctt +++ b/examples/collection.ctt @@ -9,17 +9,17 @@ setFun (A B:U) (sB: set B) : set (A -> B) = setPi A (\ (x:A) -> B) (\ (x:A) -> s groupoidFun (A B : U) (gB:groupoid B) : groupoid (A -> B) = groupoidPi A (\ (x:A) -> B) (\ (x:A) -> gB) -lem3 (A B : U) (t u : Equiv A B) : Id U (Id (Equiv A B) t u) (Id (A -> B) t.1 u.1) +lem3 (A B : U) (t u : equiv A B) : Id U (Id (equiv A B) t u) (Id (A -> B) t.1 u.1) = lemSigProp (A->B) (isEquiv A B) (propIsEquiv A B) t u -lem4 (A B : U) (sB:set B) (t u:Equiv A B) : prop (Id (Equiv A B) t u) - = substInv U prop (Id (Equiv A B) t u) (Id (A -> B) t.1 u.1) (lem3 A B t u) (setFun A B sB t.1 u.1) +lem4 (A B : U) (sB:set B) (t u:equiv A B) : prop (Id (equiv A B) t u) + = substInv U prop (Id (equiv A B) t u) (Id (A -> B) t.1 u.1) (lem3 A B t u) (setFun A B sB t.1 u.1) -lem5 (A B : U) (gB:groupoid B) (t u:Equiv A B) : set (Id (Equiv A B) t u) - = substInv U set (Id (Equiv A B) t u) (Id (A -> B) t.1 u.1) (lem3 A B t u) (groupoidFun A B gB t.1 u.1) +lem5 (A B : U) (gB:groupoid B) (t u:equiv A B) : set (Id (equiv A B) t u) + = substInv U set (Id (equiv A B) t u) (Id (A -> B) t.1 u.1) (lem3 A B t u) (groupoidFun A B gB t.1 u.1) lem6 (A B : U) (sB : set B) : set (Id U A B) = - retractSet (Id U A B) (Equiv A B) (IdToEquiv A B) (EquivToId A B) (secIdEquiv A B) (lem4 A B sB) + substInv U set (Id U A B) (equiv A B) (univalence1 A B) (lem4 A B sB) -- the collection of all sets diff --git a/examples/multS1.ctt b/examples/multS1.ctt new file mode 100644 index 0000000..e710e21 --- /dev/null +++ b/examples/multS1.ctt @@ -0,0 +1,76 @@ +module multS1 where + +import susp +import equiv + +-- another inverse function + +-- the multiplication is invertible + +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 + +idL : (x : S1) -> Id S1 (mult base x) x = split + base -> refl S1 base + loop @ i -> loop1 @ i + + +multIsEquiv : (x:S1) -> isEquiv S1 S1 (mult x) = lemPropFib P pP bP + where P (x:S1) : U = isEquiv S1 S1 (mult x) + pP (x:S1) : prop (P x) = propIsEquiv S1 S1 (mult x) + rem : Id (S1 -> S1) (idfun S1) (mult base) = \ (x:S1) -> idL x @ -i + bP : P base = subst (S1->S1) (isEquiv S1 S1) (idfun S1) (mult base) rem (idIsEquiv S1) + +-- inverse of multiplication by x + +invMult (x y:S1) : S1 = ((multIsEquiv x).1 y).1 + +invS1 (x:S1) : S1 = invMult x base + +pt0 : S1 = mapOnPath S1 S1 invS1 base base loop2@0 +test1 : S1 = mapOnPath S1 S1 invS1 base base loop2@1 + +invsone : sone -> sone = subst U (\ (X:U) -> X -> X) S1 sone (s1EqCircle@-i) invS1 + +cSone : Id U sone sone = <_>sone + +pt1 : sone = + transport cSone + (transport cSone + (transport cSone + (transport cSone + (transport cSone + (transport cSone + (transport cSone + (transport cSone + (transport cSone + (transport cSone (transport cSone north)))))))))) + +lemPt1 : Id sone north pt1 = + comp cSone + (comp cSone + (comp cSone + (comp cSone + (comp cSone + (comp cSone + (comp cSone + (comp cSone + (comp cSone + (comp cSone (comp cSone north [(i=0)-><_>north]) [(i=0)-><_>north]) [(i=0)-><_>north]) [(i=0)-><_>north]) [(i=0)-><_>north]) [(i=0)-><_>north]) [(i=0)-><_>north]) [(i=0)-><_>north]) [(i=0)-><_>north]) [(i=0)-><_>north]) [(i=0)-><_>north] + +transpSone (l:Id sone pt1 pt1) : Id sone north north = + compId sone north pt1 north lemPt1 (compId sone pt1 pt1 north l (lemPt1@-i)) + +-- take a lot of time and memory + +test3 : Z = windingS (transpSone (invsone (loop1S@i))) +test4 : Z = windingS (transpSone (pt1)) +test5 : Z = windingS (transpSone (invsone (loop2S@i))) + +{- take a lot of time to type-check +loopM2 : Id S1 pt0 test1 = mapOnPath S1 S1 invS1 base base loop2 + +loopM0 : Id S1 pt0 pt0 = invMult (loop2@i) (loop2@i) +-} + diff --git a/examples/sigma.ctt b/examples/sigma.ctt index 7b3d7a2..40ab04a 100644 --- a/examples/sigma.ctt +++ b/examples/sigma.ctt @@ -1,6 +1,6 @@ module sigma where -import deppath +-- import deppath import equiv -- application of this fact @@ -26,6 +26,22 @@ lem (A:U) (P:A->U) (pP:(x:A) -> prop (P x)) (u v:(x:A) * P x) (p:Id A u.1 v.1) : propSig (A:U) (B:A-> U) (pA:prop A) (pB : (x:A) -> prop (B x)) (t u : sig A B) : Id (sig A B) t u = lem A B pB t u (pA t.1 u.1) +lemTransp (A:U) (a:A) : Id A a (transport (<_>A) a) = fill (<_>A) a [] +-- genComp (<_>A) a [(i=0) -> <_>a] + +funDepTr (A:U) (P:A->U) (a0 :A) : (a1:A) (p:Id A a0 a1) (u0:P a0) (u1:P a1) -> + Id U (IdP ( P (p@i)) u0 u1) (Id (P a1) (transport ( P (p@i)) u0) u1) = + J A a0 (\ (a1:A) (p:Id A a0 a1) -> (u0:P a0) (u1:P a1) -> + Id U (IdP ( P (p@i)) u0 u1) (Id (P a1) (transport ( P (p@i)) u0) u1)) rem + where rem (u0 u1:P a0) : Id U (Id (P a0) u0 u1) (Id (P a0) (transport (<_>P a0) u0) u1) = + Id (P a0) (lemTransp (P a0) u0@i) u1 + +funDepTr (A0:U) : (A1:U) (P:Id U A0 A1) (u0:A0) (u1:A1) -> + Id U (IdP P u0 u1) (Id A1 (transport P u0) u1) = + J U A0 (\ (A1:U) (P:Id U A0 A1) -> (u0:A0) (u1:A1) -> Id U (IdP P u0 u1) (Id A1 (transport P u0) u1)) rem + where rem (u0 u1:A0) : Id U (Id A0 u0 u1) (Id A0 (transport (<_>A0) u0) u1) = + Id A0 (lemTransp A0 u0@i) u1 + lem2 (A:U) (B:A-> U) (t u : sig A B) (p:Id A t.1 u.1) : Id U (IdP (B (p@i)) t.2 u.2) (Id (B u.1) (transport (B (p@i)) t.2) u.2) = funDepTr (B t.1) (B u.1) P t.2 u.2 @@ -80,9 +96,11 @@ groupoidSig (A:U) (B:A-> U) (gA: groupoid A) (gB : (x:A) -> groupoid (B x)) (t u rem2 : set ((p:T) * C p) = setSig T C rem1 rem rem3 : Id U (Id (sig A B) t u) ((p:T) * C p) = lemIdSig A B t u +lemContr (A:U) (pA:prop A) (a:A) : isContr A = (a,rem) + where rem (y:A) : Id A a y = pA a y + lem3 (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : sig A B) (p:Id A t.1 u.1) : - isContr (IdP (B (p@i)) t.2 u.2) = - (substInv U prop T0 T1 rem rem1,rem2) + isContr (IdP (B (p@i)) t.2 u.2) = lemContr T0 (substInv U prop T0 T1 rem rem1) rem2 where P : Id U (B t.1) (B u.1) = B (p@i) T0 : U = IdP P t.2 u.2 T1 : U = Id (B u.1) (transport P t.2) u.2 @@ -95,8 +113,8 @@ lem6 (A:U) (P:A-> U) (cA:(x:A) -> isContr (P x)) : Id U ((x:A)*P x) A = isoId T where T : U = (x:A) * P x f (z:T) : A = z.1 - g (x:A) : T = (x,(cA x).2) - s (z:T) : Id T (g (f z)) z = (z.1,((cA z.1).1 (cA z.1).2 z.2)@ i) + g (x:A) : T = (x,(cA x).1) + s (z:T) : Id T (g (f z)) z = (z.1,((cA z.1).2 z.2)@ i) t (x:A) : Id A (f (g x)) x = refl A x lemSigProp (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : sig A B) : Id U (Id (sig A B) t u) (Id A t.1 u.1) =