From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Thu, 14 Jan 2016 15:33:23 +0000 (-0500)
Subject: rename sig to Sigma and make setquot compile
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=ce9c32564146d174c10993a119556a397a1ee18b;p=cubicaltt.git

rename sig to Sigma and make setquot compile
---

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 856790e..6c7f348 100644
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -165,6 +165,8 @@ lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a :A) :
    rem
  where rem : (b0 b1:P a) -> Id (P a) b0 b1 = pP a
 
+Sigma (A : U) (B : A -> U) : U = (x : A) * B x
+
 lemSig (A : U) (B : A -> U) (pB : (x : A) -> prop (B x))
        (u v : (x:A) * B x) (p : Id A u.1 v.1) :
        Id ((x:A) * B x) u v =
diff --git a/examples/setquot.ctt b/examples/setquot.ctt
index 49f9149..1d92302 100644
--- a/examples/setquot.ctt
+++ b/examples/setquot.ctt
@@ -6,10 +6,10 @@ import pi
 import univalence
 
 subtypeEquality (A : U) (B : A -> U) (pB : (x : A) -> prop (B x))
-                (s t : (x : A) * B x) : Id A s.1 t.1 -> Id (sig A B) s t =
-  trans (Id A s.1 t.1) (Id (sig A B) s t) rem
+                (s t : (x : A) * B x) : Id A s.1 t.1 -> Id (Sigma A B) s t =
+  trans (Id A s.1 t.1) (Id (Sigma A B) s t) rem
     where
-    rem : Id U (Id A s.1 t.1) (Id (sig A B) s t) =
+    rem : Id U (Id A s.1 t.1) (Id (Sigma A B) s t) =
       <i> lemSigProp A B pB s t @ -i
 
 -- (* Propositions *)
@@ -38,23 +38,24 @@ hdisj_in1 (P Q : U) (X : P) : (hdisj P Q).1 = hinhpr (or P Q) (inl X)
 hdisj_in2 (P Q : U) (X : Q) : (hdisj P Q).1 = hinhpr (or P Q) (inr X)
 
 -- Direct proof that logical equivalence is equiv for props
