added some examples

diff --git a/examples/collection.ctt b/examples/collection.ctt
index 606b26911ac6a803bd8fd4a89ff2052dc312644c..984f6e262303a7071428bce9e39f531c989a3a84 100644 (file)
--- 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 (file)
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 -> <j> 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) = <i>\ (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 (<i>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 =
+ <i> 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 (<i>lemPt1@-i))
+
+-- take a lot of time and memory
+
+test3 : Z = windingS (transpSone (<i>invsone (loop1S@i)))
+test4 : Z = windingS (transpSone (<i>pt1))
+test5 : Z = windingS (transpSone (<i>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 = <i>invMult (loop2@i) (loop2@i)
+-}
+

diff --git a/examples/sigma.ctt b/examples/sigma.ctt
index 7b3d7a25a2ee351266bebbd37909b23bf272044a..40ab04a04c67161d51279b50a86cdebabdd951e0 100644 (file)
--- 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 []
+--  <i>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 (<i> P (p@i)) u0 u1) (Id (P a1) (transport (<i> P (p@i)) u0) u1) =
+ J A a0 (\ (a1:A) (p:Id A a0 a1) -> (u0:P a0) (u1:P a1) ->
+             Id U (IdP (<i> P (p@i)) u0 u1) (Id (P a1) (transport (<i> 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) =
+         <i>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) =
+         <i>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 (<i>B (p@i)) t.2 u.2) (Id (B u.1) (transport (<i>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 (<i>B (p@i)) t.2 u.2) =
- (substInv U prop T0 T1 rem rem1,rem2)
+  isContr (IdP (<i>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) = <i>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 = <i>(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 = <i>(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) =