Cleaning

diff --git a/examples/hedberg.ctt b/examples/hedberg.ctt
index a9443f369c0c5a280d2bc897433a2f2325fefd84..e1a60c60b4dbf9a541277ed10cd3406962dd2cdb 100644 (file)
--- a/examples/hedberg.ctt
+++ b/examples/hedberg.ctt
@@ -10,13 +10,6 @@ decEqCong (A B : U) (f : A -> B) (g : B -> A) : dec A -> dec B = split
   inl a -> inl (f a)\r
   inr h -> inr (\ (b:B) -> h (g b))\r
 \r
-pred : nat -> nat = split\r
-  zero  -> zero\r
-  suc n -> n\r
-\r
-sucInj (n m : nat) (p:Id nat (suc n) (suc m)) : Id nat n m = \r
- <i> pred (p @ i)\r
-\r
 caseNat (A:U) (a0 aS : A) : nat -> A = split\r
  zero -> a0\r
  suc n -> aS\r
@@ -38,11 +31,7 @@ natDec : (n m:nat) -> dec (Id nat n m) = split
    (\ (m:nat) -> decEqCong (Id nat n m) (Id nat (suc n) (suc m)) (\ (p:Id nat n m) -> <i> suc (p @ i))\r
                  (sucInj n m) (natDec n m))\r
 \r
-prop (A:U) : U = (a b:A) -> Id A a b\r
-\r
-set (A:U) : U = (a b:A) -> prop (Id A a b)\r
-\r
-exConst (A : U) :U = (f:A -> A) * const A f\r
+exConst (A : U) : U = (f:A -> A) * const A f\r
 \r
 decConst (A : U) : dec A -> exConst A = split\r
   inl a -> (\ (x:A)  -> a, \ (x y:A) -> refl A a)\r
@@ -54,14 +43,6 @@ hedbergLemma (A: U) (f : (a b : A) -> Id A a b -> Id A a b) (a :A) :
   J A a (\ (b:A) (p:Id A a b) -> Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p)) \r
     (refl (Id A a a) (f a a (refl A a)))\r
 \r
-compUp (A : U) (a a' b b' : A) \r
-       (p : Id A a a') (q: Id A b b') (r:Id A a b) : Id A a' b' =\r
- <i> comp A (r@i) [(i=0) -> p, (i=1) -> q]\r
-\r
-compDown (A : U) (a a' b b' : A) \r
-         (p : Id A a a') (q: Id A b b') : Id A a' b' -> Id A a b =\r
- compUp A a' a b' b (inv A a a' p) (inv A b b' q)\r
-\r
 hedberg (A : U) (h:discrete A) (a b :A) (p q:Id A a b) : Id (Id A a b) p q = \r
    lemSimpl A a a b r p q rem5\r
   where\r

diff --git a/examples/nat.ctt b/examples/nat.ctt
index 1b2153515d6f4be76fa302023286c5baa5671569..321a0a6e450bf36ab4c76891ade09cfbbd11c3bd 100644 (file)
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -20,6 +20,11 @@ add' : nat -> nat -> nat = split
   zero -> \(x : nat) -> x
   suc n -> \(x : nat) -> suc (add' n x)
 
+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)
@@ -79,4 +84,3 @@ lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c)
                      (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 f772009ad8e04247b14eb80610b89716289a29e5..c2d7f9a62e14f8076f5db5d2ce55c8027a4fc73b 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -42,7 +42,15 @@ compId' (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c =
 compId'' (A : U) (a b : A) (p : Id A a b) : (c : A) -> (q : Id A b c) -> Id A a c =
   J A a ( \ (b : A) (p : Id A a b) -> (c : A) -> (q : Id A b c) -> Id A a c) rem b p
     where rem (c : A) (p : Id A a c) : Id A a c = p
-  
+
+compUp (A : U) (a a' b b' : A)
+       (p : Id A a a') (q : Id A b b') (r : Id A a b) : Id A a' b' =
+  <i> comp A (r @ i) [(i = 0) -> p, (i = 1) -> q]
+
+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)
+
 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/retract.ctt b/examples/retract.ctt
index 66a0bb8cf4f40d41467bcea0603149c80266cc13..34d3559c760933197035f5f85b4e3775d5478cf3 100644 (file)
--- a/examples/retract.ctt
+++ b/examples/retract.ctt
@@ -1,8 +1,6 @@
 module retract where\r
 \r
 import prelude\r
-import hedberg\r
-\r
 \r
 section (A B : U) (f : A -> B) (g : B -> A) :U = (b : B) -> Id B (f (g b)) b\r
 \r