updated multS1

diff --git a/examples/mult.ctt b/examples/mult.ctt
index a0a88cfe44ac53046b30bdef85f3308460238a5e..859805e3483f365f325fc65c0625d6b34ad79822 100644 (file)
--- a/examples/mult.ctt
+++ b/examples/mult.ctt
@@ -1,7 +1,6 @@
 module mult where
 
-import susp
-import helix
+import circle
 
 -- another inverse function
 
@@ -9,41 +8,39 @@ invS : S1 -> S1 = split
  base -> base
  loop @ i -> loop1 @ -i
 
+test (x:S1) : S1 = mult x (invS x)
+testL : Id S1 base base = <i>test (loop{S1} @ i)
+test1 (x:S1) : S1 = mult (invS x) x
 
+-- test0S : Z = winding (<i>mult (loop2@i) (invS (loop2@i)))
+-- loop4 : loopS1 = compS1 loop2 loop2
+-- test00S : Z = winding (<i>mult (loop4@i) (invS (loop4@i)))
 
-lemInv : (x:S1) -> Id S1 (mult x (invS x)) base = split 
- base -> refl S1 base
- loop @ i -> <j>base
+-- lemInv1 : (x:S1) -> Id S1 (mult (invS x) x) base = split
+-- base -> refl S1 base
+-- loop @ i -> <j> base -- loop1 @ -i\/i\/j
 
-test0S : Z = winding (<i>mult (loop2@i) (invS (loop2@i)))
-loop4 : loopS1 = compS1 loop2 loop2
-test00S : Z = winding (<i>mult (loop4@i) (invS (loop4@i)))
-
-lemInv1 : (x:S1) -> Id S1 (mult (invS x) x) base = split
- base -> refl S1 base
- loop @ i -> <j> base -- loop1 @ -i\/i\/j
-
-test : loopS1 = <i> mult (loop1@i) (loop1@-i)
-test1 : IdP (<i>Id S1 (mult (loop1@i) base) (mult (loop1@i) base)) loop1 loop1 = <i j> mult (loop1@i) (loop1@j)
-test2 : loopS1 = <i> mult (loop1@i) (loop1@i)
+test2 : loopS1 = <i> mult (loop1@i) (loop1@-i)
+-- test1 : IdP (<i>Id S1 (mult (loop1@i) base) (mult (loop1@i) base)) loop1 loop1 = <i j> mult (loop1@i) (loop1@j)
+test3 : loopS1 = <i> mult (loop1@i) (loop1@i)
 -- test3 : Id loopS1 test2 (compS1 loop1 loop1) = refl loopS1 test2
 
-lemBase (y:S1) : Id S1 (mult base (mult base y)) y = 
- compId S1 (mult base (mult base y)) (mult base y) y (idL (mult base y)) (idL y)
+-- lemBase (y:S1) : Id S1 (mult base (mult base y)) y = 
+-- compId S1 (mult base (mult base y)) (mult base y) y (idL (mult base y)) (idL y)
 
-corrInv (x y : S1) : Id S1 (mult x (mult (invS x) y)) y =
- compId S1 (mult x (mult (invS x) y)) (mult (mult x (invS x)) y) y rem1 rem
- where rem1 : Id S1 (mult x (mult (invS x) y)) (mult (mult x (invS x)) y) = multAssoc x (invS x) y
+-- corrInv (x y : S1) : Id S1 (mult x (mult (invS x) y)) y =
+--  compId S1 (mult x (mult (invS x) y)) (mult (mult x (invS x)) y) y rem1 rem
+--  where rem1 : Id S1 (mult x (mult (invS x) y)) (mult (mult x (invS x)) y) = multAssoc x (invS x) y
 
-       rem : Id S1 (mult (mult x (invS x)) y) y =
-        compId S1 (mult (mult x (invS x)) y) (mult base y) y  (<i>mult (lemInv x @i) y) (idL y)
+--        rem : Id S1 (mult (mult x (invS x)) y) y =
+--         compId S1 (mult (mult x (invS x)) y) (mult base y) y  (<i>mult (lemInv x @i) y) (idL y)
 
