Lots of cleaning in the examples

diff --git a/examples/bool.ctt b/examples/bool.ctt
index dbbcab8c2e8cd53728bc5216eabc6f11d5e5ef89..f94af65514c3905122ec0965b99f6f56a46e2d3e 100644 (file)
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -4,18 +4,18 @@ import prelude
 
 data bool = false | true
 
-neg : bool -> bool = split
+negBool : bool -> bool = split
   false -> true
   true  -> false
 
-negK : (b : bool) -> Id bool (neg (neg b)) b = split
+negBoolK : (b : bool) -> Id bool (negBool (negBool b)) b = split
   false -> refl bool false
   true -> refl bool true
 
-negEq : Id U bool bool =
-  <i> glue bool [ (i = 0) -> (bool,neg,neg,negK,negK) ]
+negBoolEq : Id U bool bool =
+  <i> glue bool [ (i = 0) -> (bool,negBool,negBool,negBoolK,negBoolK) ]
 
-test : bool = transport negEq true
+test : bool = transport negBoolEq true
 
 data F2 = zeroF2 | oneF2
 
@@ -38,7 +38,7 @@ boolToF2K : (b : bool) -> Id bool (f2ToBool (boolToF2 b)) b = split
 boolEqF2 : Id U bool F2 =
  isoId bool F2 boolToF2 f2ToBool f2ToBoolK boolToF2K
   
-negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 neg
+negF2 : F2 -> F2 = subst U (\(X : U) -> (X -> X)) bool F2 boolEqF2 negBool
 
 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)
@@ -48,21 +48,21 @@ test1 : IdP boolEqF2 true oneF2 = lemTest bool F2 boolEqF2 true
 
 F2EqBool : Id U F2 bool = inv U bool F2 boolEqF2
 
-negBool : bool -> bool = subst U (\(X : U) -> (X -> X)) F2 bool F2EqBool negF2
+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
+  compId U F2 bool bool F2EqBool negBoolEq
 
 test2 : bool = transport F2EqBoolComp oneF2
 
 negNegEq : Id U bool bool =
-  compId U bool bool bool negEq negEq
+  compId U bool bool bool negBoolEq negBoolEq
 
 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
+  kan U bool bool bool bool negBoolEq negBoolEq negBoolEq
 
 squareBoolF2 : Square U bool bool (refl U bool) bool F2
                   boolEqF2 (refl U bool)  boolEqF2 =

diff --git a/examples/circle.ctt b/examples/circle.ctt
index d7a0a17a248d5b3e1dcbd5b838b95621088d5b7c..758e41225c08d013f18dfc2eca832e88fce89d6f 100644 (file)
--- a/examples/circle.ctt
+++ b/examples/circle.ctt
@@ -1,34 +1,39 @@
 module circle where
 
 import bool
-import integer
+import int
 
-data S1 = base | loop @ base ~ base
+data S1 = base
+        | loop @ base ~ base
+
+loopS1 : U = Id S1 base base
+
+loop1 : Id S1 base base = <i> loop{S1} @ i
+
+invLoop : loopS1 = inv S1 base base loop1
 
 moebius : S1 -> U = split
   base -> bool
-  loop @ i -> negEq @ i
-
-loop' : Id S1 base base = <i> loop{S1} @ i
+  loop @ i -> negBoolEq @ i
 
 helix : S1 -> U = split
   base -> Z
   loop @ i -> sucIdZ @ i
 
-loopS1 : U = Id S1 base base 
-
 winding (p : loopS1) : Z = transport rem zeroZ
   where
     rem : Id U Z Z = <i> helix (p @ i)
 
+compS1 : loopS1 -> loopS1 -> loopS1 = compId S1 base base base
+
 -- All of these should be equal to "posZ (suc zero)":
-loop2 : loopS1 = compId S1 base base base loop' loop'
-loop2' : loopS1 = compId' S1 base base base loop' loop'
-loop2'' : loopS1 = compId'' S1 base base loop' base loop'
+loop2 : loopS1 = compS1 loop1 loop1
+loop2' : loopS1 = compId' S1 base base base loop1 loop1
+loop2'' : loopS1 = compId'' S1 base base loop1 base loop1
 
 mLoop : (x : S1) -> Id S1 x x = split
