removed some examples (to be updated)

diff --git a/examples/booltest.ctt b/examples/booltest.ctt
deleted file mode 100644 (file)
index 3d20e99..0000000
--- a/examples/booltest.ctt
+++ /dev/null
@@ -1,32 +0,0 @@
-module booltest where
-
-import bool
-import newhedberg
-
-falseNotTrue (h : Id bool false true) : N0 = transport (<i> T (h @ i)) tt
-  where T : bool -> U = split
-    false -> Unit
-    true  -> N0
-
-trueNotFalse (h : Id bool true false) : N0 = falseNotTrue (<i> h @ - i)
-
-lemFalse : (b : bool) -> dec (Id bool false b) = split
-  false -> inl (<i> false)
-  true -> inr falseNotTrue
-
-lemTrue : (b : bool) -> dec (Id bool true b) = split
-  false -> inr trueNotFalse
-  true -> inl (<i> true)
-
-boolDec : (a b : bool) -> dec (Id bool a b) = split
-  false -> lemFalse
-  true -> lemTrue
-
-boolSet : set bool = corrhedberg bool boolDec
-
-F2Set : set F2 = subst U set bool F2 boolEqF2 boolSet
-
-T : U = Id F2 oneF2 oneF2
-p0 : T = refl F2 oneF2
-
-test : Id T p0 p0 = F2Set oneF2 oneF2 p0 p0
\ No newline at end of file

diff --git a/examples/list.ctt b/examples/list.ctt
index da6b6ce50813abc6afcb1460ec166ccb1d23f3f0..cba3326f8de61ba4cf0749c60715af948bda44be 100644 (file)
--- a/examples/list.ctt
+++ b/examples/list.ctt
@@ -39,6 +39,8 @@ assoc (A:U) : (xs ys zs : list A) -> Id (list A) (append A (append A xs ys) zs)
  nil -> \ (ys zs:list A) -> <i>append A ys zs
  cons x xs -> \ (ys zs:list A) -> <i>cons x (assoc A xs ys zs@i)
 
+{-
+
 lem4 (A:U) : (xs ys:list A) -> Id (list A) (reverse A (append A xs ys)) (append A (reverse A ys) (reverse A xs)) = split
  nil -> \ (ys:list A) -> <i>lem2 A (reverse A ys)@-i
  cons x xs -> \ (ys:list A) -> <i>comp (list A) (append A (lem4 A xs ys@i) (cons x nil))
@@ -48,3 +50,4 @@ lem5 (A:U) : (xs:list A) -> Id (list A) (reverse A (reverse A xs)) xs = split
  nil -> <i>nil
  cons x xs -> <i>comp (list A) (lem4 A (reverse A xs) (cons x nil)@i) [(i=1) -> <j>cons x (lem5 A xs@j)]
 
+-}

diff --git a/examples/deppath.ctt b/experiments/deppath.ctt
similarity index 100%
rename from examples/deppath.ctt
rename to experiments/deppath.ctt

diff --git a/examples/exchange.ctt b/experiments/exchange.ctt
similarity index 100%
rename from examples/exchange.ctt
rename to experiments/exchange.ctt

diff --git a/examples/helix.ctt b/experiments/helix.ctt
similarity index 100%
rename from examples/helix.ctt
rename to experiments/helix.ctt

diff --git a/examples/hopf.ctt b/experiments/hopf.ctt
similarity index 100%
rename from examples/hopf.ctt
rename to experiments/hopf.ctt

diff --git a/examples/join.ctt b/experiments/join.ctt
similarity index 100%
rename from examples/join.ctt
rename to experiments/join.ctt

diff --git a/examples/mystery.ctt b/experiments/mystery.ctt
similarity index 100%
rename from examples/mystery.ctt
rename to experiments/mystery.ctt

diff --git a/examples/other.ctt b/experiments/other.ctt
similarity index 100%
rename from examples/other.ctt
rename to experiments/other.ctt

diff --git a/examples/pi1S2output.ctt b/experiments/pi1S2output.ctt
similarity index 100%
rename from examples/pi1S2output.ctt
rename to experiments/pi1S2output.ctt

diff --git a/examples/pi1s2.ctt b/experiments/pi1s2.ctt
similarity index 100%
rename from examples/pi1s2.ctt
rename to experiments/pi1s2.ctt

diff --git a/examples/pi4s3.ctt b/experiments/pi4s3.ctt
similarity index 100%
rename from examples/pi4s3.ctt
rename to experiments/pi4s3.ctt

diff --git a/examples/pointed.ctt b/experiments/pointed.ctt
similarity index 100%
rename from examples/pointed.ctt
rename to experiments/pointed.ctt

diff --git a/examples/s2.ctt b/experiments/s2.ctt
similarity index 100%
rename from examples/s2.ctt
rename to experiments/s2.ctt

diff --git a/examples/set.ctt b/experiments/set.ctt
similarity index 100%
rename from examples/set.ctt
rename to experiments/set.ctt

diff --git a/examples/setTrunc.ctt b/experiments/setTrunc.ctt
similarity index 100%
rename from examples/setTrunc.ctt
rename to experiments/setTrunc.ctt

diff --git a/examples/testall.ctt b/experiments/testall.ctt
similarity index 100%
rename from examples/testall.ctt
rename to experiments/testall.ctt

diff --git a/examples/thm7312.ctt b/experiments/thm7312.ctt
similarity index 100%
rename from examples/thm7312.ctt
rename to experiments/thm7312.ctt

diff --git a/examples/torus.ctt b/experiments/torus.ctt
similarity index 100%
rename from examples/torus.ctt
rename to experiments/torus.ctt

diff --git a/examples/truncS2.ctt b/experiments/truncS2.ctt
similarity index 100%
rename from examples/truncS2.ctt
rename to experiments/truncS2.ctt

diff --git a/examples/uafunext1.ctt b/experiments/uafunext1.ctt
similarity index 100%
rename from examples/uafunext1.ctt
rename to experiments/uafunext1.ctt

diff --git a/examples/uafunext2.ctt b/experiments/uafunext2.ctt
similarity index 100%
rename from examples/uafunext2.ctt
rename to experiments/uafunext2.ctt