move context of indSusp to susp

diff --git a/examples/indSusp.ctt b/examples/indSusp.ctt
deleted file mode 100644 (file)
index 4d88d12..0000000
--- a/examples/indSusp.ctt
+++ /dev/null
@@ -1,27 +0,0 @@
-module indSusp where
-
-import susp
-
-suspOf (A X : U) : U = (u:X) * (v:X) * (A -> Id X u v)
-
-funToL (A X:U) (f:susp A -> X) : suspOf A X =
-  (f north,f south,\ (a:A) -> <i>f (merid{susp A} a@i))
-
-lToFun (A X:U) (z:suspOf A X) : susp A -> X = split
- north -> z.1
- south -> z.2.1
- merid a @ i-> z.2.2 a @ i
-
-test1 (A X:U) (z:suspOf A X) : Id (suspOf A X) (funToL A X (lToFun A X z)) z
-   = refl (suspOf A X) z
-
-rem (A X:U) (f:susp A ->X) : (u:susp A) -> Id X (lToFun A X (funToL A X f) u) (f u) = split
-    north -> refl X (f north)
-    south -> refl X (f south)
-    merid a @ i -> refl X (f (merid{susp A} a @ i))
-
-test2 (A X:U) (f:susp A ->X) : Id (susp A ->X) (lToFun A X (funToL A X f)) f
-   = <i>\ (u:susp A) -> rem A X f u @ i
-
-funSusp (A X:U) : Id U (susp A -> X) (suspOf A X) =
- isoId (susp A -> X) (suspOf A X) (funToL A X) (lToFun A X) (test1 A X) (test2 A X)

diff --git a/examples/susp.ctt b/examples/susp.ctt
index aa4e587d4300b710f032b52f550057ca71bd392a..b6050d89c468db69fc8328229bc202bb0392b564 100644 (file)
--- a/examples/susp.ctt
+++ b/examples/susp.ctt
@@ -114,3 +114,29 @@ loop2S : Id sone north north = compId sone north north north loop1S loop1S
 -- test4S : Z = windingS (compId sone north north north loop2S loop2S)\r
 \r
 \r
+-- indSusp:\r
+\r
+\r
+suspOf (A X : U) : U = (u:X) * (v:X) * (A -> Id X u v)\r
+\r
+funToL (A X:U) (f:susp A -> X) : suspOf A X =\r
+  (f north,f south,\ (a:A) -> <i>f (merid{susp A} a@i))\r
+\r
+lToFun (A X:U) (z:suspOf A X) : susp A -> X = split\r
+ north -> z.1\r
+ south -> z.2.1\r
+ merid a @ i-> z.2.2 a @ i\r
+\r
+test1 (A X:U) (z:suspOf A X) : Id (suspOf A X) (funToL A X (lToFun A X z)) z\r
+   = refl (suspOf A X) z\r
+\r
+rem (A X:U) (f:susp A ->X) : (u:susp A) -> Id X (lToFun A X (funToL A X f) u) (f u) = split\r
+    north -> refl X (f north)\r
+    south -> refl X (f south)\r
+    merid a @ i -> refl X (f (merid{susp A} a @ i))\r
+\r
+test2 (A X:U) (f:susp A ->X) : Id (susp A ->X) (lToFun A X (funToL A X f)) f\r
+   = <i>\ (u:susp A) -> rem A X f u @ i\r
+\r
+funSusp (A X:U) : Id U (susp A -> X) (suspOf A X) =\r
+ isoId (susp A -> X) (suspOf A X) (funToL A X) (lToFun A X) (test1 A X) (test2 A X)\r