From ce9c32564146d174c10993a119556a397a1ee18b Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 14 Jan 2016 10:33:23 -0500 Subject: [PATCH] rename sig to Sigma and make setquot compile --- examples/prelude.ctt | 2 ++ examples/setquot.ctt | 53 +++++++++++++++++++++-------------------- examples/sigma.ctt | 38 ++++++++++++++--------------- examples/univalence.ctt | 18 +++++++------- 4 files changed, 55 insertions(+), 56 deletions(-) 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) = 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 = foo true' (K' true') - -- Tests of checking normal forms: -ntrue' : bool' = (\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ])) +ntrue' : bool' = (\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P : Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (Sigma bool (\(x : bool) -> IdP ( bool) true x)) -> P.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ])) --- Why is this not working? Bug in pretty printer? --- ntest : (P' true').1 = \(P : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : or (IdP ( sig (bool -> (sig U (\(X : U) -> (a b : X) -> IdP ( X) a b))) (\(A : bool -> (sig U (\(X : U) -> (a b : X) -> IdP ( X) a b))) -> sig (sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) (\(_ : sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) -> (x1 x2 : bool) -> (A x1).1 -> ((A x2).1 -> (IdP ( bool) x1 x2))))) ((\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ]))) ((\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ]))), IdP ( sig (bool -> (sig U (\(X : U) -> (a b : X) -> IdP ( X) a b))) (\(A : bool -> (sig U (\(X : U) -> (a b : X) -> IdP ( X) a b))) -> sig (sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) (\(_ : sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) -> (x1 x2 : bool) -> (A x1).1 -> ((A x2).1 -> (IdP ( bool) x1 x2))))) ((\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ]))) ((\(x : bool) -> (IdP ( bool) false x,lem7 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) false x)) -> P0.1) -> f ((false, false)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) false x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> false, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) false x1) -> \(X2 : IdP ( bool) false x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ])))) -> P.1) -> f (inl ( (\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f0 : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f0 ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> 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 ( 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 ( X) a b)) -> \(f : or (IdP ( Sigma (bool -> (Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b))) (\(A : bool -> (Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b))) -> Sigma (Sigma ((P0 : Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) (\(_ : Sigma ((P0 : Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) -> (x1 x2 : bool) -> (A x1).1 -> ((A x2).1 -> (IdP ( bool) x1 x2))))) ((\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (Sigma bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ !0) [ (!0 = 0) -> true, (!0 = 1) -> X1 @ !1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -!0) [ (!0 = 0) -> x1, (!0 = 1) -> X2 @ !1 ]))) ((\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (Sigma bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ !0) [ (!0 = 0) -> true, (!0 = 1) -> X1 @ !1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -!0) [ (!0 = 0) -> x1, (!0 = 1) -> X2 @ !1 ])))) IdP ( Sigma (bool -> (Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b))) (\(A : bool -> (Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b))) -> Sigma (Sigma ((P0 : Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) (\(_ : Sigma ((P0 : Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((Sigma bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) -> (x1 x2 : bool) -> (A x1).1 -> ((A x2).1 -> (IdP ( bool) x1 x2))))) ((\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (Sigma bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ !0) [ (!0 = 0) -> true, (!0 = 1) -> X1 @ !1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -!0) [ (!0 = 0) -> x1, (!0 = 1) -> X2 @ !1 ]))) ((\(x : bool) -> (IdP ( bool) false x,lem7 x),((\(P0 : Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (Sigma bool (\(x : bool) -> IdP ( bool) false x)) -> P0.1) -> f ((false, false)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) false x1) -> comp ( bool) (X2 @ !0) [ (!0 = 0) -> false, (!0 = 1) -> X1 @ !1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) false x1) -> \(X2 : IdP ( bool) false x2) -> comp ( bool) (X1 @ -!0) [ (!0 = 0) -> x1, (!0 = 1) -> X2 @ !1 ]))) -> P.1) -> f (inl ( (\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : Sigma U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f0 : (Sigma bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f0 ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ !0) [ (!0 = 0) -> true, (!0 = 1) -> X1 @ !1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -!0) [ (!0 = 0) -> x1, (!0 = 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 ( 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 ( 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 ( B (p@i)) t.2 u.2 f (q:T0) : T1 = ( (q@i).1, (q@i).2) g (z:T1) : T0 = (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 = (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 ( P (p@i)) u0 u1) (Id (P a1) (transport ( P (p@i)) u0) u1) = IdP (P (p@j\/i)) (comp (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 (B (p@i)) t.2 u.2) (Id (B u.1) (transport (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 (B (p@i)) t.2 u.2) = substInv U prop T0 T1 rem rem1 where P : Id U (B t.1) (B u.1) = 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 (B (p@i)) t.2 u.2) = substInv U prop T0 T1 rem rem1 where P : Id U (B t.1) (B u.1) = 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 ( 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 (B (p@i)) t.2 u.2) = substInv U set T0 T1 rem rem1 where P : Id U (B t.1) (B u.1) = 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 ( 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 (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) = 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 = (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 ( 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 ( 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 ( 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),(x0,u.2@i)) + fiber (Sigma A B) (Sigma A C) (totalFun A B C f) (x0,z0) = ((x0,u.1),(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) -> z0, (i = 1) -> f x0 (comp ( B x0) u.1 [ (j = 0) -> u.1, (l=1) -> 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 ( B (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).1, (i = 1) -> (cC.2 ((x,z)) @ j).1 ])) cB.1.2 [], comp ( C (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((x,z)) @ k).1, (i = 1)(j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> (cC.2 ((x,z)) @ k).1 ])) (comp ( C (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((x,z)) @ (j /\ k)).1, (i = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ k)).1, (j = 0) -> cC.1.1 ])) cC.1.2 [ (i = 0) -> (cC.2 ((x,z)) @ j).2, (i = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (i = 0) -> z, (i = 1) -> f (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> (cC.2 ((x,z)) @ k).1 ]) (comp ( B (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(k = 1) -> (cC.2 ((x,z)) @ i).1, (k = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> cB.1.2 ]) ]),\(x0 : sig (B x) (\(x0 : B x) -> IdP ( C x) z (f x x0))) -> (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ l)).1, (j = 1) -> (cC.2 ((x,z)) @ (k /\ l)).1, (k = 0) -> cC.1.1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -j)) @ k).1, (j = 0) -> (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) -> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> comp ( B (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> comp ( B x) x0.1 [ (j = 1) -> x0.1 ] ], comp ( C x) (comp ( C (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (j /\ m)).1, (k = 1)(l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (l = 1) -> (cC.2 ((x,z)) @ (j /\ m)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ (-l /\ k))) @ j).1, (k = 0) -> (cC.2 ((x,z)) @ j).1, (k = 1)(l = 0) -> (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) -> (cC.2 ((x,z)) @ j).1 ])) (comp ( C (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> cC.1.1 ], (i = 1) -> (cC.2 ((x,x0.2 @ k)) @ (l /\ j)).1, (k = 0) -> (cC.2 ((x,z)) @ (l /\ j)).1, (k = 1) -> (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) -> cC.1.1 ])) cC.1.2 [ (i = 0) -> comp ( C (comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> cC.1.1 ])) cC.1.2 [ (k = 0) -> (cC.2 ((x,z)) @ (l /\ j)).2, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j)).2, (l = 0) -> cC.1.2 ], (i = 1) -> (cC.2 ((x,x0.2 @ k)) @ l).2, (k = 0) -> (cC.2 ((x,z)) @ l).2, (k = 1) -> (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) -> z, (k = 1) -> f (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (k = 0) -> cC.1.1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> (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) -> (cC.2 ((x,z)) @ k).1 ]) (comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (k = 1)(l = 1) -> (cC.2 ((x,z)) @ (j /\ m)).1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ (-l \/ -k))) @ j).1, (k = 0) -> (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) -> (cC.2 ((x,z)) @ j).1, (l = 0) -> (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) -> (cB.2 ((x,x0.1)) @ i).2 ]) ]) [ (i = 0) -> comp ( C (comp ( A) cC.1.1 [ (j = 0)(k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1) -> (cC.2 ((x,z)) @ i).1, (k = 0) -> (cC.2 ((x,z)) @ i).1 ])) (comp ( C (comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (j /\ i)).1, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ i)).1 ])) cC.1.2 [ (k = 0) -> (cC.2 ((x,z)) @ j).2, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (k = 0) -> z, (k = 1) -> f (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ l).1, (j = 1) -> (cC.2 ((x,z)) @ l).1 ]) (comp ( B (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(l = 1) -> (cC.2 ((x,z)) @ i).1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> cB.1.2 ]) ], (i = 1) -> comp ( C x) (x0.2 @ k) [ (k = 0) -> z, (k = 1) -> f x (comp ( B x) x0.1 [ (j = 0) -> x0.1, (l = 1) -> x0.1 ]), (l = 1) -> x0.2 @ k ], (k = 0) -> z, (k = 1) -> f x (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (k = 0) -> cC.1.1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> (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) -> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> comp ( B (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> comp ( B x) x0.1 [ (k = 1)(l = 1) -> x0.1 ], (l = 0) -> comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (k = 0) -> cC.1.1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> (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) -> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 [] ]) ])) +-- \ (z:C x) -> ((comp ( B (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).1, (i = 1) -> (cC.2 ((x,z)) @ j).1 ])) cB.1.2 [], comp ( C (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((x,z)) @ k).1, (i = 1)(j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> (cC.2 ((x,z)) @ k).1 ])) (comp ( C (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((x,z)) @ (j /\ k)).1, (i = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ k)).1, (j = 0) -> cC.1.1 ])) cC.1.2 [ (i = 0) -> (cC.2 ((x,z)) @ j).2, (i = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (i = 0) -> z, (i = 1) -> f (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (j = 1) -> (cC.2 ((x,z)) @ k).1 ]) (comp ( B (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(k = 1) -> (cC.2 ((x,z)) @ i).1, (k = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> cB.1.2 ]) ]),\(x0 : Sigma (B x) (\(x0 : B x) -> IdP ( C x) z (f x x0))) -> (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ l)).1, (j = 1) -> (cC.2 ((x,z)) @ (k /\ l)).1, (k = 0) -> cC.1.1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -j)) @ k).1, (j = 0) -> (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) -> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> comp ( B (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> comp ( B x) x0.1 [ (j = 1) -> x0.1 ] ], comp ( C x) (comp ( C (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (j /\ m)).1, (k = 1)(l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (l = 1) -> (cC.2 ((x,z)) @ (j /\ m)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ (-l /\ k))) @ j).1, (k = 0) -> (cC.2 ((x,z)) @ j).1, (k = 1)(l = 0) -> (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) -> (cC.2 ((x,z)) @ j).1 ])) (comp ( C (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> cC.1.1 ], (i = 1) -> (cC.2 ((x,x0.2 @ k)) @ (l /\ j)).1, (k = 0) -> (cC.2 ((x,z)) @ (l /\ j)).1, (k = 1) -> (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) -> cC.1.1 ])) cC.1.2 [ (i = 0) -> comp ( C (comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (l /\ j /\ m)).1, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j /\ m)).1, (l = 0) -> cC.1.1 ])) cC.1.2 [ (k = 0) -> (cC.2 ((x,z)) @ (l /\ j)).2, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (l /\ j)).2, (l = 0) -> cC.1.2 ], (i = 1) -> (cC.2 ((x,x0.2 @ k)) @ l).2, (k = 0) -> (cC.2 ((x,z)) @ l).2, (k = 1) -> (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) -> z, (k = 1) -> f (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (k = 0) -> cC.1.1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> (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) -> (cC.2 ((x,z)) @ k).1 ]) (comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1, (k = 1)(l = 1) -> (cC.2 ((x,z)) @ (j /\ m)).1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ m)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ (-l \/ -k))) @ j).1, (k = 0) -> (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) -> (cC.2 ((x,z)) @ j).1, (l = 0) -> (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) -> (cB.2 ((x,x0.1)) @ i).2 ]) ]) [ (i = 0) -> comp ( C (comp ( A) cC.1.1 [ (j = 0)(k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1) -> (cC.2 ((x,z)) @ i).1, (k = 0) -> (cC.2 ((x,z)) @ i).1 ])) (comp ( C (comp ( A) cC.1.1 [ (j = 0) -> cC.1.1, (k = 0) -> (cC.2 ((x,z)) @ (j /\ i)).1, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (j /\ i)).1 ])) cC.1.2 [ (k = 0) -> (cC.2 ((x,z)) @ j).2, (k = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ j).2 ]) [ (k = 0) -> z, (k = 1) -> f (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ l).1, (j = 1) -> (cC.2 ((x,z)) @ l).1 ]) (comp ( B (comp ( A) cC.1.1 [ (j = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1, (j = 1)(l = 1) -> (cC.2 ((x,z)) @ i).1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ i).1 ])) cB.1.2 [ (j = 0) -> cB.1.2 ]) ], (i = 1) -> comp ( C x) (x0.2 @ k) [ (k = 0) -> z, (k = 1) -> f x (comp ( B x) x0.1 [ (j = 0) -> x0.1, (l = 1) -> x0.1 ]), (l = 1) -> x0.2 @ k ], (k = 0) -> z, (k = 1) -> f x (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (k = 0) -> cC.1.1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> (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) -> (cC.2 ((x,z)) @ k).1 ])) (cB.2 ((x,x0.1)) @ i).2 []) [ (i = 0) -> comp ( B (comp ( A) cC.1.1 [ (i = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ k).1, (i = 1) -> (cC.2 ((x,z)) @ k).1 ])) cB.1.2 [], (i = 1) -> comp ( B x) x0.1 [ (k = 1)(l = 1) -> x0.1 ], (l = 0) -> comp ( B (comp ( A) cC.1.1 [ (i = 0) -> comp ( A) cC.1.1 [ (k = 0) -> cC.1.1, (l = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (k /\ j)).1, (l = 1) -> (cC.2 ((x,z)) @ (k /\ j)).1 ], (i = 1) -> (cC.2 ((x,x0.2 @ -l)) @ k).1, (l = 0) -> (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) -> (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) -- 2.34.1