-equivhProp (P P' : hProp) (f : P.1 -> P'.1) (g : P'.1 -> P.1) : equiv P.1 P'.1 = (f,isEquivf)
-  where
-  isEquivf : isEquiv P.1 P'.1 f = (s,t)
-    where
-    s (y : P'.1) : fiber P.1 P'.1 f y = (g y,P'.2 (f (g y)) y)
-    t (y : P'.1) (w : fiber P.1 P'.1 f y) : Id ((x :  P.1) * Id P'.1 (f x) y) (s y) w =
-      subtypeEquality P.1 (\(x :  P.1) -> Id P'.1 (f x) y) pb (s y) w r1
-      where
-      pb (x : P.1) : (a b : Id P'.1 (f x) y) -> Id (Id P'.1 (f x) y) a b = propSet P'.1 P'.2 (f x) y
-      r1 : Id P.1 (s y).1 w.1 = P.2 (s y).1 w.1
+-- equivhProp (P P' : hProp) (f : P.1 -> P'.1) (g : P'.1 -> P.1) : equiv P.1 P'.1 = undefined
+-- (f,isEquivf)
+--   where
+--   isEquivf : isEquiv P.1 P'.1 f = (s,t)
+--     where
+--     s (y : P'.1) : fiber P.1 P'.1 f y = (g y,P'.2 (f (g y)) y)
+--     t (y : P'.1) (w : fiber P.1 P'.1 f y) : Id ((x :  P.1) * Id P'.1 (f x) y) (s y) w =
+--       subtypeEquality P.1 (\(x :  P.1) -> Id P'.1 (f x) y) pb (s y) w r1
+--       where
+--       pb (x : P.1) : (a b : Id P'.1 (f x) y) -> Id (Id P'.1 (f x) y) a b = propSet P'.1 P'.2 (f x) y
+--       r1 : Id P.1 (s y).1 w.1 = P.2 (s y).1 w.1
 
 -- Proof of uahp using full univalence
-uahp' (P P' : hProp) (f : P.1 -> P'.1) (g : P'.1 -> P.1) : Id hProp P P' =
-  subtypeEquality U prop propIsProp P P' rem
-  where
-  rem : Id U P.1 P'.1 =
-    invEq (Id U P.1 P'.1) (equiv P.1 P'.1) (univalence P.1 P'.1) (equivhProp P P' f g)
+-- uahp' (P P' : hProp) (f : P.1 -> P'.1) (g : P'.1 -> P.1) : Id hProp P P' = undefined
+  -- subtypeEquality U prop propIsProp P P' rem
+  -- where
+  -- rem : Id U P.1 P'.1 =
+  --   invEq (Id U P.1 P'.1) (equiv P.1 P'.1) (univalence P.1 P'.1) (equivhProp P P' f g)
 
 -- Direct proof of uahp
 uahp (P P' : hProp) (f : P.1 -> P'.1) (g : P'.1 -> P.1) : Id hProp P P' =
@@ -75,7 +76,7 @@ sethProp (P P' : hProp) : prop (Id hProp P P') =
   propidU (Id hProp P P') (equiv P.1 P'.1) rem (propequiv P.1 P'.1 P'.2)
   where
    rem1 : Id U (Id hProp P P') (Id U P.1 P'.1) = lemSigProp U prop propIsProp P P'
-   rem2 : Id U (Id U P.1 P'.1) (equiv P.1 P'.1) = univalence1 P.1 P'.1
+   rem2 : Id U (Id U P.1 P'.1) (equiv P.1 P'.1) = corrUniv P.1 P'.1
    rem : Id U (Id hProp P P') (equiv P.1 P'.1) =
      compId U (Id hProp P P') (Id U P.1 P'.1) (equiv P.1 P'.1) rem1 rem2
 
@@ -83,7 +84,7 @@ sethProp (P P' : hProp) : prop (Id hProp P P') =
 
 hsubtypes (X : U) : U = X -> hProp
 
-carrier (X : U) (A : hsubtypes X) : U = sig X (\(x : X) -> (A x).1)
+carrier (X : U) (A : hsubtypes X) : U = Sigma X (\(x : X) -> (A x).1)
 
 sethsubtypes (X : U) : set (hsubtypes X) =
   setPi X (\(_ : X) -> hProp) (\(_ : X) -> sethProp)
@@ -176,7 +177,7 @@ setquotunivprop (X : U) (R : eqrel X) (P : setquot X R.1 -> hProp)
    rem : (ishinh (carrier X c.1)).1 = eqax0 X R.1 c.1 c.2
 
 
--- Finally the exercise:
+-- The bool exercise:
 
 R : eqrel bool = (r1,r2)
   where
@@ -260,7 +261,7 @@ foo (x : bool') (x' : (P' x).1) : bool = f x rem
   rem : or (ishinh (Id bool' x true')).1 (ishinh (Id bool' x false')).1 =
     hinhuniv (or (Id bool' x true') (Id bool' x false'))
              (or (ishinh (Id bool' x true')).1 (ishinh (Id bool' x false')).1,test3 x)
-             (bar x) x' 
+             (bar x) x'
 
 -- > :n testfoo
 -- NORMEVAL: true
@@ -270,12 +271,12 @@ testfoo : bool = foo true' (K' true')
 testfoo' : Id bool (foo true' (K' true')) true = <i> foo true' (K' true')
 
 
-
 -- Tests of checking normal forms:
 
-ntrue' : bool' = (\(x : bool) -> (IdP (<i0> bool) true x,lem8 x),((\(P : sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP (<i0> bool) true x)) -> P.1) -> f ((true,<i0> true)),\(x1 x2 : bool) -> \(X1 : IdP (<i0> bool) x1 x2) -> \(X2 : IdP (<i0> bool) true x1) -> <i0> comp (<i1> bool) (X2 @ i0) [ (i0 = 0) -> <i1> true, (i0 = 1) -> <i1> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP (<i0> bool) true x1) -> \(X2 : IdP (<i0> bool) true x2) -> <i0> comp (<i1> bool) (X1 @ -i0) [ (i0 = 0) -> <i1> x1, (i0 = 1) -> <i1> X2 @ i1 ]))
+ntrue' : bool' = (\(x : bool) -> (IdP (<i0> bool) true x,lem8 x),((\(P : Sigma U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b)) -> \(f : (Sigma bool (\(x : bool) -> IdP (<i0> bool) true x)) -> P.1) -> f ((true,<i0> true)),\(x1 x2 : bool) -> \(X1 : IdP (<i0> bool) x1 x2) -> \(X2 : IdP (<i0> bool) true x1) -> <i0> comp (<i1> bool) (X2 @ i0) [ (i0 = 0) -> <i1> true, (i0 = 1) -> <i1> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP (<i0> bool) true x1) -> \(X2 : IdP (<i0> bool) true x2) -> <i0> comp (<i1> bool) (X1 @ -i0) [ (i0 = 0) -> <i1> x1, (i0 = 1) -> <i1> X2 @ i1 ]))
 
--- Why is this not working? Bug in pretty printer?
--- ntest : (P' true').1 = \(P : sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b)) -> \(f : or (IdP (<i0> sig (bool -> (sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b))) (\(A : bool -> (sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b))) -> sig (sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP (<i0> bool) x1 x2) -> ((A x1).1 -> (A x2).1))) (\(_ : sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP (<i0> bool) x1 x2) -> ((A x1).1 -> (A x2).1))) -> (x1 x2 : bool) -> (A x1).1 -> ((A x2).1 -> (IdP (<i0> bool) x1 x2))))) ((\(x : bool) -> (IdP (<i0> bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP (<i0> bool) true x)) -> P0.1) -> f ((true,<i0> true)),\(x1 x2 : bool) -> \(X1 : IdP (<i0> bool) x1 x2) -> \(X2 : IdP (<i0> bool) true x1) -> <i0> comp (<i1> bool) (X2 @ i0) [ (i0 = 0) -> <i1> true, (i0 = 1) -> <i1> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP (<i0> bool) true x1) -> \(X2 : IdP (<i0> bool) true x2) -> <i0> comp (<i1> bool) (X1 @ -i0) [ (i0 = 0) -> <i1> x1, (i0 = 1) -> <i1> X2 @ i1 ]))) ((\(x : bool) -> (IdP (<i0> bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP (<i0> bool) true x)) -> P0.1) -> f ((true,<i0> true)),\(x1 x2 : bool) -> \(X1 : IdP (<i0> bool) x1 x2) -> \(X2 : IdP (<i0> bool) true x1) -> <i0> comp (<i1> bool) (X2 @ i0) [ (i0 = 0) -> <i1> true, (i0 = 1) -> <i1> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP (<i0> bool) true x1) -> \(X2 : IdP (<i0> bool) true x2) -> <i0> comp (<i1> bool) (X1 @ -i0) [ (i0 = 0) -> <i1> x1, (i0 = 1) -> <i1> X2 @ i1 ]))), IdP (<i0> sig (bool -> (sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b))) (\(A : bool -> (sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b))) -> sig (sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP (<i0> bool) x1 x2) -> ((A x1).1 -> (A x2).1))) (\(_ : sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP (<i0> bool) x1 x2) -> ((A x1).1 -> (A x2).1))) -> (x1 x2 : bool) -> (A x1).1 -> ((A x2).1 -> (IdP (<i0> bool) x1 x2))))) ((\(x : bool) -> (IdP (<i0> bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP (<i0> bool) true x)) -> P0.1) -> f ((true,<i0> true)),\(x1 x2 : bool) -> \(X1 : IdP (<i0> bool) x1 x2) -> \(X2 : IdP (<i0> bool) true x1) -> <i0> comp (<i1> bool) (X2 @ i0) [ (i0 = 0) -> <i1> true, (i0 = 1) -> <i1> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP (<i0> bool) true x1) -> \(X2 : IdP (<i0> bool) true x2) -> <i0> comp (<i1> bool) (X1 @ -i0) [ (i0 = 0) -> <i1> x1, (i0 = 1) -> <i1> X2 @ i1 ]))) ((\(x : bool) -> (IdP (<i0> bool) false x,lem7 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP (<i0> bool) false x)) -> P0.1) -> f ((false,<i0> false)),\(x1 x2 : bool) -> \(X1 : IdP (<i0> bool) x1 x2) -> \(X2 : IdP (<i0> bool) false x1) -> <i0> comp (<i1> bool) (X2 @ i0) [ (i0 = 0) -> <i1> false, (i0 = 1) -> <i1> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP (<i0> bool) false x1) -> \(X2 : IdP (<i0> bool) false x2) -> <i0> comp (<i1> bool) (X1 @ -i0) [ (i0 = 0) -> <i1> x1, (i0 = 1) -> <i1> X2 @ i1 ])))) -> P.1) -> f (inl (<i0> (\(x : bool) -> (IdP (<i0> bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP (<i0> X) a b)) -> \(f0 : (sig bool (\(x : bool) -> IdP (<i0> bool) true x)) -> P0.1) -> f0 ((true,<i0> true)),\(x1 x2 : bool) -> \(X1 : IdP (<i0> bool) x1 x2) -> \(X2 : IdP (<i0> bool) true x1) -> <i0> comp (<i1> bool) (X2 @ i0) [ (i0 = 0) -> <i1> true, (i0 = 1) -> <i1> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP (<i0> bool) true x1) -> \(X2 : IdP (<i0> bool) true x2) -> <i0> comp (<i1> bool) (X1 @ -i0) [ (i0 = 0) -> <i1> x1, (i0 = 1) -> <i1> X2 @ i1 ]))))
 
