From: Anders Mörtberg Date: Thu, 7 Jul 2016 11:32:35 +0000 (+0200) Subject: remove duplicate code X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=098a24249fe86fad5e9e3d8cba4f3ec55b5d9374;p=cubicaltt.git remove duplicate code --- diff --git a/examples/collection.ctt b/examples/collection.ctt index d68f710..bb751dd 100644 --- a/examples/collection.ctt +++ b/examples/collection.ctt @@ -1,53 +1,35 @@ +-- This file proves that the collection of all sets is a groupoid module collection where -import prelude -import equiv import univalence import sigma import pi --- import testContr -propIsContr (A:U) (z0 z1 : isContr A) : Id (isContr A) z0 z1 = - (p0 a1@j, - \ (x:A) -> - comp (<_>A) (lem1 x@i@j) [ (i=0) -> p0 a1@j, (i=1) -> p0 x@(j\/k), - (j=0) -> p0 x@(i/\k), (j=1) -> p1 x@i ]) - where - a0 : A = z0.1 - p0 : (x:A) -> Id A a0 x = z0.2 - a1 : A = z1.1 - p1 : (x:A) -> Id A a1 x = z1.2 - lem1 (x:A) : IdP (Id A a0 (p1 x@i)) (p0 a1) (p0 x) = p0 (p1 x@i) @ j - -propIsEquiv (A B : U) (f : A -> B) - : prop (isEquiv A B f) = \ (u0 u1:isEquiv A B f) -> \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i +setFun (A B : U) (sB : set B) : set (A -> B) = + setPi A (\(x : A) -> B) (\(x : A) -> sB) -setFun (A B:U) (sB: set B) : set (A -> B) = setPi A (\ (x:A) -> B) (\ (x:A) -> sB) +eqEquivFst (A B : U) : (t u : equiv A B) -> + Id U (Id (equiv A B) t u) (Id (A -> B) t.1 u.1) + = lemSigProp (A -> B) (isEquiv A B) (propIsEquiv A B) -groupoidFun (A B : U) (gB:groupoid B) : groupoid (A -> B) = groupoidPi A (\ (x:A) -> B) (\ (x:A) -> gB) +-- groupoidFun (A B : U) (gB:groupoid B) : groupoid (A -> B) = +-- groupoidPi A (\(x : A) -> B) (\(x : A) -> gB) -lem3 (A B : U) (t u : equiv A B) : Id U (Id (equiv A B) t u) (Id (A -> B) t.1 u.1) - = lemSigProp (A->B) (isEquiv A B) (propIsEquiv A B) t u +-- lem5 (A B : U) (gB:groupoid B) (t u:equiv A B) : set (Id (equiv A B) t u) +-- = substInv U set (Id (equiv A B) t u) (Id (A -> B) t.1 u.1) +-- (eqEquivFst A B t u) (groupoidFun A B gB t.1 u.1) -lem4 (A B : U) (sB:set B) (t u:equiv A B) : prop (Id (equiv A B) t u) - = substInv U prop (Id (equiv A B) t u) (Id (A -> B) t.1 u.1) (lem3 A B t u) (setFun A B sB t.1 u.1) - -lem5 (A B : U) (gB:groupoid B) (t u:equiv A B) : set (Id (equiv A B) t u) - = substInv U set (Id (equiv A B) t u) (Id (A -> B) t.1 u.1) (lem3 A B t u) (groupoidFun A B gB t.1 u.1) - -lem6 (A B : U) (sB : set B) : set (Id U A B) = - substInv U set (Id U A B) (equiv A B) (corrUniv A B ) (lem4 A B sB) - --- the collection of all sets - -SET : U = (X:U) * set X +setId (A B : U) (sB : set B) : set (Id U A B) = + substInv U set (Id U A B) (equiv A B) (corrUniv A B) (rem A B sB) + where + rem (A B : U) (sB:set B) (t u:equiv A B) : prop (Id (equiv A B) t u) + = substInv U prop (Id (equiv A B) t u) (Id (A -> B) t.1 u.1) + (eqEquivFst A B t u) (setFun A B sB t.1 u.1) -- the collection of all sets is a groupoid - -groupoidSET (A B : SET) : set (Id SET A B) = - rem2 - where - rem : set (Id U A.1 B.1) = lem6 A.1 B.1 B.2 - rem1 : Id U (Id SET A B) (Id U A.1 B.1) = lemSigProp U set setIsProp A B - rem2 : set (Id SET A B) = substInv U set (Id SET A B) (Id U A.1 B.1) rem1 rem +groupoidSET : groupoid SET = \(A B : SET) -> + let rem : set (Id U A.1 B.1) = setId A.1 B.1 B.2 + rem1 : Id U (Id SET A B) (Id U A.1 B.1) = + lemSigProp U set setIsProp A B + in substInv U set (Id SET A B) (Id U A.1 B.1) rem1 rem diff --git a/examples/equiv.ctt b/examples/equiv.ctt index d8c1105..d8280fe 100644 --- a/examples/equiv.ctt +++ b/examples/equiv.ctt @@ -13,7 +13,8 @@ equiv (A B : U) : U = (f : A -> B) * isEquiv A B f propIsEquiv (A B : U) (f : A -> B) : prop (isEquiv A B f) = - \ (u0 u1:isEquiv A B f) -> \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i + \ (u0 u1:isEquiv A B f) -> + \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i equivLemma (A B : U) : (v w : equiv A B) -> Id (A -> B) v.1 w.1 -> Id (equiv A B) v w diff --git a/examples/prelude.ctt b/examples/prelude.ctt index 4ead1a8..dd1fc1b 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -136,6 +136,9 @@ prop (A : U) : U = (a b : A) -> Id A a b set (A : U) : U = (a b : A) -> prop (Id A a b) groupoid (A : U) : U = (a b : A) -> set (Id A a b) +-- the collection of all sets +SET : U = (X:U) * set X + propSet (A : U) (h : prop A) : set A = \(a b : A) (p q : Id A a b) -> comp (A) a [ (i=0) -> h a a diff --git a/examples/sigma.ctt b/examples/sigma.ctt index 4277784..51f1534 100644 --- a/examples/sigma.ctt +++ b/examples/sigma.ctt @@ -3,8 +3,6 @@ module sigma where import prelude import equiv --- application of this fact - 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 @@ -18,15 +16,6 @@ lemIdSig (A:U) (B : A -> U) (t u : Sigma A B) : lemIdAnd (A B : U) (t u : and A B) : Id U (Id (and A B) t u) (and (Id A t.1 u.1) (Id B t.2 u.2)) = lemIdSig A (\(_ : A) -> B) t u -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 : Sigma A B) : Id (Sigma A B) t u - = lem A B pB t u (pA t.1 u.1) - -propAnd (A:U) (B:U) (pA:prop A) (pB:prop B) : prop (and A B) - = propSig A (\(_:A)->B) pA (\(_:A)->pB) - lemTransp (A:U) (a:A) : Id A a (transport (<_>A) a) = fill (<_>A) a [] funDepTr (A:U) (P:A->U) (a0 a1 :A) (p:Id A a0 a1) (u0:P a0) (u1:P a1) : diff --git a/examples/univalence.ctt b/examples/univalence.ctt index 95d71e0..97cf7f2 100644 --- a/examples/univalence.ctt +++ b/examples/univalence.ctt @@ -78,7 +78,7 @@ equivFunFib (A:U) (B C : A->U) (f : (x:A) -> B x -> C x) (cB : isContr (Sigma A (isEquivContr (Sigma A B) (Sigma A C) cB cC (totalFun A B C f) (x,z)) -- test normal form -nequivFunFib : (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) = \(A : U) -> \(B C : A -> U) -> \(f : (x : A) -> (B x) -> (C x)) -> \(cB : Sigma (Sigma A (\(x : A) -> B x)) (\(x : Sigma A (\(x : A) -> B x)) -> (y : Sigma A (\(x0 : A) -> B x0)) -> IdP ( Sigma A (\(x0 : A) -> B x0)) x y)) -> \(cC : Sigma (Sigma A (\(x : A) -> C x)) (\(x : Sigma A (\(x : A) -> C x)) -> (y : Sigma A (\(x0 : A) -> C x0)) -> IdP ( Sigma A (\(x0 : A) -> C x0)) x y)) -> \(x : A) -> \(z : C x) -> ((comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((x,z)) @ !2).1, (!0 = 1)(!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((x,z)) @ (!1 /\ !2)).1, (!0 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!1 /\ !2)).1, (!1 = 0) -> cC.1.1 ])) cC.1.2 [ (!0 = 0) -> (cC.2 ((x,z)) @ !1).2, (!0 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).2 ]) [ (!0 = 0) -> z, (!0 = 1) -> f (comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ]) (comp ( B (comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).1, (!1 = 1)(!2 = 1) -> (cC.2 ((x,z)) @ !3).1, (!2 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).1 ])) cB.1.2 [ (!1 = 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 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 []) [ (!0 = 0) -> comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], (!0 = 1) -> comp ( B x) x0.1 [ (!1 = 1) -> x0.1 ] ], comp ( C x) (comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!2 = 1)(!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!4 /\ !5)).1, (!3 = 1) -> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!4 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ (!2 /\ -!3))) @ !4).1, (!2 = 0) -> (cC.2 ((x,z)) @ !4).1, (!2 = 1)(!3 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ])) (comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4 /\ !5)).1, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4 /\ !5)).1, (!3 = 0) -> cC.1.1, (!4 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ !2)) @ (!3 /\ !4)).1, (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4)).1, (!2 = 1) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ (!3 /\ !4)).1, (!3 = 0) -> cC.1.1 ])) cC.1.2 [ (!0 = 0) -> comp ( C (comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4 /\ !5)).1, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4 /\ !5)).1, (!3 = 0) -> cC.1.1, (!4 = 0) -> cC.1.1 ])) cC.1.2 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4)).2, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4)).2, (!3 = 0) -> cC.1.2 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ !2)) @ !3).2, (!2 = 0) -> (cC.2 ((x,z)) @ !3).2, (!2 = 1) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !3).2 ]) [ (!2 = 0) -> z, (!2 = 1) -> f (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!4 /\ !5)).1, (!3 = 1) -> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!4 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!3)) @ !4).1, (!3 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ]) (comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!5 /\ !6)).1, (!3 = 1)(!4 = 1) -> (cC.2 ((x,z)) @ (!5 /\ !6)).1, (!4 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!5 /\ !6)).1, (!5 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ (-!3 \/ -!4))) @ !5).1, (!3 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !5).1, (!3 = 1)(!4 = 1) -> (cC.2 ((x,z)) @ !5).1, (!4 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !5).1 ])) (cB.2 ((x,x0.1)) @ !0).2 [ (!3 = 0) -> (cB.2 ((x,x0.1)) @ !0).2 ]) ]) [ (!0 = 0) -> comp ( C (comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ !4).1, (!2 = 1)(!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ])) (comp ( C (comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4)).1, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4)).1, (!3 = 0) -> cC.1.1 ])) cC.1.2 [ (!2 = 0) -> (cC.2 ((x,z)) @ !3).2, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).2 ]) [ (!2 = 0) -> z, (!2 = 1) -> f (comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ]) (comp ( B (comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !5).1, (!3 = 1)(!4 = 1) -> (cC.2 ((x,z)) @ !5).1, (!4 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !5).1 ])) cB.1.2 [ (!3 = 0) -> cB.1.2 ]) ], (!0 = 1) -> comp ( C x) (x0.2 @ !2) [ (!2 = 0) -> z, (!2 = 1) -> f x (comp ( B x) x0.1 [ (!3 = 1) -> x0.1, (!4 = 0) -> x0.1 ]), (!3 = 1) -> x0.2 @ !2 ], (!2 = 0) -> z, (!2 = 1) -> f x (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 []) [ (!0 = 0) -> comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], (!0 = 1) -> comp ( B x) x0.1 [ (!3 = 1)(!4 = 1) -> x0.1 ], (!3 = 0) -> comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 [] ]) ])) +-- nequivFunFib : (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) = \(A : U) -> \(B C : A -> U) -> \(f : (x : A) -> (B x) -> (C x)) -> \(cB : Sigma (Sigma A (\(x : A) -> B x)) (\(x : Sigma A (\(x : A) -> B x)) -> (y : Sigma A (\(x0 : A) -> B x0)) -> IdP ( Sigma A (\(x0 : A) -> B x0)) x y)) -> \(cC : Sigma (Sigma A (\(x : A) -> C x)) (\(x : Sigma A (\(x : A) -> C x)) -> (y : Sigma A (\(x0 : A) -> C x0)) -> IdP ( Sigma A (\(x0 : A) -> C x0)) x y)) -> \(x : A) -> \(z : C x) -> ((comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((x,z)) @ !2).1, (!0 = 1)(!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((x,z)) @ (!1 /\ !2)).1, (!0 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!1 /\ !2)).1, (!1 = 0) -> cC.1.1 ])) cC.1.2 [ (!0 = 0) -> (cC.2 ((x,z)) @ !1).2, (!0 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).2 ]) [ (!0 = 0) -> z, (!0 = 1) -> f (comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ]) (comp ( B (comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).1, (!1 = 1)(!2 = 1) -> (cC.2 ((x,z)) @ !3).1, (!2 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).1 ])) cB.1.2 [ (!1 = 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 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 []) [ (!0 = 0) -> comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], (!0 = 1) -> comp ( B x) x0.1 [ (!1 = 1) -> x0.1 ] ], comp ( C x) (comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!2 = 1)(!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!4 /\ !5)).1, (!3 = 1) -> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!4 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ (!2 /\ -!3))) @ !4).1, (!2 = 0) -> (cC.2 ((x,z)) @ !4).1, (!2 = 1)(!3 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ])) (comp ( C (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4 /\ !5)).1, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4 /\ !5)).1, (!3 = 0) -> cC.1.1, (!4 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ !2)) @ (!3 /\ !4)).1, (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4)).1, (!2 = 1) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ (!3 /\ !4)).1, (!3 = 0) -> cC.1.1 ])) cC.1.2 [ (!0 = 0) -> comp ( C (comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4 /\ !5)).1, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4 /\ !5)).1, (!3 = 0) -> cC.1.1, (!4 = 0) -> cC.1.1 ])) cC.1.2 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4)).2, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4)).2, (!3 = 0) -> cC.1.2 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ !2)) @ !3).2, (!2 = 0) -> (cC.2 ((x,z)) @ !3).2, (!2 = 1) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !3).2 ]) [ (!2 = 0) -> z, (!2 = 1) -> f (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!4 /\ !5)).1, (!3 = 1) -> (cC.2 ((x,z)) @ (!4 /\ !5)).1, (!4 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!3)) @ !4).1, (!3 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ]) (comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!5 /\ !6)).1, (!3 = 1)(!4 = 1) -> (cC.2 ((x,z)) @ (!5 /\ !6)).1, (!4 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!5 /\ !6)).1, (!5 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ (-!3 \/ -!4))) @ !5).1, (!3 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !5).1, (!3 = 1)(!4 = 1) -> (cC.2 ((x,z)) @ !5).1, (!4 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !5).1 ])) (cB.2 ((x,x0.1)) @ !0).2 [ (!3 = 0) -> (cB.2 ((x,x0.1)) @ !0).2 ]) ]) [ (!0 = 0) -> comp ( C (comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ !4).1, (!2 = 1)(!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ])) (comp ( C (comp ( A) cC.1.1 [ (!2 = 0) -> (cC.2 ((x,z)) @ (!3 /\ !4)).1, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!3 /\ !4)).1, (!3 = 0) -> cC.1.1 ])) cC.1.2 [ (!2 = 0) -> (cC.2 ((x,z)) @ !3).2, (!2 = 1) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !3).2 ]) [ (!2 = 0) -> z, (!2 = 1) -> f (comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !4).1, (!3 = 1) -> (cC.2 ((x,z)) @ !4).1 ]) (comp ( B (comp ( A) cC.1.1 [ (!3 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !5).1, (!3 = 1)(!4 = 1) -> (cC.2 ((x,z)) @ !5).1, (!4 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !5).1 ])) cB.1.2 [ (!3 = 0) -> cB.1.2 ]) ], (!0 = 1) -> comp ( C x) (x0.2 @ !2) [ (!2 = 0) -> z, (!2 = 1) -> f x (comp ( B x) x0.1 [ (!3 = 1) -> x0.1, (!4 = 0) -> x0.1 ]), (!3 = 1) -> x0.2 @ !2 ], (!2 = 0) -> z, (!2 = 1) -> f x (comp ( B x) (comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 []) [ (!0 = 0) -> comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ !1).1, (!0 = 1) -> (cC.2 ((x,z)) @ !1).1 ])) cB.1.2 [], (!0 = 1) -> comp ( B x) x0.1 [ (!3 = 1)(!4 = 1) -> x0.1 ], (!3 = 0) -> comp ( B (comp ( A) cC.1.1 [ (!0 = 0) -> comp ( A) cC.1.1 [ (!1 = 0) -> (cC.2 ((cB.1.1,f cB.1.1 cB.1.2)) @ (!2 /\ !3)).1, (!1 = 1) -> (cC.2 ((x,z)) @ (!2 /\ !3)).1, (!2 = 0) -> cC.1.1 ], (!0 = 1) -> (cC.2 ((x,x0.2 @ -!1)) @ !2).1, (!1 = 0) -> (cC.2 (((cB.2 ((x,x0.1)) @ !0).1,f (cB.2 ((x,x0.1)) @ !0).1 (cB.2 ((x,x0.1)) @ !0).2)) @ !2).1, (!1 = 1) -> (cC.2 ((x,z)) @ !2).1 ])) (cB.2 ((x,x0.1)) @ !0).2 [] ]) ])) lem1 (B:U) : isContr ((X:U) * equiv X B) = @@ -115,7 +115,7 @@ lem1 (B:U) : isContr ((X:U) * equiv X B) = ,(j=1) -> v.2]) in (center,contr))) -nlem1 (B:U) : isContr ((X:U) * equiv X B) = ((B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))),\(w : Sigma U (\(X : U) -> Sigma (X -> B) (\(f : X -> B) -> (y : B) -> Sigma (Sigma X (\(x : X) -> IdP ( B) y (f x))) (\(x : Sigma X (\(x : X) -> IdP ( B) y (f x))) -> (y0 : Sigma X (\(x0 : X) -> IdP ( B) y (f x0))) -> IdP ( Sigma X (\(x0 : X) -> IdP ( B) y (f x0))) x y0)))) -> (glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],(\(g : glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> unglueElem g [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],\(b : B) -> ((glueElem (comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ !1 ]) [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.1 ], comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!1 /\ !2), (!1 = 0) -> b ]),\(v : Sigma (glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) (\(x : glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> IdP ( B) b (unglueElem x [ (!0 = 0) -> (B,(\(x0 : B) -> x0,\(a : B) -> ((a, a),\(z : Sigma B (\(x0 : B) -> IdP ( B) a x0)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]))) -> (glueElem (comp ( B) b [ (!0 = 0) -> v.2 @ (!1 /\ !2), (!0 = 1) -> ((w.2.2 b).2 v @ !1).2 @ !2, (!1 = 0) -> comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!2 /\ !3), (!2 = 0) -> b ], (!1 = 1) -> v.2 @ !2 ]) [ (!0 = 0) -> v.2 @ !1, (!0 = 1) -> ((w.2.2 b).2 v @ !1).1 ], comp ( B) b [ (!0 = 0) -> v.2 @ (!1 /\ !2 /\ !3), (!0 = 1) -> ((w.2.2 b).2 v @ !1).2 @ (!2 /\ !3), (!1 = 0) -> comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!2 /\ !3 /\ !4), (!2 = 0) -> b, (!3 = 0) -> b ], (!1 = 1) -> v.2 @ (!2 /\ !3), (!2 = 0) -> b ]))))) +-- nlem1 (B:U) : isContr ((X:U) * equiv X B) = ((B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))),\(w : Sigma U (\(X : U) -> Sigma (X -> B) (\(f : X -> B) -> (y : B) -> Sigma (Sigma X (\(x : X) -> IdP ( B) y (f x))) (\(x : Sigma X (\(x : X) -> IdP ( B) y (f x))) -> (y0 : Sigma X (\(x0 : X) -> IdP ( B) y (f x0))) -> IdP ( Sigma X (\(x0 : X) -> IdP ( B) y (f x0))) x y0)))) -> (glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],(\(g : glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> unglueElem g [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ],\(b : B) -> ((glueElem (comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ !1 ]) [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.1 ], comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!1 /\ !2), (!1 = 0) -> b ]),\(v : Sigma (glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) (\(x : glue B [ (!0 = 0) -> (B,(\(x : B) -> x,\(a : B) -> ((a, a),\(z : Sigma B (\(x : B) -> IdP ( B) a x)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]) -> IdP ( B) b (unglueElem x [ (!0 = 0) -> (B,(\(x0 : B) -> x0,\(a : B) -> ((a, a),\(z : Sigma B (\(x0 : B) -> IdP ( B) a x0)) -> (z.2 @ !0, z.2 @ (!0 /\ !1))))), (!0 = 1) -> w ]))) -> (glueElem (comp ( B) b [ (!0 = 0) -> v.2 @ (!1 /\ !2), (!0 = 1) -> ((w.2.2 b).2 v @ !1).2 @ !2, (!1 = 0) -> comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!2 /\ !3), (!2 = 0) -> b ], (!1 = 1) -> v.2 @ !2 ]) [ (!0 = 0) -> v.2 @ !1, (!0 = 1) -> ((w.2.2 b).2 v @ !1).1 ], comp ( B) b [ (!0 = 0) -> v.2 @ (!1 /\ !2 /\ !3), (!0 = 1) -> ((w.2.2 b).2 v @ !1).2 @ (!2 /\ !3), (!1 = 0) -> comp ( B) b [ (!0 = 0) -> b, (!0 = 1) -> (w.2.2 b).1.2 @ (!2 /\ !3 /\ !4), (!2 = 0) -> b, (!3 = 0) -> b ], (!1 = 1) -> v.2 @ (!2 /\ !3), (!2 = 0) -> b ]))))) contrSingl' (A : U) (a b : A) (p : Id A a b) : Id ((x:A) * Id A x b) (b,refl A b) (a,p) = (p @ -i, p @ -i\/j)