-corrInv1 (x y : S1) : Id S1 (mult (invS x) (mult x y)) y =
- compId S1 (mult (invS x) (mult x y)) (mult (mult (invS x) x) y) y rem1 rem
- where rem1 : Id S1 (mult (invS x) (mult x y)) (mult (mult (invS x) x) y) = multAssoc (invS x) x y
+-- corrInv1 (x y : S1) : Id S1 (mult (invS x) (mult x y)) y =
+--  compId S1 (mult (invS x) (mult x y)) (mult (mult (invS x) x) y) y rem1 rem
+--  where rem1 : Id S1 (mult (invS x) (mult x y)) (mult (mult (invS x) x) y) = multAssoc (invS x) x y
 
-       rem : Id S1 (mult (mult (invS x) x) y) y =
-        compId S1 (mult (mult (invS x) x) y) (mult base y) y (<i>mult (lemInv1 x@i) y) (idL y)
+--        rem : Id S1 (mult (mult (invS x) x) y) y =
+--         compId S1 (mult (mult (invS x) x) y) (mult base y) y (<i>mult (lemInv1 x@i) y) (idL y)
 
-eqS1 (x:S1) : Id U S1 S1 = isoId S1 S1 (mult x) (mult (invS x)) (corrInv x) (corrInv1 x)
+-- eqS1 (x:S1) : Id U S1 S1 = isoId S1 S1 (mult x) (mult (invS x)) (corrInv x) (corrInv1 x)
 

diff --git a/examples/multS1.ctt b/examples/multS1.ctt
index e710e217ae3225f2c17ba4cbb8c180558e78dd78..b7e0cee6e5a529032d665774c3107d74294f67e8 100644 (file)
--- a/examples/multS1.ctt
+++ b/examples/multS1.ctt
@@ -1,12 +1,30 @@
 module multS1 where
 
-import susp
-import equiv
+import circle
 
 -- another inverse function
 
 -- the multiplication is invertible
 