+nhdisj_in1 : (P Q : U) (X : P) -> (hdisj P Q).1 =
+  \(P Q : U) -> \(X : P) -> \(P0 : Sigma U (\(X0 : U) -> (a b : X0) -> IdP (<!0> X0) a b)) -> \(f : or P Q -> P0.1) -> f (inl X)
 
+ntest : (P' true').1 = \(P : Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b)) -> \(f : or (IdP (<!0> Sigma (bool -> (Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b))) (\(A : bool -> (Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b))) -> Sigma (Sigma ((P0 : Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP (<!0> bool) x1 x2) -> ((A x1).1 -> (A x2).1))) (\(_ : Sigma ((P0 : Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP (<!0> bool) x1 x2) -> ((A x1).1 -> (A x2).1))) -> (x1 x2 : bool) -> (A x1).1 -> ((A x2).1 -> (IdP (<!0> bool) x1 x2))))) ((\(x : bool) -> (IdP (<!0> bool) true x,lem8 x),((\(P0 : Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b)) -> \(f : (Sigma bool (\(x : bool) -> IdP (<!0> bool) true x)) -> P0.1) -> f ((true,<!0> true)),\(x1 x2 : bool) -> \(X1 : IdP (<!0> bool) x1 x2) -> \(X2 : IdP (<!0> bool) true x1) -> <!0> comp (<!1> bool) (X2 @ !0) [ (!0 = 0) -> <!1> true, (!0 = 1) -> <!1> X1 @ !1 ]),\(x1 x2 : bool) -> \(X1 : IdP (<!0> bool) true x1) -> \(X2 : IdP (<!0> bool) true x2) -> <!0> comp (<!1> bool) (X1 @ -!0) [ (!0 = 0) -> <!1> x1, (!0 = 1) -> <!1> X2 @ !1 ]))) ((\(x : bool) -> (IdP (<!0> bool) true x,lem8 x),((\(P0 : Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b)) -> \(f : (Sigma bool (\(x : bool) -> IdP (<!0> bool) true x)) -> P0.1) -> f ((true,<!0> true)),\(x1 x2 : bool) -> \(X1 : IdP (<!0> bool) x1 x2) -> \(X2 : IdP (<!0> bool) true x1) -> <!0> comp (<!1> bool) (X2 @ !0) [ (!0 = 0) -> <!1> true, (!0 = 1) -> <!1> X1 @ !1 ]),\(x1 x2 : bool) -> \(X1 : IdP (<!0> bool) true x1) -> \(X2 : IdP (<!0> bool) true x2) -> <!0> comp (<!1> bool) (X1 @ -!0) [ (!0 = 0) -> <!1> x1, (!0 = 1) -> <!1> X2 @ !1 ])))) IdP (<!0> Sigma (bool -> (Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b))) (\(A : bool -> (Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b))) -> Sigma (Sigma ((P0 : Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP (<!0> bool) x1 x2) -> ((A x1).1 -> (A x2).1))) (\(_ : Sigma ((P0 : Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP (<!0> bool) x1 x2) -> ((A x1).1 -> (A x2).1))) -> (x1 x2 : bool) -> (A x1).1 -> ((A x2).1 -> (IdP (<!0> bool) x1 x2))))) ((\(x : bool) -> (IdP (<!0> bool) true x,lem8 x),((\(P0 : Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b)) -> \(f : (Sigma bool (\(x : bool) -> IdP (<!0> bool) true x)) -> P0.1) -> f ((true,<!0> true)),\(x1 x2 : bool) -> \(X1 : IdP (<!0> bool) x1 x2) -> \(X2 : IdP (<!0> bool) true x1) -> <!0> comp (<!1> bool) (X2 @ !0) [ (!0 = 0) -> <!1> true, (!0 = 1) -> <!1> X1 @ !1 ]),\(x1 x2 : bool) -> \(X1 : IdP (<!0> bool) true x1) -> \(X2 : IdP (<!0> bool) true x2) -> <!0> comp (<!1> bool) (X1 @ -!0) [ (!0 = 0) -> <!1> x1, (!0 = 1) -> <!1> X2 @ !1 ]))) ((\(x : bool) -> (IdP (<!0> bool) false x,lem7 x),((\(P0 : Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b)) -> \(f : (Sigma bool (\(x : bool) -> IdP (<!0> bool) false x)) -> P0.1) -> f ((false,<!0> false)),\(x1 x2 : bool) -> \(X1 : IdP (<!0> bool) x1 x2) -> \(X2 : IdP (<!0> bool) false x1) -> <!0> comp (<!1> bool) (X2 @ !0) [ (!0 = 0) -> <!1> false, (!0 = 1) -> <!1> X1 @ !1 ]),\(x1 x2 : bool) -> \(X1 : IdP (<!0> bool) false x1) -> \(X2 : IdP (<!0> bool) false x2) -> <!0> comp (<!1> bool) (X1 @ -!0) [ (!0 = 0) -> <!1> x1, (!0 = 1) -> <!1> X2 @ !1 ]))) -> P.1) -> f (inl (<!0> (\(x : bool) -> (IdP (<!0> bool) true x,lem8 x),((\(P0 : Sigma U (\(X : U) -> (a b : X) -> IdP (<!0> X) a b)) -> \(f0 : (Sigma bool (\(x : bool) -> IdP (<!0> bool) true x)) -> P0.1) -> f0 ((true,<!0> true)),\(x1 x2 : bool) -> \(X1 : IdP (<!0> bool) x1 x2) -> \(X2 : IdP (<!0> bool) true x1) -> <!0> comp (<!1> bool) (X2 @ !0) [ (!0 = 0) -> <!1> true, (!0 = 1) -> <!1> X1 @ !1 ]),\(x1 x2 : bool) -> \(X1 : IdP (<!0> bool) true x1) -> \(X2 : IdP (<!0> bool) true x2) -> <!0> comp (<!1> bool) (X1 @ -!0) [ (!0 = 0) -> <!1> x1, (!0 = 1) -> <!1> X2 @ !1 ]))))
diff --git a/examples/sigma.ctt b/examples/sigma.ctt
index cd124eb..1053e70 100644
--- a/examples/sigma.ctt
+++ b/examples/sigma.ctt
@@ -4,12 +4,10 @@ import prelude
 
 -- application of this fact
 