-  base -> loop'
-  loop @ i -> (constSquare S1 base loop') @ i
+  base -> loop1
+  loop @ i -> (constSquare S1 base loop1) @ i
 
 mult (x : S1) : S1 -> S1 = split
   base -> x

diff --git a/examples/discor.ctt b/examples/discor.ctt
index ecfc66519ffc8c025db42fe8c5dd56883d01cfa5..e983ff1287d7a279d8a47b1c9cfa560ff42cadf1 100644 (file)
--- a/examples/discor.ctt
+++ b/examples/discor.ctt
@@ -2,20 +2,6 @@ module discor where
 \r
 import prelude\r
 \r
-data or (A B:U) = inl (a:A) | inr (b:B)\r
-\r
-data Unit = tt\r
-\r
-data N0 = \r
-\r
-efq (A:U) : N0 -> A = split{}\r
-\r
-neg (A:U) : U = A -> N0\r
-\r
-dec (A:U) : U = or A (neg A)\r
-\r
-discrete (A:U) : U = (a b:A) -> dec (Id A a b)\r
-\r
 inlNotinr (A B:U) (a:A) (b:B) (h: Id (or A B) (inl a) (inr b)) : N0 = \r
  subst (or A B) T (inl a) (inr b) h tt\r
  where\r
@@ -30,8 +16,6 @@ inrNotinl (A B:U) (a:A) (b:B) (h : Id (or A B) (inr b) (inl a)) : N0 =
        inl _ -> N0\r
        inr _ -> Unit\r
 \r
-injective (A B:U) (f:A->B) : U = (a0 a1:A) -> Id B (f a0) (f a1) -> Id A a0 a1\r
-\r
 injInl (A B :U) (x0 x1:A) (h : Id (or A B) (inl x0) (inl x1)) : Id A x0 x1 = \r
  subst (or A B) T (inl x0) (inl x1) h (refl A x0)\r
  where\r
@@ -46,7 +30,9 @@ injInr (A B :U) (x0 x1:B) (h: Id (or A B) (inr x0) (inr x1)) : Id B x0 x1 =
          inl _ -> N0\r
          inr x -> Id B x0 x\r
 \r
-orDisc (A B : U) (dA: discrete A) (dB: discrete B) : (z z1 : or A B) -> dec (Id (or A B) z z1) = split\r
+-- If A and B are discrete then "A or B" is discrete\r
+orDisc (A B : U) (dA : discrete A) (dB : discrete B) :\r
+  (z z1 : or A B) -> dec (Id (or A B) z z1) = split\r
   inl a -> rem1\r
     where rem1 : (z1:or A B) -> dec (Id (or A B) (inl a) z1) = split\r
             inl a1 -> rem (dA a a1)\r

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index 5e325175b3ce79f001f68e441089bc1124c15557..d1d860a4d7c3e73ed225a2ac605fc99ba41918a7 100644 (file)
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -2,8 +2,6 @@ module equiv where
 \r
 import prelude\r
 \r
-and (A B:U) :U = (_:A) * B\r
-\r
 contr (A:U) : U = (_:A) * prop A\r
 \r
 isContr (A : U) : U = and (prop A) A\r

diff --git a/examples/hedberg.ctt b/examples/hedberg.ctt
index e1a60c60b4dbf9a541277ed10cd3406962dd2cdb..9db5b1d9bc954088b288090b2e5396393656f829 100644 (file)
--- a/examples/hedberg.ctt
+++ b/examples/hedberg.ctt
@@ -1,8 +1,6 @@
 module hedberg where\r
 \r
-import bool\r
-import discor\r
-import int\r
+import prelude\r
 \r
 const (A : U) (f : A -> A) : U = (x y : A) -> Id A (f x) (f y)\r
 \r
@@ -10,60 +8,34 @@ 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
-caseNat (A:U) (a0 aS : A) : nat -> A = split\r
- zero -> a0\r
- suc n -> aS\r
-\r
-caseDNat (P:nat -> U) (a0 :P zero) (aS : (n:nat) -> P (suc n)) \r
-            : (n:nat) -> P n = split\r
- zero -> a0\r
- suc n -> aS n\r
-\r
-znots (n : nat) : neg (Id nat zero (suc n)) =\r
- \ (h:Id nat zero (suc n)) -> subst nat (caseNat U nat N0) zero (suc n) h zero\r
-\r
-snotz (n : nat) : neg (Id nat (suc n) zero) =\r
- \ (h:Id nat (suc n) zero) -> znots n (inv nat (suc n) zero h)\r
-\r
-natDec : (n m:nat) -> dec (Id nat n m) = split\r
- zero -> caseDNat (\ (m:nat) -> dec (Id nat zero m)) (inl (refl nat zero)) (\ (m:nat) -> inr (znots m))\r
- suc n -> caseDNat (\ (m:nat) -> dec (Id nat (suc n) m)) (inr (snotz n))\r
-   (\ (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
 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
   inr h -> (\ (x:A) -> x, \ (x y:A) -> efq (Id A x y) (h x))\r
 \r
-hedbergLemma (A: U) (f : (a b : A) -> Id A a b -> Id A a b) (a :A) : \r
+hedbergLemma (A: U) (f : (a b : A) -> Id A a b -> Id A a b) (a :A) :\r
   (b : A) (p : Id A a b) ->\r
-            Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p) = \r
-  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
+            Id (Id A a b) (compId A a a b (f a a (refl A a)) p) (f a b p) =\r
+  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
-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
-    rem1 (x y : A) : exConst (Id A x y) = decConst (Id A x y) (h x y)\r
-\r
-    f (x y : A) : Id A x y -> Id A x y = (rem1 x y).1\r
-\r
-    fIsConst (x y : A) : const (Id A x y) (f x y) = (rem1 x y).2\r
+hedberg (A : U) (h : discrete A) : set A = \(a b : A) (p q : Id A a b) ->\r
+   let rem1 (x y : A) : exConst (Id A x y) = decConst (Id A x y) (h x y)\r
 \r
-    r : Id A a a = f a a (refl A a)\r
+       f (x y : A) : Id A x y -> Id A x y = (rem1 x y).1\r
 \r
-    rem2 : Id (Id A a b) (compId A a a b r p) (f a b p) = hedbergLemma A f a b p\r
+       fIsConst (x y : A) : const (Id A x y) (f x y) = (rem1 x y).2\r
 \r
-    rem3 : Id (Id A a b) (compId A a a b r q) (f a b q) = hedbergLemma A f a b q\r
+       r : Id A a a = f a a (refl A a)\r
 \r
-    rem4 : Id (Id A a b) (f a b p) (f a b q) = fIsConst a b p q\r
+       rem2 : Id (Id A a b) (compId A a a b r p) (f a b p) = hedbergLemma A f a b p\r
 \r
-    rem5 : Id (Id A a b) (compId A a a b r p) (compId A a a b r q) = \r
-     compDown (Id A a b) (compId A a a b r p) (f a b p) (compId A a a b r q)\r
-                (f a b q) rem2 rem3 rem4\r
+       rem3 : Id (Id A a b) (compId A a a b r q) (f a b q) = hedbergLemma A f a b q\r
 \r
-natSet : set nat = hedberg nat natDec\r
+       rem4 : Id (Id A a b) (f a b p) (f a b q) = fIsConst a b p q\r
 \r
-ZSet : set Z = hedberg Z (orDisc nat nat natDec natDec)
\ No newline at end of file
+       rem5 : Id (Id A a b) (compId A a a b r p) (compId A a a b r q) =\r
+         compDown (Id A a b) (compId A a a b r p) (f a b p) (compId A a a b r q)\r
+                  (f a b q) rem2 rem3 rem4\r
+  in lemSimpl A a a b r p q rem5\r

diff --git a/examples/helix.ctt b/examples/helix.ctt
index 4f5d750bc50a85fb17514d7a5035d5e14a2c98c8..df89a0b5908c97082b41187149ed26f2b091b892 100644 (file)
--- a/examples/helix.ctt
+++ b/examples/helix.ctt
@@ -4,19 +4,12 @@ import circle
 import hedberg\r
 import retract\r
 \r
-loop1 : loopS1 = loop'\r
-triv : loopS1 = <i>base\r
-\r
-compS1 : loopS1 -> loopS1 -> loopS1 = compId S1 base base base\r
-\r
 encode (x:S1) (p:Id S1 base x) : helix x = subst S1 helix base x p zeroZ\r
 \r
 itLoop : nat -> loopS1 = split\r
  zero -> triv\r
  suc n -> compS1 (itLoop n) loop1\r
 \r
-invLoop : loopS1 = inv S1 base base loop1\r
-\r
 itLoopNeg : nat -> loopS1 = split \r
  zero -> invLoop\r
  suc n -> compS1 (itLoopNeg n) invLoop\r
@@ -28,12 +21,6 @@ loopIt : Z -> loopS1 = split
 lemItNat (n:nat) : Id loopS1 (itLoop (suc n)) (transport (<i>Id S1 base (loop{S1} @ i)) (itLoop n)) = \r
  refl loopS1 (itLoop (suc n))\r
 \r
-lemCompInv (A:U) (a b c:A) (p:Id A a b) (q:Id A b c) : Id (Id A a b) (compId A a c b (compId A a b c p q) (inv A b c q)) p =\r
- <j i> comp A (comp A (p @ i) [(i=1) -> <k> q @ (-j /\ k)]) [(i=1) -> <k> q @ (-j /\ - k)]\r
-\r
-lemInv (A:U) (a b:A) (p:Id A a b) : Id (Id A b b) (compId A b a b (inv A a b p) p)  (refl A b) =\r
-  <j i> comp A (p @ (-i \/ j)) [(i=1) -> <k> p @ (j \/ k)]\r
-\r
 lemItNeg : (n:nat) -> Id loopS1  (transport (<i>Id S1 base (loop{S1} @ i)) (loopIt (inl n))) (loopIt (sucZ (inl n))) = split\r
  zero ->  lemInv S1 base base loop1\r
  suc n -> lemCompInv S1 base base base (itLoopNeg n) invLoop\r
@@ -71,8 +58,6 @@ lemPropFib (P:S1 -> U) (pP:(x:S1) -> prop (P x)) (bP: P base) : (x:S1) -> P x =
  base -> bP\r
  loop @ i -> (lemPropF S1 P pP base base loop1 bP bP) @ i\r
 \r
--- other proof?\r
-\r
 helixSet : (x:S1) -> set (helix x) = lemPropFib (\ (x:S1) -> set (helix x)) rem ZSet\r
  where rem (x:S1) : prop (set (helix x)) = setIsProp (helix x)\r
 \r
@@ -82,7 +67,6 @@ retHelix (x:S1) (p : Id S1 base x) : Id (Id S1 base x) (decode x (encode x p)) p
 setLoop : set loopS1 = retractSet loopS1 Z (encode base) (decode base) (retHelix base) ZSet\r
 \r
 -- S1 is a groupoid\r
-\r
 isGroupoidS1 : groupoid S1 = lem\r
  where\r
   lem2 : (y : S1) -> set (Id S1 base y)\r
@@ -182,10 +166,3 @@ invLaw : (x y : S1) ->
                 (compId S1 (mult x y) (mult y x) (mult x y) (multCom x y) (multCom y x))\r
 \r
   bP : P base base = refl (Id S1 base base) (refl S1 base)\r
-\r
-\r
--- homotopy\r
-\r
-aLoop : loopS1 = <i>loop{S1}@(i/\-i)\r
-\r
-test : Id loopS1 triv aLoop = <j i>loop{S1}@(j/\i/\-i)\r

diff --git a/examples/int.ctt b/examples/int.ctt
index 3ff969188580ad6a195a56a708628c6ecdc47b42..3d12f3239f8f0ce327b9430781777c580ac3b5ab 100644 (file)
--- a/examples/int.ctt
+++ b/examples/int.ctt
@@ -40,3 +40,5 @@ predsucZ : (x : Z) -> Id Z (predZ (sucZ x)) x = split
   inr v -> refl Z (inr v)\r
 \r
 sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ\r
+\r
+ZSet : set Z = hedberg Z (orDisc nat nat natDec natDec)
\ No newline at end of file

diff --git a/examples/interval.ctt b/examples/interval.ctt
index ee1f108c16d3a90c626eb278cc9f633567f6cfb0..d5a2c43718c630c1ecce1dbb367f614b8552a32a 100644 (file)
--- a/examples/interval.ctt
+++ b/examples/interval.ctt
@@ -4,6 +4,7 @@ import prelude
 
 data I = zero | one | seg @ zero ~ one
 
+-- Proof of funext from the interval
 fext (A B : U) (f g : A -> B) (p : (x : A) -> Id B (f x) (g x)) :
      Id (A -> B) f g = <j> (\(x : A) -> htpy x (seg{I} @ j))
   where htpy (x : A) : I -> B = split

diff --git a/examples/nat.ctt b/examples/nat.ctt
index a3a7be4e39e4543aa8a0208f37b31bad9ca961c9..f36e78dbf0e90dc660534cb55097f8de4d98bf1d 100644 (file)
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -1,6 +1,6 @@
 module nat where
 
-import prelude
+import hedberg
 
 data nat = zero | suc (n : nat)
 
@@ -31,3 +31,26 @@ test : Id (nat -> nat) idnat (idfun nat) = funExt nat (\(_ : nat) -> nat) idnat
   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)
+
+caseNat (A : U) (a0 aS : A) : nat -> A = split
+ zero -> a0
+ suc n -> aS
+
+caseDNat (P:nat -> U) (a0 :P zero) (aS : (n:nat) -> P (suc n))
+            : (n:nat) -> P n = split
+ zero -> a0
+ suc n -> aS n
+
+znots (n : nat) : neg (Id nat zero (suc n)) =
+ \ (h:Id nat zero (suc n)) -> subst nat (caseNat U nat N0) zero (suc n) h zero
+
+snotz (n : nat) : neg (Id nat (suc n) zero) =
+ \ (h:Id nat (suc n) zero) -> znots n (inv nat (suc n) zero h)
+
+natDec : (n m:nat) -> dec (Id nat n m) = split
+ zero -> caseDNat (\ (m:nat) -> dec (Id nat zero m)) (inl (refl nat zero)) (\ (m:nat) -> inr (znots m))
+ suc n -> caseDNat (\ (m:nat) -> dec (Id nat (suc n) m)) (inr (snotz n))
+   (\ (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))
+
+natSet : set nat = hedberg nat natDec

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 23d17e2a7577de58fcd24e072cd32158cf3cef50..c584fe60b37e961d782ded8f247f65021c8661bd 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -1,5 +1,7 @@
 module prelude where
 
+-- Identity types
+
 Id (A : U) (a0 a1 : A) : U = IdP (<i> A) a0 a1
 
 refl (A : U) (a : A) : Id A a a = <i> a
@@ -18,6 +20,9 @@ subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
 substRefl (A : U) (P : A -> U) (a : A) (e : P a) :
   Id (P a) (subst A P a a (refl A a) e) e = refl (P a) e
 
+substInv (A : U) (P : A -> U) (a b : A) (p : Id A a b) : P b -> P a =
+ subst A P b a (<i> p @ -i)
+
 singl (A : U) (a : A) : U = (x : A) * Id A a x
 
 contrSingl (A : U) (a b : A) (p : Id A a b) :
@@ -51,7 +56,11 @@ 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
+lemCompInv (A:U) (a b c:A) (p:Id A a b) (q:Id A b c) : Id (Id A a b) (compId A a c b (compId A a b c p q) (inv A b c q)) p =
+ <j i> comp A (comp A (p @ i) [(i=1) -> <k> q @ (-j /\ k)]) [(i=1) -> <k> q @ (-j /\ - k)]
+
+lemInv (A:U) (a b:A) (p:Id A a b) : Id (Id A b b) (compId A b a b (inv A a b p) p)  (refl A b) =
+  <j i> comp A (p @ (-i \/ j)) [(i=1) -> <k> p @ (j \/ k)]
 
 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)
