remove all <_>

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index c617191669593b7f15a5f7a984bf1bba224e8e6f..6105336a0cdd015cf9dcb3f1f8272986a30a36b2 100644 (file)
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -87,7 +87,7 @@ transIdFun (A B : U) (w : equiv A B)
        u : A = comp (<j>A) a []
        q : Id B (w.1 u) b = <i>w.1 (comp (<j>A) a [(i=1) -> <j>a])
    in comp (<j> B)
-        (comp (<j> B) (comp (<j> B) (comp (<j> B) (w.1 u) [(i=0)->q]) [(i=0)-><_>b]) [(i=0)-><_>b]) [(i=0)-><_>b]
+        (comp (<j> B) (comp (<j> B) (comp (<j> B) (w.1 u) [(i=0)->q]) [(i=0)-><k>b]) [(i=0)-><k>b]) [(i=0)-><k>b]
 
 idToId (A B : U) (w : equiv A B)
   : Id (equiv A B) (transEquiv A B (transEquivToId A B w)) w
@@ -104,44 +104,44 @@ lemIso (A B : U) (f : A -> B) (g : B -> A)
        Id (fiber A B f y) (x0,p0) (x1,p1) = <i> (p @ i,sq1 @ i)
   where
     rem0 : Id A (g y) x0 =
-      <i> comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <_> g y ]
+      <i> comp (<k> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <k> g y ]
 
     rem1 : Id A (g y) x1 =
-      <i> comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <_> g y ]
+      <i> comp (<k> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <k> g y ]
 
     p : Id A x0 x1 =
-     <i> comp (<_> A) (g y) [ (i = 0) -> rem0
+     <i> comp (<k> A) (g y) [ (i = 0) -> rem0
                             , (i = 1) -> rem1 ]
 
     fill0 : Square A (g y) (g (f x0)) (g y) x0
                      (<i> g (p0 @ i)) rem0 (<i> g y) (t x0)  =
-      <i j> comp (<_> A) (g (p0 @ i)) [ (i = 1) -> <k> t x0 @ j /\ k
-                                      , (i = 0) -> <_> g y
-                                      , (j = 0) -> <_> g (p0 @ i) ]
+      <i j> comp (<k> A) (g (p0 @ i)) [ (i = 1) -> <k> t x0 @ j /\ k
+                                      , (i = 0) -> <k> g y
+                                      , (j = 0) -> <k> g (p0 @ i) ]
 
     fill1 : Square A (g y) (g (f x1)) (g y) x1
                      (<i> g (p1 @ i)) rem1 (<i> g y) (t x1) =
-      <i j> comp (<_> A) (g (p1 @ i)) [ (i = 1) -> <k> t x1 @ j /\ k
-                                      , (i = 0) -> <_> g y
-                                      , (j = 0) -> <_> g (p1 @ i) ]
+      <i j> comp (<k> A) (g (p1 @ i)) [ (i = 1) -> <k> t x1 @ j /\ k
+                                      , (i = 0) -> <k> g y
+                                      , (j = 0) -> <k> g (p1 @ i) ]
 
     fill2 : Square A (g y) (g y) x0 x1
-                     (<_> g y) p rem0 rem1 =
-      <i j> comp (<_> A) (g y) [ (i = 0) -> <k> rem0 @ j /\ k
+                     (<k> g y) p rem0 rem1 =
+      <i j> comp (<k> A) (g y) [ (i = 0) -> <k> rem0 @ j /\ k
                                , (i = 1) -> <k> rem1 @ j /\ k
-                               , (j = 0) -> <_> g y ]
+                               , (j = 0) -> <k> g y ]
 
     sq : Square A (g y) (g y) (g (f x0)) (g (f x1))
                   (<i> g y) (<i> g (f (p @ i)))
                   (<j> g (p0 @ j)) (<j> g (p1 @ j)) =
-      <i j> comp (<_> A) (fill2 @ i @ j) [ (i = 0) -> <k> fill0 @ j @ -k
+      <i j> comp (<k> A) (fill2 @ i @ j) [ (i = 0) -> <k> fill0 @ j @ -k
                                          , (i = 1) -> <k> fill1 @ j @ -k
-                                         , (j = 0) -> <_> g y
+                                         , (j = 0) -> <k> g y
                                          , (j = 1) -> <k> t (p @ i) @ -k ]
 
     sq1 : Square B y y (f x0) (f x1)
-                   (<_>y) (<i> f (p @ i)) p0 p1 =
-      <i j> comp (<_> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j)
+                   (<k>y) (<i> f (p @ i)) p0 p1 =
+      <i j> comp (<k> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j)
                                          , (i = 1) -> s (p1 @ j)
                                          , (j = 1) -> s (f (p @ i))
                                          , (j = 0) -> s y ]

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index f452fb249dacdc120eff0c9c9717c4d67e2d29ba..856790e05685f40a5d7e4bb2d54de2aa25148c85 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -27,7 +27,7 @@ subst (A : U) (P : A -> U) (a b : A) (p : Id A a b) (e : P a) : P b =
 
 substEq (A : U) (P : A -> U) (a : A) (e : P a)
   : Id (P a) e (subst A P a a (refl A a) e) =
-  fill (<_> P a) e []
+  fill (<i> 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)
@@ -51,7 +51,7 @@ JEq (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d : C a (refl A a))
 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=0) -> <_> a ]
