Adapted prelude

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index f359fead3a15813c76af2197db5265a6c0afaf5a..925118259476f9b066cb53b57cbf4282ba0fd556 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -19,8 +19,8 @@ funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
 subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
   transport (mapOnPath A U P a b p) e
 
-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
+-- 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)
@@ -35,13 +35,13 @@ J (A : U) (a : A) (C : (x : A) -> Id A a x -> U)
     subst (singl A a) T (a, refl A a) (x, p) (contrSingl A a x p) d
       where T (z : singl A a) : U = C (z.1) (z.2)
 
-defEqJ (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a)) :
-       Id (C a (refl A a)) (J A a C d a (refl A a)) d = refl (C a (refl A a)) d
+-- defEqJ (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a)) :
+--        Id (C a (refl A a)) (J A a C d a (refl A a)) d = refl (C a (refl A a)) d
 
 inv (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> p @ -i
 
 compId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c =
-  <i> comp A (p @ i) [ (i = 1) -> q ]
+  <i> comp A (p @ i) [ (i = 1) -> q, (i=0) -> <_> a ]
 
 compId' (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c =
   subst A (Id A a) b c q p
@@ -58,28 +58,28 @@ 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)
 
-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)]
+-- 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)]
+-- 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)
 
-compEmpty (A : U) (a b : A) (p : Id A a b) : Id A a b =
-  <i> comp A (p @ i) [ ]
+-- 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 ]
+-- 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)
@@ -88,9 +88,9 @@ isoId (A B : U) (f : A -> B) (g : B -> A)
 
 idfun (A : U) (a : A) : A = a
 
-isoIdRef (A : U) :
-  Id (Id U A A) (refl U A) (isoId A A (idfun A) (idfun A) (refl A) (refl A)) =
-  <i j> glueLine j i A
+-- isoIdRef (A : U) :
+--   Id (Id U A A) (refl U A) (isoId A A (idfun A) (idfun A) (refl A) (refl A)) =
+--   <i j> glueLine j i A
 
 --         u
 --    a0 -----> a1
@@ -136,10 +136,10 @@ propPi (A : U) (B : A -> U) (h : (x : A) -> prop (B x))
 IdS (A : U) (P : A -> U) (a0 a1 : A) (p : Id A a0 a1) (u0 : P a0) (u1 : P a1) : U =
   IdP (<i> P (p @ i)) u0 u1
 
-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
+-- 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
 
 -- Basic data types