@@ -113,7 +122,7 @@ setIsProp (A : U) (f g : set A) : Id (set A) f g =
  <i> \(a b :A) -> (propIsProp (Id A a b) (f a b) (g a b)) @ i
 
 propPi (A : U) (B : A -> U) (h : (x : A) -> prop (B x))
-       (f0 f1 : (x : A) -> B x) : Id ((x : A) -> B x) f0 f1 
+       (f0 f1 : (x : A) -> B x) : Id ((x : A) -> B x) f0 f1
   = <i> \ (x:A) -> (h x (f0 x) (f1 x)) @ i
 
 IdS (A : U) (P : A -> U) (a0 a1 : A) (p : Id A a0 a1) (u0 : P a0) (u1 : P a1) : U =
@@ -122,4 +131,28 @@ IdS (A : U) (P : A -> U) (a0 a1 : A) (p : Id A a0 a1) (u0 : P a0) (u1 : P a1) :
 lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 : A)
          (p : Id A a0 a1) (b0 : P a0) (b1 : P a1) : IdS A P a0 a1 p b0 b1 =
   <i> (pP (p @ i) (transport (<j> P (p @ i /\ j)) b0)
-          (transport (<j> P (p @ i \/ -j)) b1)) @ i
\ No newline at end of file
+          (transport (<j> P (p @ i \/ -j)) b1)) @ i
+
+
+-- Basic data types
+
+data N0 =
+
+efq (A : U) : N0 -> A = split{}
+neg (A : U) : U = A -> N0
+
+data Unit = tt
+
+data or (A B : U) = inl (a : A)
+                  | inr (b : B)
+
+dec (A : U) : U = or A (neg A)
+
+discrete (A : U) : U = (a b : A) -> dec (Id A a b)
+
+injective (A B : U) (f : A -> B) : U =
+  (a0 a1 : A) -> Id B (f a0) (f a1) -> Id A a0 a1
+
+idfun (A : U) (a : A) : A = a
+
+and (A B : U) : U = (_ : A) * B