-sig (A : U) (P : A -> U) : U = (x : A) * P x
-
-lemIdSig (A:U) (B : A -> U) (t u : sig A B) :
- Id U (Id (sig A B) t u) ((p : Id A t.1 u.1) * IdP (<i> B (p @ i)) t.2 u.2) =
+lemIdSig (A:U) (B : A -> U) (t u : Sigma A B) :
+ Id U (Id (Sigma A B) t u) ((p : Id A t.1 u.1) * IdP (<i> B (p @ i)) t.2 u.2) =
   isoId T0 T1 f g s t where
-   T0 : U = Id (sig A B) t u
+   T0 : U = Id (Sigma A B) t u
    T1 : U = (p:Id A t.1 u.1) * IdP (<i> B (p@i)) t.2 u.2
    f (q:T0) : T1 = (<i> (q@i).1,<i> (q@i).2)
    g (z:T1) : T0 = <i>(z.1 @i,z.2 @i)
@@ -22,7 +20,7 @@ lemIdAnd (A B : U) (t u : and A B) :
 lem (A:U) (P:A->U) (pP:(x:A) -> prop (P x)) (u v:(x:A) * P x) (p:Id A u.1 v.1) :
  Id ((x:A)*P x) u v = <i>(p@i,(lemPropF A P pP u.1 v.1 p u.2 v.2)@i)
 
-propSig (A:U) (B:A-> U) (pA:prop A) (pB : (x:A) -> prop (B x)) (t u : sig A B) : Id (sig A B) t u
+propSig (A:U) (B:A-> U) (pA:prop A) (pB : (x:A) -> prop (B x)) (t u : Sigma A B) : Id (Sigma A B) t u
  = lem A B pB t u (pA t.1 u.1)
 
 lemTransp (A:U) (a:A) : Id A a (transport (<_>A) a) = fill (<_>A) a []
@@ -31,11 +29,11 @@ funDepTr (A:U) (P:A->U) (a0 a1 :A) (p:Id A a0 a1) (u0:P a0) (u1:P a1) :
              Id U (IdP (<i> P (p@i)) u0 u1) (Id (P a1) (transport (<i> P (p@i)) u0) u1) =
  <j>IdP (<i>P (p@j\/i)) (comp (<i>P (p@j/\i)) u0 [(j=0)-><_>u0]) u1
 
-lem2 (A:U) (B:A-> U) (t u : sig A B) (p:Id A t.1 u.1) : 
+lem2 (A:U) (B:A-> U) (t u : Sigma A B) (p:Id A t.1 u.1) : 
   Id U  (IdP (<i>B (p@i)) t.2 u.2) (Id (B u.1) (transport (<i>B (p@i)) t.2) u.2) =
     funDepTr A B t.1 u.1 p  t.2 u.2
 
-corSigProp (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : sig A B) (p:Id A t.1 u.1) : 
+corSigProp (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : Sigma A B) (p:Id A t.1 u.1) : 
   prop (IdP (<i>B (p@i)) t.2 u.2) = substInv U prop T0 T1 rem rem1
  where P : Id U (B t.1) (B u.1) = <i>B (p@i)
        T0 : U = IdP P t.2 u.2
