Clean examples

diff --git a/examples/bool.ctt b/examples/bool.ctt
index 12469e227665d48891c99ed592b3a81235d42632..dbbcab8c2e8cd53728bc5216eabc6f11d5e5ef89 100644 (file)
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -1,7 +1,6 @@
 module bool where
 
 import prelude
-import nat
 
 data bool = false | true
 
@@ -18,37 +17,34 @@ negEq : Id U bool bool =
 
 test : bool = transport negEq true
 
-data F2 = zero | one
+data F2 = zeroF2 | oneF2
 
 f2ToBool : F2 -> bool = split
-  zero -> false
-  one -> true
+  zeroF2 -> false
+  oneF2 -> true
 
 boolToF2 : bool -> F2 = split
-  false -> zero
-  true -> one
+  false -> zeroF2
+  true -> oneF2
 
 f2ToBoolK : (x : F2) -> Id F2 (boolToF2 (f2ToBool x)) x = split
-  zero -> refl F2 zero
-  one -> refl F2 one
+  zeroF2 -> refl F2 zeroF2
+  oneF2 -> refl F2 oneF2
 
 boolToF2K : (b : bool) -> Id bool (f2ToBool (boolToF2 b)) b = split
   false -> refl bool false
   true -> refl bool true
 
 boolEqF2 : Id U bool F2 =
- -- <i> glue F2 [ (i = 0) -> (bool,(boolToF2,(f2ToBool,(f2ToBoolK,boolToF2K))))]
  isoId bool F2 boolToF2 f2ToBool f2ToBoolK boolToF2K
   
 negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 neg
 
-
 lemTest (A : U) : (B : U) (p : Id U A B) (a : A) -> IdP p a (transport p a) =
   J U A (\(B : U) (p : Id U A B) -> (a : A) -> IdP p a (transport p a)) (refl A)
 
-
-test : IdP boolEqF2 true one = <i> glueElem one [ (i = 0) -> true ]
-test1 : IdP boolEqF2 true one = lemTest bool F2 boolEqF2 true
+test : IdP boolEqF2 true oneF2 = <i> glueElem oneF2 [ (i = 0) -> true ]
+test1 : IdP boolEqF2 true oneF2 = lemTest bool F2 boolEqF2 true
 
 F2EqBool : Id U F2 bool = inv U bool F2 boolEqF2
 
@@ -57,28 +53,22 @@ negBool : bool -> bool = subst U (\(X : U) -> (X -> X)) F2 bool F2EqBool negF2
 F2EqBoolComp : Id U F2 bool =
   compId U F2 bool bool F2EqBool negEq
 
-test2 : bool = transport F2EqBoolComp one
+test2 : bool = transport F2EqBoolComp oneF2
 
 negNegEq : Id U bool bool =
   compId U bool bool bool negEq negEq
 
-
 test3 : bool = transport negNegEq true
-
 test4 : Id U bool bool = <i> negNegEq @ i
 
 kanBool : Id U bool bool =
   kan U bool bool bool bool negEq negEq negEq
 
--- connectSquare (A : U) (a0 a1 : A) (u : Id A a0 a1)
---               (b0 b1 : A) (v : Id A b0 b1)
---               (r0 : Id A a0 b0) (r1 : Id A a1 b1) : Square A a0 a1 u b0 b1 v r0 r1= 
-
 squareBoolF2 : Square U bool bool (refl U bool) bool F2
                   boolEqF2 (refl U bool)  boolEqF2 =
   <i j> boolEqF2 @ i /\ j
 
-test5 : IdP boolEqF2 true one = 
+test5 : IdP boolEqF2 true oneF2 = 
   <i> transport (<j> boolEqF2 @ i /\ j) true
 
 test6 : Id bool true true =

diff --git a/examples/interval.ctt b/examples/interval.ctt
index 01c49e6858b0782f9e554e65be153aaafd73b339..ee1f108c16d3a90c626eb278cc9f633567f6cfb0 100644 (file)
--- a/examples/interval.ctt
+++ b/examples/interval.ctt
@@ -5,8 +5,7 @@ import prelude
 data I = zero | one | seg @ zero ~ one
 
 fext (A B : U) (f g : A -> B) (p : (x : A) -> Id B (f x) (g x)) :
-     Id (A -> B) f g = mapOnPath I (A -> B) (\(i : I) (x : A) -> htpy x i)
-                          zero one (<i> seg{I} @ i)
+     Id (A -> B) f g = <j> (\(x : A) -> htpy x (seg{I} @ j))
   where htpy (x : A) : I -> B = split
           zero    -> f x
           one     -> g x

diff --git a/examples/list.ctt b/examples/list.ctt
new file mode 100644 (file)
index 0000000..1073d10
--- /dev/null
+++ b/examples/list.ctt
@@ -0,0 +1,11 @@
+module list where
+
+data list (A : U) = nil | cons (a : A) (as : list A)
+
+append (A : U) : list A -> list A -> list A = split
+  nil -> id (list A)
+  cons x xs -> \(ys : list A) -> cons x (append A xs ys)
+
+reverse (A : U) : list A -> list A = split
+  nil -> nil
+  cons x xs -> append A (reverse A xs) (cons x nil)

diff --git a/examples/nat.ctt b/examples/nat.ctt
index 321a0a6e450bf36ab4c76891ade09cfbbd11c3bd..a3a7be4e39e4543aa8a0208f37b31bad9ca961c9 100644 (file)
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -4,7 +4,6 @@ import prelude
 
 data nat = zero | suc (n : nat)
 
-zero' : nat = zero
 one : nat = suc zero
 two : nat = suc one
 
