small modification in the file susp

diff --git a/examples/susp.ctt b/examples/susp.ctt
index c1212ce7602362b876f0f72589d0af8dbf2d9dc0..2a79d9fcbe4f47b2816a1299153173c3b288dd50 100644 (file)
--- a/examples/susp.ctt
+++ b/examples/susp.ctt
@@ -67,12 +67,6 @@ s1EqS1 : Id U S1 S1 = compId U S1 sone S1 (inv U sone S1 s1EqCircle) s1EqCircle
 \r
 ptU : U = (X : U) * X\r
 \r
-lemPt1 (A :U) : (B:U) (p:Id U A B) (a:A) -> Id ptU (A,a) (B,transport p a)\r
- = J U A (\ (B:U) (p:Id U A B) -> (a:A) -> Id ptU (A,a) (B,transport p a))\r
-   (\ (a:A) -> refl ptU (A,a))\r
-\r
-s1PtCircle1 : Id ptU (sone,north) (S1,base) = lemPt1 sone S1 s1EqCircle north\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
 \r
@@ -88,12 +82,6 @@ windingS : Id sone north north -> Z = rem1
   rem : G (S1,base) = winding\r
   rem1 : G (sone,north) = subst ptU G (S1,base) (sone,north) (<i> s1PtCircle @ -i) rem\r
 \r
-windingT : loopS1 -> Z = rem1\r
- where\r
-  G (X: ptU): U = (Omega X).1 -> Z\r
-  rem : G (S1,base) = winding\r
-  rem1 : G (S1,base) = subst ptU G (S1,base) (S1,base) s1PtS1 rem\r
-\r
 s1ToCId (p: Id sone north north) : Id S1 base base\r
  = <i> transport s1EqCircle (p @ i) \r
 \r
@@ -108,6 +96,3 @@ test0S : Z = windingS (refl sone north)
 \r
 test2S : Z = windingS loop2S\r
 \r
-winding' (l : Id sone north north) : Z = winding (s1ToCId l)\r
-\r
-testS : Id sone north north = <i> comp sone (m0 @ i) [ (i=1) -> <k> m1 @ (-k)]\r