+  <i> comp (<j>A) (p @ i) [ (i = 1) -> q, (i=0) -> <j> 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
@@ -62,7 +62,7 @@ compId'' (A : U) (a b : A) (p : Id A a b) : (c : A) -> (q : Id A b c) -> Id 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]
+  <i> comp (<j>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 =
@@ -70,17 +70,17 @@ compDown (A : U) (a a' b b' : 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)
-          ((fill (<_>A) (p @ i) [(i=0) -> <_>a, (i=1) -> q]) @ -j)
-          [ (i=0) -> <_> a
+  <j i> comp (<k>A)
+          ((fill (<k>A) (p @ i) [(i=0) -> <k>a, (i=1) -> q]) @ -j)
+          [ (i=0) -> <k> a
           , (i=1) -> <k> q @ - (j \/  k)
-          , (j=0) -> fill (<_>A) ((compId A a b c p q @ i))
-                       [(i=0) -> <_>a, (i=1) -> <k> q @ -k ]
-          , (j=1) -> <_> p @ i
+          , (j=0) -> fill (<k>A) ((compId A a b c p q @ i))
+                       [(i=0) -> <k>a, (i=1) -> <k> q @ -k ]
+          , (j=1) -> <k> p @ i
           ]
 
 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=0) -> <l>b, (j=1) -> <l>b, (i=1) -> <k> p @ (j \/ k)]
+   <j i> comp (<k>A) (p @ (-i \/ j)) [(i=0) -> <l>b, (j=1) -> <l>b, (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)
@@ -90,17 +90,17 @@ test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1)
 
 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 ]
+  <i> comp (<j>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)
+   <j k> comp (<i> A) a
+           [ (j = 0) -> <i> comp (<l> A) (p @ i)
                               [ (k = 0) -> <l> p @ i
                               , (i = 0) -> <l> a
                               , (i = 1) -> <l> q @ k /\ l]
-           , (j = 1) -> <i> comp (<_> A) (p @ i)
+           , (j = 1) -> <i> comp (<l> A) (p @ i)
                               [ (k = 0) -> <l> p @ i
                               , (i = 0) -> <l> a
                               , (i = 1) -> <l> q' @ k /\ l]
@@ -108,8 +108,8 @@ lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c)
            , (k = 1)  -> s @ j ]
 
 IdPathTest1 (A : U) (a b : A) (p : Id A a b) :
-  Id (Id A a b) p (<i> comp (<_> A) (p @ i) [(i=0) -> <_> a,(i=1) -> <_> b]) = 
-  <j i> fill (<_> A) (p @ i) [(i=0) -> <_> a,(i=1) -> <_> b] @ j
+  Id (Id A a b) p (<i> comp (<j> A) (p @ i) [(i=0) -> <j> a,(i=1) -> <j> b]) = 
+  <j i> fill (<k> A) (p @ i) [(i=0) -> <k> a,(i=1) -> <k> b] @ j
 
 idfun (A : U) (a : A) : A = a
 
