From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Thu, 7 Jul 2016 11:43:02 +0000 (+0200)
Subject: move context of indSusp to susp
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=49a61382cdc4d0664c06846a4a35b1b799f1b1b9;p=cubicaltt.git

move context of indSusp to susp
---

diff --git a/examples/indSusp.ctt b/examples/indSusp.ctt
deleted file mode 100644
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 aa4e587..b6050d8 100644
--- 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)
 
 
+-- indSusp:
+
+
+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)