From: Anders <mortberg@chalmers.se>
Date: Wed, 8 Apr 2015 10:27:59 +0000 (+0200)
Subject: Cleaning
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=d44d48c411732b8d03c28e6a504472123c6f6659;p=cubicaltt.git

Cleaning
---

diff --git a/examples/hedberg.ctt b/examples/hedberg.ctt
index a9443f3..e1a60c6 100644
--- 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)
   inr h -> inr (\ (b:B) -> h (g b))
 
-pred : nat -> nat = split
-  zero  -> zero
-  suc n -> n
-
-sucInj (n m : nat) (p:Id nat (suc n) (suc m)) : Id nat n m = 
- <i> pred (p @ i)
-
 caseNat (A:U) (a0 aS : A) : nat -> A = split
  zero -> a0
  suc n -> aS
@@ -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))
                  (sucInj n m) (natDec n m))
 
-prop (A:U) : U = (a b:A) -> Id A a b
-
-set (A:U) : U = (a b:A) -> prop (Id A a b)
-
-exConst (A : U) :U = (f:A -> A) * const A f
+exConst (A : U) : U = (f:A -> A) * const A f
 
 decConst (A : U) : dec A -> exConst A = split
   inl a -> (\ (x:A)  -> a, \ (x y:A) -> refl A a)
@@ -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)) 
     (refl (Id A a a) (f a a (refl A a)))
 
-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)
-
 hedberg (A : U) (h:discrete A) (a b :A) (p q:Id A a b) : Id (Id A a b) p q = 
    lemSimpl A a a b r p q rem5
   where
diff --git a/examples/nat.ctt b/examples/nat.ctt
index 1b21535..321a0a6 100644
--- 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 f772009..c2d7f9a 100644
--- 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 66a0bb8..34d3559 100644
--- a/examples/retract.ctt
+++ b/examples/retract.ctt
@@ -1,8 +1,6 @@
 module retract where
 
 import prelude
-import hedberg
-
 
 section (A B : U) (f : A -> B) (g : B -> A) :U = (b : B) -> Id B (f (g b)) b