@@ -127,7 +127,7 @@ Square (A : U) (a0 a1 b0 b1 : A)
   = IdP (<i> (IdP (<j> A) (u @ i) (v @ i))) r0 r1
 
 constSquare (A : U) (a : A) (p : Id A a a) : Square A a a a a p p p p =
-  <i j> comp (<_>A) a
+  <i j> comp (<k>A) a
      [(i = 0) -> <k> p @ (j \/ - k),
       (i = 1) -> <k> p @ (j /\ k),
       (j = 0) -> <k> p @ (i \/ - k),
@@ -138,7 +138,7 @@ set (A : U) : U = (a b : A) -> prop (Id A a b)
 groupoid (A : U) : U = (a b : A) -> set (Id A a b)
 
 propSet (A : U) (h : prop A) (a b : A) (p q : Id A a b) : Id (Id A a b) p q =
- <j i> comp (<_>A) a [ (i=0) -> h a a
+ <j i> comp (<k>A) a [ (i=0) -> h a a
                 , (i=1) -> h a b
                 , (j=0) -> h a (p @ i)
                 , (j=1) -> h a (q @ i)]

diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index 693c62897a2e54efbda16756b8e0d030cd6c1145..58c6920ac19c3d09ad1db3c1a2b8a3a00c216776 100644 (file)
--- a/examples/univalence.ctt
+++ b/examples/univalence.ctt
@@ -6,7 +6,7 @@
 module univalence where
 
 import equiv
-import bool
+-- import bool
 
 ------------------------------------------------------------------------------
 -- Proof of univalence using unglue:
@@ -96,24 +96,24 @@ lem1 (B:U) : isContr ((X:U) * equiv X B) =
               ,unglueElemB
               ,\(b : B)
                -> let center : fiber glueB B unglueElemB b
-                             = (glueElem (comp (<_> B) b [(i=0) -> <_> b
+                             = (glueElem (comp (<j> B) b [(i=0) -> <j> b
                                                          ,(i=1) -> (w.2.2 b).1.2])
                                          [(i=0) -> b
                                          ,(i=1) -> (w.2.2 b).1.1]
-                               ,fill (<_> B) b [(i=0) -> <_> b
+                               ,fill (<j> B) b [(i=0) -> <j> b
                                                ,(i=1) -> (w.2.2 b).1.2])
                       contr (v : fiber glueB B unglueElemB b)
                             : Id (fiber glueB B unglueElemB b) center v
-                            = <j> (glueElem (comp (<_> B) b [(i=0) -> <k> v.2 @ (j /\ k)
+                            = <j> (glueElem (comp (<j> B) b [(i=0) -> <k> v.2 @ (j /\ k)
                                                             ,(i=1) -> ((w.2.2 b).2 v @ j).2
-                                                            ,(j=0) -> fill (<_> B) b [(i=0) -> <_> b
+                                                            ,(j=0) -> fill (<j> B) b [(i=0) -> <j> b
                                                                                      ,(i=1) -> (w.2.2 b).1.2]
                                                             ,(j=1) -> v.2])
                                             [(i=0) -> v.2 @ j
                                             ,(i=1) -> ((w.2.2 b).2 v @ j).1]
-                                  ,fill (<_> B) b [(i=0) -> <l> v.2 @ (j /\ l)
+                                  ,fill (<j> B) b [(i=0) -> <l> v.2 @ (j /\ l)
                                                   ,(i=1) -> ((w.2.2 b).2 v @ j).2
-                                                  ,(j=0) -> fill (<_> B) b [(i=0) -> <_> b
+                                                  ,(j=0) -> fill (<j> B) b [(i=0) -> <j> b
                                                                            ,(i=1) -> (w.2.2 b).1.2]
                                                   ,(j=1) -> v.2])
                   in (center,contr)))
@@ -144,100 +144,100 @@ corrUniv' (A B : U) : equiv (Id U A B) (equiv A B) =
   (transEquiv' B A,univalence B A)
 
 
--- Some tests of normal forms:
-testUniv1 (A : U) : Id U A A =
-  trans (equiv A A) (Id U A A) (<i> corrUniv A A @ -i) (idEquiv A)
+-- -- Some tests of normal forms:
+-- testUniv1 (A : U) : Id U A A =
+--   trans (equiv A A) (Id U A A) (<i> corrUniv A A @ -i) (idEquiv A)
 
--- obtained by normal form
-ntestUniv1 (A:U) : Id U A A =
- <i> comp (<_>U)
-      (comp (<_>U) A
-         [ (i = 0) -> <l> comp (<_>U) A [ (l = 0) -> <i> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i))))), (i = 1) -> (A,(comp (<l> A -> A) (\(x : A) -> x) [],comp (<l> (y : A) ->
-  ((x : ((x : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x []) [ (l = 0) -> <j> comp (<k> A) x [ (j = 1) -> <k> x ] ]))) *    (y0 : ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i)))) [])) ], (l = 1) -> <i> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i))))), (i = 1) -> (A,(comp (<l> A -> A) (\(x : A) -> x) [],comp (<l> (y : A) ->
-        ((x : ((x : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x []) [ (l = 0) -> <j> comp (<k> A) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i)))) [])) ] ], (i = 1) -> <l> A ]) [ (i = 0) -> <l> A, (i = 1) -> <l> A ]
+-- -- obtained by normal form
+-- ntestUniv1 (A:U) : Id U A A =
+--  <i> comp (<_>U)
+--       (comp (<_>U) A
+--          [ (i = 0) -> <l> comp (<_>U) A [ (l = 0) -> <i> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i))))), (i = 1) -> (A,(comp (<l> A -> A) (\(x : A) -> x) [],comp (<l> (y : A) ->
+--   ((x : ((x : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x []) [ (l = 0) -> <j> comp (<k> A) x [ (j = 1) -> <k> x ] ]))) *    (y0 : ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i)))) [])) ], (l = 1) -> <i> glue A [ (i = 0) -> (A,(\(x : A) -> x,\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i))))), (i = 1) -> (A,(comp (<l> A -> A) (\(x : A) -> x) [],comp (<l> (y : A) ->
+--         ((x : ((x : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x []) [ (l = 0) -> <j> comp (<k> A) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : A) * IdP (<j> A) y (comp (<j> A) (comp (<i> A) x0 []) [ (l = 0) -> <j> comp (<k> A) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : A) -> ((a,<l> a),\(z : ((x : A) * IdP (<l> A) a x)) -> <l> (z.2 @ l,<i> z.2 @ (l /\ i)))) [])) ] ], (i = 1) -> <l> A ]) [ (i = 0) -> <l> A, (i = 1) -> <l> A ]
 