@@ -44,7 +42,7 @@ corSigProp (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : sig A B) (p:Id A t.
        v2 : B u.1 = transport P t.2
        rem1 : prop T1 = propSet (B u.1) (pB u.1) v2 u.2
 
-corSigSet (A:U) (B:A-> U) (sB : (x:A) -> set (B x)) (t u : sig A B) (p:Id A t.1 u.1) : 
+corSigSet (A:U) (B:A-> U) (sB : (x:A) -> set (B x)) (t u : Sigma A B) (p:Id A t.1 u.1) : 
   prop (IdP (<i>B (p@i)) t.2 u.2) = substInv U prop T0 T1 rem rem1
  where P : Id U (B t.1) (B u.1) = <i>B (p@i)
        T0 : U = IdP P t.2 u.2
@@ -53,17 +51,17 @@ corSigSet (A:U) (B:A-> U) (sB : (x:A) -> set (B x)) (t u : sig A B) (p:Id A t.1
        v2 : B u.1 = transport P t.2
        rem1 : prop T1 = sB u.1 v2 u.2
 
-setSig (A:U) (B:A-> U) (sA: set A) (sB : (x:A) -> set (B x)) (t u : sig A B) : prop (Id (sig A B) t u) = 
-  substInv U prop (Id (sig A B) t u) ((p:T) * C p) rem3 rem2
+setSig (A:U) (B:A-> U) (sA: set A) (sB : (x:A) -> set (B x)) (t u : Sigma A B) : prop (Id (Sigma A B) t u) = 
+  substInv U prop (Id (Sigma A B) t u) ((p:T) * C p) rem3 rem2
  where
    T : U = Id A t.1 u.1
    C (p:T) : U = IdP (<i> B (p@i)) t.2 u.2
    rem (p : T) : prop (C p) = corSigSet A B sB t u p
    rem1 : prop T = sA t.1 u.1
    rem2 : prop ((p:T) * C p) = propSig T C rem1 rem
-   rem3 : Id U (Id (sig A B) t u) ((p:T) * C p) = lemIdSig A B t u
+   rem3 : Id U (Id (Sigma A B) t u) ((p:T) * C p) = lemIdSig A B t u
 
-corSigGroupoid (A:U) (B:A-> U) (gB : (x:A) -> groupoid (B x)) (t u : sig A B) (p:Id A t.1 u.1) : 
+corSigGroupoid (A:U) (B:A-> U) (gB : (x:A) -> groupoid (B x)) (t u : Sigma A B) (p:Id A t.1 u.1) : 
   set (IdP (<i>B (p@i)) t.2 u.2) = substInv U set T0 T1 rem rem1
  where P : Id U (B t.1) (B u.1) = <i>B (p@i)
        T0 : U = IdP P t.2 u.2
@@ -72,20 +70,20 @@ corSigGroupoid (A:U) (B:A-> U) (gB : (x:A) -> groupoid (B x)) (t u : sig A B) (p
        v2 : B u.1 = transport P t.2
        rem1 : set T1 = gB u.1 v2 u.2
 
-groupoidSig (A:U) (B:A-> U) (gA: groupoid A) (gB : (x:A) -> groupoid (B x)) (t u : sig A B) : set (Id (sig A B) t u) = 
-  substInv U set (Id (sig A B) t u) ((p:T) * C p) rem3 rem2
+groupoidSig (A:U) (B:A-> U) (gA: groupoid A) (gB : (x:A) -> groupoid (B x)) (t u : Sigma A B) : set (Id (Sigma A B) t u) = 
+  substInv U set (Id (Sigma A B) t u) ((p:T) * C p) rem3 rem2
  where
    T : U = Id A t.1 u.1
    C (p:T) : U = IdP (<i> B (p@i)) t.2 u.2
    rem (p : T) : set (C p) = corSigGroupoid A B gB t u p
    rem1 : set T = gA t.1 u.1
    rem2 : set ((p:T) * C p) = setSig T C rem1 rem
-   rem3 : Id U (Id (sig A B) t u) ((p:T) * C p) = lemIdSig A B t u
+   rem3 : Id U (Id (Sigma A B) t u) ((p:T) * C p) = lemIdSig A B t u
 
 lemContr (A:U) (pA:prop A) (a:A) : isContr A = (a,rem)
  where rem (y:A) : Id A a y = pA a y
 
-lem3 (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : sig A B) (p:Id A t.1 u.1) : 
+lem3 (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : Sigma A B) (p:Id A t.1 u.1) : 
   isContr (IdP (<i>B (p@i)) t.2 u.2) = lemContr T0 (substInv U prop T0 T1 rem rem1) rem2
  where P : Id U (B t.1) (B u.1) = <i>B (p@i)
        T0 : U = IdP P t.2 u.2
@@ -103,14 +101,14 @@ lem6 (A:U) (P:A-> U) (cA:(x:A) -> isContr (P x)) : Id U ((x:A)*P x) A = isoId T
    s (z:T) : Id T (g (f z)) z = <i>(z.1,((cA z.1).2 z.2)@ i)
    t (x:A) : Id A (f (g x)) x = refl A x
 
-lemSigProp (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : sig A B) : Id U (Id (sig A B) t u) (Id A t.1 u.1) =
- compId U (Id (sig A B) t u) ((p:Id A t.1 u.1) * IdP (<i> B (p@i)) t.2 u.2) (Id A t.1 u.1) rem2 rem1
+lemSigProp (A:U) (B:A-> U) (pB : (x:A) -> prop (B x)) (t u : Sigma A B) : Id U (Id (Sigma A B) t u) (Id A t.1 u.1) =
+ compId U (Id (Sigma A B) t u) ((p:Id A t.1 u.1) * IdP (<i> B (p@i)) t.2 u.2) (Id A t.1 u.1) rem2 rem1
  where
    T : U = Id A t.1 u.1
    C (p:T) : U = IdP (<i> B (p@i)) t.2 u.2
    rem (p : T) : isContr (C p) = lem3 A B pB t u p
    rem1 : Id U ((p:T) * C p) T = lem6 T C rem
-   rem2 : Id U (Id (sig A B) t u) ((p:T) * C p) = lemIdSig A B t u
+   rem2 : Id U (Id (Sigma A B) t u) ((p:T) * C p) = lemIdSig A B t u
 
 setGroupoid (A:U) (sA:set A) (a0 a1:A) : set (Id A a0 a1) = propSet (Id A a0 a1) (sA a0 a1)
 
diff --git a/examples/univalence.ctt b/examples/univalence.ctt
index 2a18e4f..28b7658 100644
--- a/examples/univalence.ctt
+++ b/examples/univalence.ctt
@@ -41,16 +41,14 @@ isPathContr (A:U) (cA:isContr A) (x y:A) : isContr (Id A x y) =  (p0,q)
 isEquivContr (A B:U) (cA:isContr A) (cB:isContr B) (f:A->B) : isEquiv A B f =
  \ (y:B) -> sigIsContr A (\ (x:A) -> Id B y (f x)) cA (\ (x:A) -> isPathContr B cB y (f x))
 
-sig (A:U) (B:A->U) : U = (x:A) * B x
-
-totalFun (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (w:sig A B) : sig A C =
+totalFun (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (w:Sigma A B) : Sigma A C =
  (w.1,f (w.1) (w.2))
 
 funFib1  (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u:fiber (B x0) (C x0) (f x0) z0) :
- fiber (sig A B) (sig A C) (totalFun A B C f) (x0,z0) =  ((x0,u.1),<i>(x0,u.2@i))
+ fiber (Sigma A B) (Sigma A C) (totalFun A B C f) (x0,z0) =  ((x0,u.1),<i>(x0,u.2@i))
 
 funFib2  (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0)
-         (w : fiber (sig A B) (sig A C) (totalFun A B C f) (x0,z0)) : fiber (B x0) (C x0) (f x0) z0 = (b0,s)
+         (w : fiber (Sigma A B) (Sigma A C) (totalFun A B C f) (x0,z0)) : fiber (B x0) (C x0) (f x0) z0 = (b0,s)
  where
   x : A = w.1.1
   b : B x = w.1.2
@@ -70,18 +68,18 @@ retFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (x0:A) (z0:C x0) (u:fiber
                                       (i = 0) -> <j> z0,
                                       (i = 1) -> <j> f x0 (comp (<k> B x0) u.1 [ (j = 0) -> <k> u.1, (l=1) -> <k>u.1 ]) ])
 
-equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (sig A B)) (cC : isContr (sig A C)) (x:A)
+equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (Sigma A B)) (cC : isContr (Sigma A C)) (x:A)
   : isEquiv (B x) (C x) (f x) =
- \ (z:C x) -> retIsContr (fiber (B x) (C x) (f x) z) (fiber (sig A B) (sig A C) (totalFun A B C f) (x,z))
+ \ (z:C x) -> retIsContr (fiber (B x) (C x) (f x) z) (fiber (Sigma A B) (Sigma A C) (totalFun A B C f) (x,z))
                          (funFib1 A B C f x z)
                          (funFib2 A B C f x z)
                          (retFunFib A B C f x z)
-                         (isEquivContr (sig A B) (sig A C) cB cC (totalFun A B C f) (x,z))
+                         (isEquivContr (Sigma A B) (Sigma A C) cB cC (totalFun A B C f) (x,z))
 
 -- test normal form
--- equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (sig A B)) (cC : isContr (sig A C)) (x:A)
+-- equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (Sigma A B)) (cC : isContr (Sigma A C)) (x:A)
 --   : isEquiv (B x) (C x) (f x) =
