Update susp

diff --git a/examples/susp.ctt b/examples/susp.ctt
index 20a80c92681b66a8e52de0556080b68e013672cd..aa4e587d4300b710f032b52f550057ca71bd392a 100644 (file)
--- a/examples/susp.ctt
+++ b/examples/susp.ctt
@@ -36,18 +36,14 @@ circleToS1 : S1 -> sone = split
 \r
 merid1 (b:bool) : Id sone north south = <i> merid{sone} b @ i\r
 \r
-oc (x:S1) : S1 = s1ToCircle (circleToS1 x)\r
-\r
-ocid : (x : S1) -> Id S1 (oc x) x = split\r
-    base -> refl S1 base\r
-    loop @ i -> <j> oc (loop1 @ i)\r
-\r
 co (x: sone) : sone = circleToS1 (s1ToCircle x)\r
 \r
 lemSquare (A:U) (a b : A) (m0 m1 : Id A a b) :\r
-  Square A a a (compId A a b a m0 (inv A a b m1)) a b m0 (refl A a) m1 =\r
- <j i> comp A (m0 @ j) [(j=1) -> <k> m1 @ (i \/ -k)\r
-                       ,(i=0) -> <k> comp A (m0 @ j) [(j=1) -> <l> m1 @ (-k \/ -l)]]\r
+  Square A a a a b (compId A a b a m0 (inv A a b m1)) m0 (refl A a) m1 =\r
+ <i j> comp (<_>A) (m0 @ i) [(i=1) -> <k> m1 @ (j \/ -k),\r
+                        (i=0) -> <_>a,\r
+                        (j=1) -> <_>m0@i,\r
+                        (j=0) -> <k> comp (<_>A) (m0 @ i) [(k=0) -> <_>m0@i, (i=0) -> <_>a, (i=1) -> <l> m1 @ (-k \/ -l)]]\r
 \r
 coid : (x : sone) -> Id sone (co x) x = split\r
  north -> refl sone north\r
@@ -60,44 +56,61 @@ coid : (x : sone) -> Id sone (co x) x = split
       false -> lemSquare sone north south m0 m1\r
       true -> <j k> m1 @ (j /\ k)\r
 \r
+oc (x:S1) : S1 = s1ToCircle (circleToS1 x)\r
+\r
+ocid : (x : S1) -> Id S1 (oc x) x = \r
+ split\r
+    base -> refl S1 base\r
+    loop @ i -> <j>comp (<_>S1) (loop1@i) [(i=0) -> <_>base,(i=1) -> <_>base,(j=1) -> <_>loop1@i, \r
+                                      (j=0) ->  <k>comp (<_>S1) (loop1 @ i)[(k=0) -> <_>loop1@i,(i=0) -> <_>base,(i=1)-><_>base]]\r
+\r
+\r
+\r
 s1EqCircle : Id U sone S1 = isoId sone S1 s1ToCircle circleToS1 ocid coid\r
 \r
 s1EqS1 : Id U S1 S1 = compId U S1 sone S1 (inv U sone S1 s1EqCircle) s1EqCircle\r
 \r
+lem (A:U) (a:A) : Id A (comp (<_>A) (comp (<_>A) (comp (<_>A) a []) []) []) a = \r
+ <i>comp (<_>A) (comp (<_>A) (comp (<_>A) a [(i=1) -> <_>a]) [(i=1) -> <_>a]) [(i=1) -> <_>a]\r
+\r
+\r
+\r
 -- pointed sets\r
 \r
 ptU : U = (X : U) * X\r
 \r
 lemPt (A :U) (B:U) (p:Id U A B) (a:A) : Id ptU (A,a) (B,transport p a) =\r
- <i> (p @ i,transport (<j> p @ (i/\j)) a)\r
+ <i> (p @ i,comp (<j> p @ (i/\j)) a [(i=0) -> <_>a])\r
 \r
 Omega (X:ptU) : ptU = (Id X.1 X.2 X.2,refl X.1 X.2)\r
 \r
-s1PtCircle : Id ptU (sone,north) (S1,base) = lemPt sone S1 s1EqCircle north\r
+lem (A:U) (a:A) : Id A (comp (<_>A) (comp (<_>A) (comp (<_>A) a []) []) []) a = \r
+ <i>comp (<_>A) (comp (<_>A) (comp (<_>A) a [(i=1) -> <_>a]) [(i=1) -> <_>a]) [(i=1) -> <_>a]\r
+\r
+lem1 (A:U) (a:A) : Id ptU (A,comp (<_>A) (comp (<_>A) (comp (<_>A) a []) []) []) (A,a) = \r
+ <i>(A,lem A a@i)\r
 \r
-s1PtS1 : Id ptU (S1,base) (S1,base) = lemPt S1 S1 s1EqS1 base\r
+-- s1PtCircle : Id ptU (sone,north) (S1,base) = \r
+--  compId ptU (sone,north) (S1,comp (<_>S1) (comp (<_>S1) (comp (<_>S1) base []) []) []) (S1,base) (lemPt sone S1 s1EqCircle north) (lem1 S1 base) \r
 \r
-windingS : Id sone north north -> Z = rem1\r
- where\r
-  G (X:ptU) : U = (Omega X).1 -> Z\r
-  rem : G (S1,base) = winding\r
-  rem1 : G (sone,north) = subst ptU G (S1,base) (sone,north) (<i> s1PtCircle @ -i) rem\r
+-- windingS : Id sone north north -> Z = rem1\r
+--  where\r
+--   G (X:ptU) : U = (Omega X).1 -> Z\r
+--   rem : G (S1,base) = winding\r
+--   rem1 : G (sone,north) = subst ptU G (S1,base) (sone,north) (<i> s1PtCircle @ -i) rem\r
 \r
-s1ToCId (p: Id sone north north) : Id S1 base base\r
- = <i> transport s1EqCircle (p @ i)\r
+-- s1ToCId (p: Id sone north north) : Id S1 base base  = <i> transport s1EqCircle (p @ i)\r
 \r
-s1ToCIdInv (p : Id S1 base base) : Id sone north north\r
- = <i> (transport (<j> s1EqCircle @ -j) (p @ i))\r
+-- s1ToCIdInv (p : Id S1 base base) : Id sone north north  = <i> (transport (<j> s1EqCircle @ -j) (p @ i))\r
 \r
-loop1S :  Id sone north north = s1ToCIdInv loop1\r
+loop1S :  Id sone north north = compId sone north south north m0 invm1\r
 \r
 loop2S : Id sone north north = compId sone north north north loop1S loop1S\r
 \r
-test0S : Z = windingS (refl sone north)\r
+-- test0S : Z = windingS (refl sone north)\r
+\r
+-- test2S : Z = windingS loop2S\r
 \r
-test2S : Z = windingS loop2S\r
+-- test4S : Z = windingS (compId sone north north north loop2S loop2S)\r
 \r
--- The sphere is the suspension of the circle:\r
-S2 : U = susp S1\r
 \r
-loopS2 : U = Id S2 north north\r