-testUniv2 : bool = trans bool bool (ntestUniv1 bool) true
+-- testUniv2 : bool = trans bool bool (ntestUniv1 bool) true
 
-ntestUniv2 : bool =
- comp (<i> comp (<_>U) (comp (<_>U) bool [ (i = 0) -> <j> comp (<_>U) bool [ (j = 0) -> <i> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp (<i> bool -> bool) (\(x : bool) -> x) [],comp (<i> (y : bool) ->
-  ((x : ((x : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x []) [ (i = 0) -> <j> comp (<k> bool) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : bool) * IdP (<k> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j)))) [])) ], (j = 1) -> <i> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp (<i> bool -> bool) (\(x : bool) -> x) [],comp (<i> (y : bool) ->
-  ((x : ((x : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x []) [ (i = 0) -> <j> comp (<k> bool) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : bool) * IdP (<k> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> <j> bool ]) [ (i = 0) -> <j> bool, (i = 1) -> <j> bool ]) true []
+-- ntestUniv2 : bool =
+--  comp (<i> comp (<_>U) (comp (<_>U) bool [ (i = 0) -> <j> comp (<_>U) bool [ (j = 0) -> <i> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp (<i> bool -> bool) (\(x : bool) -> x) [],comp (<i> (y : bool) ->
+--   ((x : ((x : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x []) [ (i = 0) -> <j> comp (<k> bool) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : bool) * IdP (<k> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j)))) [])) ], (j = 1) -> <i> glue bool [ (i = 0) -> (bool,(\(x : bool) -> x,\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j))))), (i = 1) -> (bool,(comp (<i> bool -> bool) (\(x : bool) -> x) [],comp (<i> (y : bool) ->
+--   ((x : ((x : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x []) [ (i = 0) -> <j> comp (<k> bool) x [ (j = 1) -> <k> x ] ]))) * (y0 : ((x0 : bool) * IdP (<j> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) -> IdP (<j> ((x0 : bool) * IdP (<k> bool) y (comp (<j> bool) (comp (<i> bool) x0 []) [ (i = 0) -> <j> comp (<k> bool) x0 [ (j = 1) -> <k> x0 ] ]))) x y0)) (\(a : bool) -> ((a,<i> a),\(z : ((x : bool) * IdP (<i> bool) a x)) -> <i> (z.2 @ i,<j> z.2 @ (i /\ j)))) [])) ] ], (i = 1) -> <j> bool ]) [ (i = 0) -> <j> bool, (i = 1) -> <j> bool ]) true []
 
 
--- A small test of univalence using boolean negation
-isEquivNegBool : isEquiv bool bool negBool =
- gradLemma bool bool negBool negBool negBoolK negBoolK
+-- -- A small test of univalence using boolean negation
+-- isEquivNegBool : isEquiv bool bool negBool =
+--  gradLemma bool bool negBool negBool negBoolK negBoolK
 