---  \ (z:C x) ->  ((comp (<i> B (comp (<j> A) cC.1.1 [ (i = 0) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).1, (i = 1) -> <j> (cC.2 ((x,z)) @ j).1 ])) cB.1.2 [],<i> comp (<j> C (comp (<k> A) cC.1.1 [ (i = 0) -> <k> (cC.2 ((x,z)) @ k).1, (i = 1)(j = 0) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) (comp (<j> C (comp (<k> A) cC.1.1 [ (i = 0) -> <k> (cC.2 ((x,z)) @ (j /\ k)).1, (i = 1) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ k)).1, (j = 0) -> <k> cC.1.1 ])) cC.1.2 [ (i = 0) -> <j> (cC.2 ((x,z)) @ j).2, (i = 1) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (i = 0) -> <j> z, (i = 1) -> <j> f (comp (<k> A) cC.1.1 [ (j = 0) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> <k> (cC.2 ((x,z)) @ k).1 ]) (comp (<k> B (comp (<i> A) cC.1.1 [ (j = 0) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(k = 1) -> <i> (cC.2 ((x,z)) @ i).1, (k = 0) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> <k> cB.1.2 ]) ]),\(x0 : sig (B x) (\(x0 : B x) -> IdP (<i> C x) z (f x x0))) -> <i> (comp (<j> B x) (comp (<j> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> comp (<l> A) cC.1.1 [ (j = 0) -> <l> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ l)).1, (j = 1) -> <l> (cC.2 ((x,z)) @ (k /\ l)).1, (k = 0) -> <l> cC.1.1 ], (i = 1) -> <k> (cC.2 ((x,x0.2 @ -j)) @ k).1, (j = 0) -> <k> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (j = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> <j> comp (<i> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> <j> comp (<k> B x) x0.1 [ (j = 1) -> <k> x0.1 ] ],<k> comp (<l> C x) (comp (<l> C (comp (<j> A) cC.1.1 [ (i = 0) -> <j> comp (<m> A) cC.1.1 [ (j = 0) -> <m> cC.1.1, (k = 0) -> <m> (cC.2 ((x,z)) @ (j /\ m)).1, (k = 1)(l = 0) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (l = 1) -> <m> (cC.2 ((x,z)) @ (j /\ m)).1 ], (i = 1) -> <j> (cC.2 ((x,x0.2 @ (-l /\ k))) @ j).1, (k = 0) -> <j> (cC.2 ((x,z)) @ j).1, (k = 1)(l = 0) -> <j> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ j).1, (l = 1) -> <j> (cC.2 ((x,z)) @ j).1 ])) (comp (<l> C (comp (<j> A) cC.1.1 [ (i = 0) -> <j> comp (<m> A) cC.1.1 [ (j = 0) -> <m> cC.1.1, (k = 0) -> <m> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> <m> cC.1.1 ], (i = 1) -> <j> (cC.2 ((x,x0.2 @ k)) @ (l /\ j)).1, (k = 0) -> <j> (cC.2 ((x,z)) @ (l /\ j)).1, (k = 1) -> <j> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ (l /\ j)).1, (l = 0) -> <j> cC.1.1 ])) cC.1.2 [ (i = 0) -> <l> comp (<j> C (comp (<m> A) cC.1.1 [ (j = 0) -> <m> cC.1.1, (k = 0) -> <m> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> <m> cC.1.1 ])) cC.1.2 [ (k = 0) -> <j> (cC.2 ((x,z)) @ (l /\ j)).2, (k = 1) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j)).2, (l = 0) -> <j> cC.1.2 ], (i = 1) -> <l> (cC.2 ((x,x0.2 @ k)) @ l).2, (k = 0) -> <l> (cC.2 ((x,z)) @ l).2, (k = 1) -> <l> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ l).2 ]) [ (k = 0) -> <l> z, (k = 1) -> <l> f (comp (<k> A) cC.1.1 [ (i = 0) -> <k> comp (<j> A) cC.1.1 [ (k = 0) -> <j> cC.1.1, (l = 0) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> <j> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> <k> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> <k> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (l = 1) -> <k> (cC.2 ((x,z)) @ k).1 ]) (comp (<k> B (comp (<j> A) cC.1.1 [ (i = 0) -> <j> comp (<m> A) cC.1.1 [ (j = 0) -> <m> cC.1.1, (k = 0) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (k = 1)(l = 1) -> <m> (cC.2 ((x,z)) @ (j /\ m)).1, (l = 0) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1 ], (i = 1) -> <j> (cC.2 ((x,x0.2 @ (-l \/ -k))) @ j).1, (k = 0) -> <j> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ j).1, (k = 1)(l = 1) -> <j> (cC.2 ((x,z)) @ j).1, (l = 0) -> <j> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ j).1 ])) (cB.2 ((x,x0.1)) @ i).2 [ (l = 0) -> <k> (cB.2 ((x,x0.1)) @ i).2 ]) ]) [ (i = 0) -> <l> comp (<j> C (comp (<i> A) cC.1.1 [ (j = 0)(k = 1) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1) -> <i> (cC.2 ((x,z)) @ i).1, (k = 0) -> <i> (cC.2 ((x,z)) @ i).1 ])) (comp (<j> C (comp (<i> A) cC.1.1 [ (j = 0) -> <i> cC.1.1, (k = 0) -> <i> (cC.2 ((x,z)) @ (j /\ i)).1, (k = 1) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ i)).1 ])) cC.1.2 [ (k = 0) -> <j> (cC.2 ((x,z)) @ j).2, (k = 1) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (k = 0) -> <j> z, (k = 1) -> <j> f (comp (<l> A) cC.1.1 [ (j = 0) -> <l> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ l).1, (j = 1) -> <l> (cC.2 ((x,z)) @ l).1 ]) (comp (<l> B (comp (<i> A) cC.1.1 [ (j = 0) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(l = 1) -> <i> (cC.2 ((x,z)) @ i).1, (l = 0) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> <l> cB.1.2 ]) ], (i = 1) -> <l> comp (<j> C x) (x0.2 @ k) [ (k = 0) -> <j> z, (k = 1) -> <j> f x (comp (<k> B x) x0.1 [ (j = 0) -> <k> x0.1, (l = 1) -> <k> x0.1 ]), (l = 1) -> <j> x0.2 @ k ], (k = 0) -> <l> z, (k = 1) -> <l> f x (comp (<k> B x) (comp (<l> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> comp (<j> A) cC.1.1 [ (k = 0) -> <j> cC.1.1, (l = 0) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> <j> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> <k> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> <k> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (l = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> <k> comp (<i> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> <k> comp (<j> B x) x0.1 [ (k = 1)(l = 1) -> <j> x0.1 ], (l = 0) -> <k> comp (<l> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> comp (<j> A) cC.1.1 [ (k = 0) -> <j> cC.1.1, (l = 0) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> <j> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> <k> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> <k> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (l = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 [] ]) ]))
+--  \ (z:C x) ->  ((comp (<i> B (comp (<j> A) cC.1.1 [ (i = 0) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).1, (i = 1) -> <j> (cC.2 ((x,z)) @ j).1 ])) cB.1.2 [],<i> comp (<j> C (comp (<k> A) cC.1.1 [ (i = 0) -> <k> (cC.2 ((x,z)) @ k).1, (i = 1)(j = 0) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) (comp (<j> C (comp (<k> A) cC.1.1 [ (i = 0) -> <k> (cC.2 ((x,z)) @ (j /\ k)).1, (i = 1) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ k)).1, (j = 0) -> <k> cC.1.1 ])) cC.1.2 [ (i = 0) -> <j> (cC.2 ((x,z)) @ j).2, (i = 1) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (i = 0) -> <j> z, (i = 1) -> <j> f (comp (<k> A) cC.1.1 [ (j = 0) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> <k> (cC.2 ((x,z)) @ k).1 ]) (comp (<k> B (comp (<i> A) cC.1.1 [ (j = 0) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(k = 1) -> <i> (cC.2 ((x,z)) @ i).1, (k = 0) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> <k> cB.1.2 ]) ]),\(x0 : Sigma (B x) (\(x0 : B x) -> IdP (<i> C x) z (f x x0))) -> <i> (comp (<j> B x) (comp (<j> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> comp (<l> A) cC.1.1 [ (j = 0) -> <l> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ l)).1, (j = 1) -> <l> (cC.2 ((x,z)) @ (k /\ l)).1, (k = 0) -> <l> cC.1.1 ], (i = 1) -> <k> (cC.2 ((x,x0.2 @ -j)) @ k).1, (j = 0) -> <k> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (j = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> <j> comp (<i> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> <j> comp (<k> B x) x0.1 [ (j = 1) -> <k> x0.1 ] ],<k> comp (<l> C x) (comp (<l> C (comp (<j> A) cC.1.1 [ (i = 0) -> <j> comp (<m> A) cC.1.1 [ (j = 0) -> <m> cC.1.1, (k = 0) -> <m> (cC.2 ((x,z)) @ (j /\ m)).1, (k = 1)(l = 0) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (l = 1) -> <m> (cC.2 ((x,z)) @ (j /\ m)).1 ], (i = 1) -> <j> (cC.2 ((x,x0.2 @ (-l /\ k))) @ j).1, (k = 0) -> <j> (cC.2 ((x,z)) @ j).1, (k = 1)(l = 0) -> <j> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ j).1, (l = 1) -> <j> (cC.2 ((x,z)) @ j).1 ])) (comp (<l> C (comp (<j> A) cC.1.1 [ (i = 0) -> <j> comp (<m> A) cC.1.1 [ (j = 0) -> <m> cC.1.1, (k = 0) -> <m> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> <m> cC.1.1 ], (i = 1) -> <j> (cC.2 ((x,x0.2 @ k)) @ (l /\ j)).1, (k = 0) -> <j> (cC.2 ((x,z)) @ (l /\ j)).1, (k = 1) -> <j> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ (l /\ j)).1, (l = 0) -> <j> cC.1.1 ])) cC.1.2 [ (i = 0) -> <l> comp (<j> C (comp (<m> A) cC.1.1 [ (j = 0) -> <m> cC.1.1, (k = 0) -> <m> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> <m> cC.1.1 ])) cC.1.2 [ (k = 0) -> <j> (cC.2 ((x,z)) @ (l /\ j)).2, (k = 1) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j)).2, (l = 0) -> <j> cC.1.2 ], (i = 1) -> <l> (cC.2 ((x,x0.2 @ k)) @ l).2, (k = 0) -> <l> (cC.2 ((x,z)) @ l).2, (k = 1) -> <l> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ l).2 ]) [ (k = 0) -> <l> z, (k = 1) -> <l> f (comp (<k> A) cC.1.1 [ (i = 0) -> <k> comp (<j> A) cC.1.1 [ (k = 0) -> <j> cC.1.1, (l = 0) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> <j> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> <k> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> <k> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (l = 1) -> <k> (cC.2 ((x,z)) @ k).1 ]) (comp (<k> B (comp (<j> A) cC.1.1 [ (i = 0) -> <j> comp (<m> A) cC.1.1 [ (j = 0) -> <m> cC.1.1, (k = 0) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (k = 1)(l = 1) -> <m> (cC.2 ((x,z)) @ (j /\ m)).1, (l = 0) -> <m> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1 ], (i = 1) -> <j> (cC.2 ((x,x0.2 @ (-l \/ -k))) @ j).1, (k = 0) -> <j> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ j).1, (k = 1)(l = 1) -> <j> (cC.2 ((x,z)) @ j).1, (l = 0) -> <j> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ j).1 ])) (cB.2 ((x,x0.1)) @ i).2 [ (l = 0) -> <k> (cB.2 ((x,x0.1)) @ i).2 ]) ]) [ (i = 0) -> <l> comp (<j> C (comp (<i> A) cC.1.1 [ (j = 0)(k = 1) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1) -> <i> (cC.2 ((x,z)) @ i).1, (k = 0) -> <i> (cC.2 ((x,z)) @ i).1 ])) (comp (<j> C (comp (<i> A) cC.1.1 [ (j = 0) -> <i> cC.1.1, (k = 0) -> <i> (cC.2 ((x,z)) @ (j /\ i)).1, (k = 1) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ i)).1 ])) cC.1.2 [ (k = 0) -> <j> (cC.2 ((x,z)) @ j).2, (k = 1) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (k = 0) -> <j> z, (k = 1) -> <j> f (comp (<l> A) cC.1.1 [ (j = 0) -> <l> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ l).1, (j = 1) -> <l> (cC.2 ((x,z)) @ l).1 ]) (comp (<l> B (comp (<i> A) cC.1.1 [ (j = 0) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(l = 1) -> <i> (cC.2 ((x,z)) @ i).1, (l = 0) -> <i> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> <l> cB.1.2 ]) ], (i = 1) -> <l> comp (<j> C x) (x0.2 @ k) [ (k = 0) -> <j> z, (k = 1) -> <j> f x (comp (<k> B x) x0.1 [ (j = 0) -> <k> x0.1, (l = 1) -> <k> x0.1 ]), (l = 1) -> <j> x0.2 @ k ], (k = 0) -> <l> z, (k = 1) -> <l> f x (comp (<k> B x) (comp (<l> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> comp (<j> A) cC.1.1 [ (k = 0) -> <j> cC.1.1, (l = 0) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> <j> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> <k> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> <k> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (l = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> <k> comp (<i> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> <k> comp (<j> B x) x0.1 [ (k = 1)(l = 1) -> <j> x0.1 ], (l = 0) -> <k> comp (<l> B (comp (<k> A) cC.1.1 [ (i = 0) -> <k> comp (<j> A) cC.1.1 [ (k = 0) -> <j> cC.1.1, (l = 0) -> <j> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> <j> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> <k> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> <k> (cC.2 (((cB.2 ((x,x0.1)) @ i).1,f (cB.2 ((x,x0.1)) @ i).1 (cB.2 ((x,x0.1)) @ i).2)) @ k).1, (l = 1) -> <k> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 [] ]) ]))
 
 lem1 (B:U) : isContr ((X:U) * equiv X B) =
  ((B,idEquiv B)