+propIsContr (A:U) (z0 z1:isContr A) : Id (isContr A) z0 z1 =
+ <j>(p0 a1@j,
+     \ (x:A) -> 
+        <i>comp (<_>A) (lem1 x@i@j) [ (i=0) -> <k>p0 a1@j, (i=1) -> <k>p0 x@(j\/k),
+                                      (j=0) -> <k>p0 x@(i/\k), (j=1) -> <k>p1 x@i ])
+ where
+  a0 : A = z0.1
+  p0 : (x:A) -> Id A a0 x = z0.2
+  a1 : A = z1.1
+  p1 : (x:A) -> Id A a1 x = z1.2
+  lem1 (x:A) : IdP (<i>Id A a0 (p1 x@i)) (p0 a1) (p0 x) = <i j> p0 (p1 x@i) @ j
+ 
+propIsEquiv (A B : U) (f : A -> B)
+  : prop (isEquiv A B f) = \ (u0 u1:isEquiv A B f) -> <i> \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i
+
+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) : IdP (<i>P (p@i)) b0 b1 =
+ <i>pP (p@i) (comp (<j>P (p@i/\j)) b0 [(i=0) -> <_>b0]) (comp (<j>P (p@i\/-j)) b1 [(i=1) -> <_>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
@@ -15,7 +33,6 @@ 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)
@@ -24,52 +41,57 @@ multIsEquiv : (x:S1) -> isEquiv S1 S1 (mult x) =  lemPropFib P pP bP
 
 -- inverse of multiplication by x
 
-invMult (x y:S1) : S1 = ((multIsEquiv x).1 y).1
+invMult (x y:S1) : S1 = (multIsEquiv x y).1.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)))
+test2 : Id S1 pt0 pt0 = mapOnPath S1 S1 invS1 base base loop2
+
+test2 : Id S1 pt0 pt0 = 
+  <i> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (i = 0) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) base []) [] ], (i = 1) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base [ (j = 0) -> <k> comp (<_>S1) base [ (k = 0) -> <l> base ], (j = 1) -> <k> comp (<_>S1) base [ (k = 0) -> <l> base ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) base []) [ (k = 0) -> <l> comp (<_>S1) base [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) base []) [ (k = 0) -> <l> comp (<_>S1) base [] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ] ] ]) [ (i = 0) -> <j> comp (<_>S1) (comp (<_>S1) base []) [ (j = 1) -> <k> comp (<_>S1) base [] ], (i = 1) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) [ (j = 1) -> <k> comp (<_>S1) base [] ]) []) [] ]) [ (i = 0) -> <j> comp (<_>S1) (comp (<_>S1) base []) [ (j = 0) -> <k> comp (<_>S1) base [] ], (i = 1) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (loop {S1} @ -j) []) []) []) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ] ]) [ (i = 0) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) base []) [] ], (i = 1) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base [ (j = 0) -> <k> comp (<_>S1) base [ (k = 0) -> <l> base ], (j = 1) -> <k> comp (<_>S1) base [ (k = 0) -> <l> base ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) base []) [ (k = 0) -> <l> comp (<_>S1) base [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) base []) [ (k = 0) -> <l> comp (<_>S1) base [] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [] ] ] ]) [ (i = 0) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ], (i = 1) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) []) [ (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [] ] ]) [ (i = 0) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) [ (j = 1) -> <k> comp (<_>S1) base [] ]) []) [], (i = 1) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ] ]) [ (i = 0) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base [ (j = 1) -> <k> base ]) []) [], (i = 1) -> <j> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base [ (j = 1) -> <k> base ]) []) []) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (k = 1) -> <l> comp (<_>S1) (comp (<_>S1) base []) [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base [ (k = 0) -> <l> comp (<_>S1) base [ (l = 0) -> <m> base ], (k = 1) -> <l> comp (<_>S1) base [ (l = 0) -> <m> base ] ]) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [ (l = 0) -> <m> comp (<_>S1) base [] ], (k = 1) -> <l> comp (<_>S1) (comp (<_>S1) base []) [ (l = 0) -> <m> comp (<_>S1) base [] ] ]) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [], (k = 1) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (l = 0) -> <m> comp (<_>S1) (comp (<_>S1) base []) [] ] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) base []) [ (k = 1) -> <l> comp (<_>S1) base [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base [ (k = 1) -> <l> base ]) []) [] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) base []) [ (k = 0) -> <l> comp (<_>S1) base [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (loop {S1} @ -k) []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base [ (k = 0) -> <l> comp (<_>S1) base [ (l = 0) -> <m> base ], (k = 1) -> <l> comp (<_>S1) base [ (l = 0) -> <m> base ] ]) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) base []) [ (l = 0) -> <m> comp (<_>S1) base [] ], (k = 1) -> <l> comp (<_>S1) (comp (<_>S1) base []) [ (l = 0) -> <m> comp (<_>S1) base [] ] ]) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (l = 0) -> <m> comp (<_>S1) (comp (<_>S1) base []) [] ], (k = 1) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (l = 0) -> <m> comp (<_>S1) (comp (<_>S1) base []) [] ] ]) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [], (k = 1) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (l = 0) -> <m> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (k = 0) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) [ (k = 1) -> <l> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [] ] ]) [ (j = 0) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) [ (k = 1) -> <l> comp (<_>S1) base [] ]) []) [], (j = 1) -> <k> comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) [ (k = 1) -> <l> comp (<_>S1) (comp (<_>S1) base []) [] ] ] ]
+
+-- invsone : sone -> sone  = subst U (\ (X:U) -> X -> X) <_>S1 sone (<i>s1EqCircle@-i) inv<_>S1
+
+-- 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
+loopM2 : Id <_>S1 pt0 test1 = mapOnPath S1 S1 invS1 base base loop2
 
 loopM0 : Id S1 pt0 pt0 = <i>invMult (loop2@i) (loop2@i)
 -}