-eqBool : Id U bool bool = 
- trans (equiv bool bool) (Id U bool bool)
-       (<i> corrUniv bool bool @ -i) (negBool,isEquivNegBool)
+-- eqBool : Id U bool bool = 
+--  trans (equiv bool bool) (Id U bool bool)
+--        (<i> corrUniv bool bool @ -i) (negBool,isEquivNegBool)
 
-test1 : bool = trans bool bool eqBool true
-test2 : bool = trans bool bool eqBool false
+-- test1 : bool = trans bool bool eqBool true
+-- test2 : bool = trans bool bool eqBool false
 
 
 
 
-------------------------------------------------------------------------------
--- The direct proof of univalence using transEquiv which is too slow
--- to normalize:
+-- ------------------------------------------------------------------------------
+-- -- The direct proof of univalence using transEquiv which is too slow
+-- -- to normalize:
 
--- transEquiv is an equiv
-transEquivIsEquiv (A B : U)
-  : isEquiv (Id U A B) (equiv A B) (transEquiv A B)
-  = gradLemma (Id U A B) (equiv A B) (transEquiv A B)
-      (transEquivToId A B) (idToId A B) (eqToEq A B)
+-- -- transEquiv is an equiv
+-- transEquivIsEquiv (A B : U)
+--   : isEquiv (Id U A B) (equiv A B) (transEquiv A B)
+--   = gradLemma (Id U A B) (equiv A B) (transEquiv A B)
+--       (transEquivToId A B) (idToId A B) (eqToEq A B)
 
--- Univalence proved using transEquiv
-univalenceTrans (A B:U) : Id U (Id U A B) (equiv A B) = 
- isoId (Id U A B) (equiv A B) (transEquiv A B)
-       (transEquivToId A B) (idToId A B) (eqToEq A B)
+-- -- Univalence proved using transEquiv
+-- univalenceTrans (A B:U) : Id U (Id U A B) (equiv A B) = 
+--  isoId (Id U A B) (equiv A B) (transEquiv A B)
+--        (transEquivToId A B) (idToId A B) (eqToEq A B)
 
-univalenceTrans' (A B : U) : equiv (Id U A B) (equiv A B) =
-  (transEquiv A B,transEquivIsEquiv A B)
+-- univalenceTrans' (A B : U) : equiv (Id U A B) (equiv A B) =
+--   (transEquiv A B,transEquivIsEquiv A B)
 
--- univalenceTrans takes extremely much memory when normalizing
+-- -- univalenceTrans takes extremely much memory when normalizing
 
