Split higherhit into multiple files

diff --git a/examples/higherhit.ctt b/examples/higherhit.ctt
deleted file mode 100644 (file)
index 4a501a5..0000000
--- a/examples/higherhit.ctt
+++ /dev/null
@@ -1,60 +0,0 @@
-module higherhit where
-
-import prelude
-
--- Some experiments with higher HITs.
-
--- old stuff looks now like this
-
-data S1 = base
-        | loop <i> [(i=0) -> base, (i=1) -> base]
-
-
-foo : S1 = base
-
-loop' : Id S1 base base = <i> loop {S1} @ i
-
-
--- new
-
-data S2 = base
-        | loop2 <i j> [ (i=0) -> base
-                      , (i=1) -> base
-                      , (j=0) -> base
-                      , (j=1) -> base]
-
-loop2' : Id (Id S2 base base) (refl S2 base) (refl S2 base) =
-  <i j> loop2 {S2} @ i @ j
-
-data Torus = ptT
-           | pathOneT <i> [ (i=0) -> ptT, (i=1) -> ptT ]
-           | pathTwoT <i> [ (i=0) -> ptT, (i=1) -> ptT ]
-           | squareT <i j> [ (i=0) -> pathOneT {Torus} @ j
-                           , (i=1) -> pathOneT {Torus} @ j
-                           , (j=0) -> pathTwoT {Torus} @ i
-                           , (j=1) -> pathTwoT {Torus} @ i ]
-
-data setTrunc (A : U)
-  = inc (a : A)
-  | setTr (a b : setTrunc A) (p q : Id (setTrunc A) a b) <i j>
-       [ (i=0) -> p @ j
-       , (i=1) -> q @ j
-       , (j=0) -> a
-       , (j=1) -> b]
-
-setTruncSet (A : U) : set (setTrunc A) =
-   \(a b : setTrunc A) (p q : Id (setTrunc A) a b) ->
-     <i j> setTr {setTrunc A} a b p q @ i @ j
-
-
-setTruncRec (A : U)
-            (B : U)
-            (bS : set B)
-            (f : A -> B) :
-            setTrunc A -> B =
-  split
-    inc a -> f a
-    setTr a b p q @ i j -> (bS (setTruncRec A B bS f a)
-                               (setTruncRec A B bS f b)
-                               (<k> setTruncRec A B bS f (p @ k))
-                               (<k> setTruncRec A B bS f (q @ k))) @ i @ j

diff --git a/examples/s2.ctt b/examples/s2.ctt
new file mode 100644 (file)
index 0000000..359ddf9
--- /dev/null
+++ b/examples/s2.ctt
@@ -0,0 +1,12 @@
+module s2 where
+
+import prelude
+
+data S2 = base
+        | loop2 <i j> [ (i=0) -> base
+                      , (i=1) -> base
+                      , (j=0) -> base
+                      , (j=1) -> base]
+
+loop2' : Id (Id S2 base base) (refl S2 base) (refl S2 base) =
+  <i j> loop2 {S2} @ i @ j

diff --git a/examples/setTrunc.ctt b/examples/setTrunc.ctt
new file mode 100644 (file)
index 0000000..bd34fba
--- /dev/null
+++ b/examples/setTrunc.ctt
@@ -0,0 +1,28 @@
+module setTrunc where
+
+import prelude
+
+data setTrunc (A : U)
+  = inc (a : A)
+  | setTr (a b : setTrunc A) (p q : Id (setTrunc A) a b) <i j>
+       [ (i=0) -> p @ j
+       , (i=1) -> q @ j
+       , (j=0) -> a
+       , (j=1) -> b]
+
+setTruncSet (A : U) : set (setTrunc A) =
+   \(a b : setTrunc A) (p q : Id (setTrunc A) a b) ->
+     <i j> setTr {setTrunc A} a b p q @ i @ j
+
+
+setTruncRec (A : U)
+            (B : U)
+            (bS : set B)
+            (f : A -> B) :
+            setTrunc A -> B =
+  split
+    inc a -> f a
+    setTr a b p q @ i j -> (bS (setTruncRec A B bS f a)
+                               (setTruncRec A B bS f b)
+                               (<k> setTruncRec A B bS f (p @ k))
+                               (<k> setTruncRec A B bS f (q @ k))) @ i @ j

diff --git a/examples/torus.ctt b/examples/torus.ctt
new file mode 100644 (file)
index 0000000..1300a27
--- /dev/null
+++ b/examples/torus.ctt
@@ -0,0 +1,11 @@
+module torus where
+
+import prelude
+
+data Torus = ptT
+           | pathOneT <i> [ (i=0) -> ptT, (i=1) -> ptT ]
+           | pathTwoT <i> [ (i=0) -> ptT, (i=1) -> ptT ]
+           | squareT <i j> [ (i=0) -> pathOneT {Torus} @ j
+                           , (i=1) -> pathOneT {Torus} @ j
+                           , (j=0) -> pathTwoT {Torus} @ i
+                           , (j=1) -> pathTwoT {Torus} @ i ]