@@ -23,64 +22,12 @@ add' : nat -> nat -> nat = split
 sucInj (n m : nat) (p : Id nat (suc n) (suc m)) : Id nat n m =
  <i> pred (p @ i)
 
--- TODO: Clean the rest of this file!
-
-id (A : U) (a : A) : A = a
-
-data list (A : U) = nil | cons (a : A) (as : list A)
-
-l : list nat = cons one (cons two nil)
-
-append (A : U) : list A -> list A -> list A = split
-  nil -> id (list A)
-  cons x xs -> \(ys : list A) -> cons x (append A xs ys)
-
-reverse (A : U) : list A -> list A = split
-  nil -> nil
-  cons x xs -> append A (reverse A xs) (cons x nil)
-
 idnat : nat -> nat = split
   zero -> zero
   suc n -> suc (idnat n)
 
-test : Id (nat -> nat) idnat (id nat) = funExt nat (\(_ : nat) -> nat) idnat (id nat) rem
+test : Id (nat -> nat) idnat (idfun nat) = funExt nat (\(_ : nat) -> nat) idnat (idfun nat) rem
   where
   rem : (n : nat) -> Id nat (idnat n) n = split
     zero -> refl nat zero
     suc n -> mapOnPath nat nat (\(x : nat) -> suc x) (idnat n) n (rem n)
-
-test0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0)
-test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1)
-
-compEmpty (A : U) (a b : A) (p : Id A a b) : Id A a b =
-  <i> comp A (p @ i) [ ]
-
-kan (A : U) (a b c d : A) (p : Id A a b) (q : Id A a c)
-                          (r : Id A b d) : Id A c d =
-  <i> comp A (p @ i) [ (i = 0) -> q, (i = 1) -> r ]
-
-
--- lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c)
---          (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : Id (Id A b c) q q' =
---   <j> <k> comp A a [ (j = 0) -> ... ]
-
--- evalPN (i:j:k:_) LemSimpl [v,a,b,c,p,q,q',s] =
---   Path j $ Path k $ comp Pos i v ss a
---    where ss = mkSystem [(j ~> 0,fill Pos k v (mkSystem [(i ~> 0,a),(i ~> 1,q @@ j)]) (p @@ i)),
---                         (j ~> 1,fill Pos k v (mkSystem [(i ~> 0,a),(i ~> 1,(q' @@ j))]) (p @@ i)),
---                         (k ~> 0,p @@ i),
---                         (k ~> 1,(s @@ j) @@ i)]
-
-test (A : U) (a b : A) (p : Id A a b) : Id A a a =
-  <i> p @ (i /\ -i)
-
--- testRefl (A : U) (a b : A) (p : Id A a b) : Id (Id A a a) (test A a b p) (refl A a) =
---   <i j> fill j A a [ (i=0) -> p  @ (i /\ -i) ]
-
-
-lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c)
-          (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : Id (Id A b c) q q' =
-  <j> <k> comp A a [ (j = 0) -> <i> comp A (p @ i) [ (i = 1) -> <l> q @ k /\ l],
-                     (j = 1) -> <i> comp A (p @ i) [ (i=1) -> <l> q' @ k /\ l],
-                     (k = 0)  -> p,
-                     (k = 1)  -> s @ j ]

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index c2d7f9a62e14f8076f5db5d2ce55c8027a4fc73b..6e749f1c74272c5ac1ed365ab08bf316c4d139de 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -51,6 +51,25 @@ compDown (A : U) (a a' b b' : A)
          (p : Id A a a') (q: Id A b b') : Id A a' b' -> Id A a b =
  compUp A a' a b' b (inv A a a' p) (inv A b b' q)
 
+idfun (A : U) (a : A) : A = a
+
+test0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0)
+test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1)
+
+compEmpty (A : U) (a b : A) (p : Id A a b) : Id A a b =
+  <i> comp A (p @ i) [ ]
+
+kan (A : U) (a b c d : A) (p : Id A a b) (q : Id A a c)
+                          (r : Id A b d) : Id A c d =
+  <i> comp A (p @ i) [ (i = 0) -> q, (i = 1) -> r ]
+
+lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c)
+          (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : Id (Id A b c) q q' =
+  <j> <k> comp A a [ (j = 0) -> <i> comp A (p @ i) [ (i = 1) -> <l> q @ k /\ l],
+                     (j = 1) -> <i> comp A (p @ i) [ (i=1) -> <l> q' @ k /\ l],
+                     (k = 0)  -> p,
+                     (k = 1)  -> s @ j ]
+
 isoId (A B : U) (f : A -> B) (g : B -> A)
       (s : (y:B) -> Id B (f (g y)) y)
       (t : (x:A) -> Id A (g (f x)) x) : Id U A B =

diff --git a/examples/susp.ctt b/examples/susp.ctt
index 905cbc954e9fcbb198412990e140815d9469bffe..161141dd1348d9ea2adf41bb1a5338ddc6701db3 100644 (file)
--- a/examples/susp.ctt
+++ b/examples/susp.ctt
@@ -1,6 +1,5 @@
 module susp where\r
 \r
--- import helix\r
 import circle\r
 \r
 data susp (A:U) = north | south | merid (a:A) @ north ~ south\r
@@ -12,8 +11,6 @@ sphere : nat -> U = split
 \r
 -- The circle (S1) is equal to the 1-sphere (aka the suspension of Bool).\r
 -- (Similar to HoTT Book, Lemma 6.5.1)\r
-one : nat = suc zero\r
-\r
 sone : U = sphere one\r
 \r
 s1ToCircle : sone -> S1 = split\r