diff --git a/examples/susp.ctt b/examples/susp.ctt
index 161141dd1348d9ea2adf41bb1a5338ddc6701db3..c1212ce7602362b876f0f72589d0af8dbf2d9dc0 100644 (file)
--- a/examples/susp.ctt
+++ b/examples/susp.ctt
@@ -2,7 +2,9 @@ module susp where
 \r
 import circle\r
 \r
-data susp (A:U) = north | south | merid (a:A) @ north ~ south\r
+data susp (A : U) = north\r
+                  | south\r
+                  | merid (a:A) @ north ~ south\r
 \r
 -- n-spheres\r
 sphere : nat -> U = split\r
@@ -18,7 +20,7 @@ s1ToCircle : sone -> S1 = split
   south   -> base\r
   merid b @ i -> (path b) @ i\r
     where path : bool ->Id S1 base base = split\r
-            false -> loop'\r
+            false -> loop1\r
             true  -> refl S1 base\r
 \r
 m0 : Id sone north south = <i> (merid{sone} false) @ i\r
@@ -37,7 +39,7 @@ oc (x:S1) : S1 = s1ToCircle (circleToS1 x)
 \r
 ocid : (x : S1) -> Id S1 (oc x) x = split\r
     base -> refl S1 base\r
-    loop @ i -> <j> oc (loop' @ i)\r
+    loop @ i -> <j> oc (loop1 @ i)\r
 \r
 co (x: sone) : sone = circleToS1 (s1ToCircle x)\r
 \r
@@ -98,7 +100,7 @@ s1ToCId (p: Id sone north north) : Id S1 base base
 s1ToCIdInv (p : Id S1 base base) : Id sone north north\r
  = <i> (transport (<j> s1EqCircle @(-j)) (p @ i))\r
 \r
-loop1S :  Id sone north north = s1ToCIdInv loop'\r
+loop1S :  Id sone north north = s1ToCIdInv loop1\r
 \r
 loop2S : Id sone north north = compId sone north north north loop1S loop1S\r
 \r