--- This also takes too long to normalize:
-slowtest (A : U) : Id (equiv A A)
-  (transEquiv A A (transEquivToId A A (idEquiv A))) (idEquiv A) =
-    idToId A A (idEquiv A)
+-- -- This also takes too long to normalize:
+-- slowtest (A : U) : Id (equiv A A)
+--   (transEquiv A A (transEquivToId A A (idEquiv A))) (idEquiv A) =
+--     idToId A A (idEquiv A)
 
 
 
 
-------------------------------------------------------------------------------
--- TODO: Adapt this to new definition of equiv
-
--- The canonical map defined using J
--- canIdToEquiv (A : U) : (B : U) -> Id U A B -> equiv A B =
---   J U A (\ (B : U) (_ : Id U A B) -> equiv A B) (idEquiv A)
-
--- canDiagTrans (A : U) : Id (A -> A) (canIdToEquiv A A (<_> A)).1 (idfun A) =
---   <i> fill (<_> A -> A) (idfun A) [] @ -i
-
--- transDiagTrans (A : U) : Id (A -> A) (idfun A) (trans A A (<_> A)) =
---   <i> \ (a : A) -> fill (<_> A) a [] @ i
-
--- canIdToEquivLem (A : U) : (B : U) (p : Id U A B) ->
---   Id (A -> B) (canIdToEquiv A B p).1 (transEquiv A B p).1
---   = J U A
---       (\ (B : U) (p : Id U A B) ->
---         Id (A -> B) (canIdToEquiv A B p).1 (transEquiv A B p).1)
---       (compId (A -> A)
---         (canIdToEquiv A A (<_> A)).1 (idfun A) (trans A A (<_> A))
---         (canDiagTrans A) (transDiagTrans A))
-
--- canIdToEquivIsTransEquiv (A B : U) :
---   Id (Id U A B -> equiv A B) (canIdToEquiv A B) (transEquiv A B) =
---   <i> \ (p : Id U A B) ->
---         equivLemma A B (canIdToEquiv A B p) (transEquiv A B p)
---           (canIdToEquivLem A B p) @ i
-
--- -- The canonical map is an equivalence
--- univalenceJ (A B : U) : isEquiv (Id U A B) (equiv A B) (canIdToEquiv A B) =
---   substInv (Id U A B -> equiv A B)
---     (isEquiv (Id U A B) (equiv A B))
---      (canIdToEquiv A B) (transEquiv A B)
---      (canIdToEquivIsTransEquiv A B)
---      (transEquivIsEquiv A B)
\ No newline at end of file
+-- ------------------------------------------------------------------------------
+-- -- TODO: Adapt this to new definition of equiv
+
+-- -- The canonical map defined using J
+-- -- canIdToEquiv (A : U) : (B : U) -> Id U A B -> equiv A B =
+-- --   J U A (\ (B : U) (_ : Id U A B) -> equiv A B) (idEquiv A)
+
+-- -- canDiagTrans (A : U) : Id (A -> A) (canIdToEquiv A A (<_> A)).1 (idfun A) =
+-- --   <i> fill (<_> A -> A) (idfun A) [] @ -i
+
+-- -- transDiagTrans (A : U) : Id (A -> A) (idfun A) (trans A A (<_> A)) =
+-- --   <i> \ (a : A) -> fill (<_> A) a [] @ i
+
+-- -- canIdToEquivLem (A : U) : (B : U) (p : Id U A B) ->
+-- --   Id (A -> B) (canIdToEquiv A B p).1 (transEquiv A B p).1
+-- --   = J U A
+-- --       (\ (B : U) (p : Id U A B) ->
+-- --         Id (A -> B) (canIdToEquiv A B p).1 (transEquiv A B p).1)
+-- --       (compId (A -> A)
+-- --         (canIdToEquiv A A (<_> A)).1 (idfun A) (trans A A (<_> A))
+-- --         (canDiagTrans A) (transDiagTrans A))
+
+-- -- canIdToEquivIsTransEquiv (A B : U) :
+-- --   Id (Id U A B -> equiv A B) (canIdToEquiv A B) (transEquiv A B) =
+-- --   <i> \ (p : Id U A B) ->
+-- --         equivLemma A B (canIdToEquiv A B p) (transEquiv A B p)
+-- --           (canIdToEquivLem A B p) @ i
+
+-- -- -- The canonical map is an equivalence
+-- -- univalenceJ (A B : U) : isEquiv (Id U A B) (equiv A B) (canIdToEquiv A B) =
+-- --   substInv (Id U A B -> equiv A B)
+-- --     (isEquiv (Id U A B) (equiv A B))
+-- --      (canIdToEquiv A B) (transEquiv A B)
+-- --      (canIdToEquivIsTransEquiv A B)
+-- --      (transEquivIsEquiv A B)
\ No newline at end of file