From: Rafaël Bocquet Date: Mon, 13 Jun 2016 15:16:35 +0000 (+0200) Subject: wip X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=8ab172f74966ccbe9a18d30fa7dd817a6bee7c51;p=cubicaltt.git wip --- diff --git a/examples/category.ctt b/examples/category.ctt index 971a7cc..dde2aa2 100644 --- a/examples/category.ctt +++ b/examples/category.ctt @@ -3,6 +3,7 @@ import prelude import sigma import equiv import nat +import univalence lemReflComp (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) (compId A a a b (<_> a) p) p = comp ( A) (p @ i /\ j) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> p @ k \/ j ] @@ -12,10 +13,28 @@ lemReflComp' (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) (compId A a b b p comp ( A) (p @ i) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> <_> b ] opaque lemReflComp' +setPi (A : U) (B : A -> U) (h : (x : A) -> set (B x)) + (f0 f1 : (x : A) -> B x) + (p1 p2 : Id ((x : A) -> B x) f0 f1) + : Id (Id ((x : A) -> B x) f0 f1) p1 p2 + = \(x : A) -> (h x (f0 x) (f1 x) ( (p1@i) x) ( (p2@i) x)) @ i @ j +opaque setPi + lemIdPProp (A B : U) (AProp : prop A) (p : Id U A B) : (x : A) -> (y : B) -> IdP p x y = J U A (\(B : U) -> \(p : Id U A B) -> (x : A) -> (y : B) -> IdP p x y) AProp B p opaque lemIdPProp +lemIdPSet (A B : U) (ASet : set A) (p : Id U A B) : (x : A) (y : B) (s t : IdP p x y) -> Id (IdP p x y) s t + = J U A (\(B : U) -> \(p : Id U A B) -> (x : A) (y : B) (s t : IdP p x y) -> Id (IdP p x y) s t) ASet B p +opaque lemIdPSet + +lemIdPSet2 (A B : U) (ASet : set A) (p1 : Id U A B) + : (p2 : Id U A B) -> (p : Id (Id U A B) p1 p2) -> + (x : A) -> (y : B) -> (s : IdP p1 x y) -> (t : IdP p2 x y) -> IdP ( (IdP (p @ i) x y)) s t + = J (Id U A B) p1 (\(p2 : Id U A B) -> \(p : Id (Id U A B) p1 p2) -> (x : A) -> (y : B) -> (s : IdP p1 x y) -> (t : IdP p2 x y) -> IdP ( (IdP (p @ i) x y)) s t) + (lemIdPSet A B ASet p1) +opaque lemIdPSet2 + substIdP (A B : U) (p : Id U A B) (x : A) (y : B) (q : Id B (transport p x) y) : IdP p x y = transport ( IdP p x (q@i)) hole where @@ -42,8 +61,8 @@ categoryData : U = (A : U) * (A -> A -> U) isPrecategory (C : categoryData) : U = let A : U = C.1 hom : A -> A -> U = C.2 - in (homSet : (x y : A) -> set (hom x y)) - * (id : (x : A) -> hom x x) * (c : (x y z : A) -> hom x y -> hom y z -> hom x z) + in (id : (x : A) -> hom x x) * (c : (x y z : A) -> hom x y -> hom y z -> hom x z) + * (homSet : (x y : A) -> set (hom x y)) * (cIdL : (x y : A) -> (f : hom x y) -> Id (hom x y) (c x x y (id x) f) f) * (cIdR : (x y : A) -> (f : hom x y) -> Id (hom x y) (c x y y f (id y)) f) * ( (x y z w : A) -> (f : hom x y) -> (g : hom y z) -> (h : hom z w) -> Id (hom x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h))) @@ -52,9 +71,9 @@ precategory : U = (C : categoryData) * isPrecategory C cA (C : precategory) : U = C.1.1 cH (C : precategory) (a b : cA C) : U = C.1.2 a b -cHSet (C : precategory) (a b : cA C) : set (cH C a b) = C.2.1 a b -cC (C : precategory) (x y z : cA C) (f : cH C x y) (g : cH C y z) : cH C x z = C.2.2.2.1 x y z f g -cId (C : precategory) (x : cA C) : cH C x x = C.2.2.1 x +cHSet (C : precategory) (a b : cA C) : set (cH C a b) = C.2.2.2.1 a b +cC (C : precategory) (x y z : cA C) (f : cH C x y) (g : cH C y z) : cH C x z = C.2.2.1 x y z f g +cId (C : precategory) (x : cA C) : cH C x x = C.2.1 x cIdL (C : precategory) (x y : cA C) (f : cH C x y) : Id (cH C x y) (cC C x x y (cId C x) f) f = C.2.2.2.2.1 x y f cIdR (C : precategory) (x y : cA C) (f : cH C x y) @@ -62,6 +81,115 @@ cIdR (C : precategory) (x y : cA C) (f : cH C x y) cIdC (C : precategory) (x y z w : cA C) (f : cH C x y) (g : cH C y z) (h : cH C z w) : Id (cH C x w) (cC C x z w (cC C x y z f g) h) (cC C x y w f (cC C y z w g h)) = C.2.2.2.2.2.2 x y z w f g h + +catIso3 (A B : precategory) : U = (e1 : Id U (cA A) (cA B)) + * (e2 : IdP ((x y : e1@i)->U) (cH A) (cH B)) + * (_ : IdP ( (x:e1@i)->(e2@i) x x) (cId A) (cId B)) + * (IdP ( (x y z:e1@i)->(e2@i) x y->(e2@i) y z->(e2@i) x z) (cC A) (cC B)) + +-- catIso2 (A B : precategory) : U = (e1 : equiv (cA A) (cA B)) +-- * (e2 : (x y : cA A) -> equiv (cH A x y) (cH B (e1.1 x) (e1.1 y))) +-- * (_ : (x : cA A) -> Id (cH B (e1.1 x) (e1.1 x)) ((e2 x x).1 (cId A x)) (cId B (e1.1 x))) +-- * ((x y z : cA A) -> (f : cH A x y) -> (g : cH A y z) -> +-- Id (cH B (e1.1 x) (e1.1 z)) +-- ((e2 x z).1 (cC A x y z f g)) +-- (cC B (e1.1 x) (e1.1 y) (e1.1 z) ((e2 x y).1 f) ((e2 y z).1 g))) + +catIso30 (A B : precategory) : U = (e1 : Id U (cA A) (cA B)) + * (e2 : Id ((x y : cA A)->U) (cH A) (\(x y:cA A)->cH B (transport e1 x) (transport e1 y))) + * (_ : Id ((x:cA A)->cH A x x) + (cId A) + (\(x : cA A) -> transport ((e2@-j) x x) (cId B (transport e1 x)))) + * (Id ((x y z:cA A)->cH A x y->cH A y z->cH A x z) + (\(x y z:cA A)(f:cH A x y)(g:cH A y z)->cC A x y z f g) + (\(x y z:cA A)(f:cH A x y)(g:cH A y z)-> + transport ((e2@-i) x z) + (cC B (transport e1 x) (transport e1 y) (transport e1 z) + (transport ((e2@i) x y) f) + (transport ((e2@i) y z) g)))) + +catIso31 (A B : precategory) : U = (e1 : Id U (cA A) (cA B)) + * (e2 : Id ((x y : cA A)->U) (cH A) (\(x y:cA A)->cH B (transport e1 x) (transport e1 y))) + * (_ : Id ((x:cA A)->cH A x x) + (cId A) + (\(x : cA A) -> transport ((e2@-j) x x) (cId B (transport e1 x)))) + * (Id ((x y z:cA A)->cH A x y->cH A y z->cH A x z) + (\(x y z:cA A)(f:cH A x y)(g:cH A y z)->cC A x y z f g) + (\(x y z:cA A)(f:cH A x y)(g:cH A y z)-> + transport ((e2@-i) x z) + (cC B (transport e1 x) (transport e1 y) (transport e1 z) + (transport ((e2@i) x y) f) + (transport ((e2@i) y z) g)))) + + +eCatIso3 (A B : precategory) : Id U (catIso3 A B) (catIso30 A B) + = (e1 : Id U (cA A) (cA B)) + * (let e21 : (x y : e1@-i) -> U + = comp (<_> (x y : e1@-i) -> U) + (\(x y : e1@-i) -> cH B (transport (e1@-i\/j) x) (transport (e1@-i\/j) y)) + [(i=1)-><_>\(x y:cA A) -> cH B (transport e1 x) (transport e1 y) + ,(i=0)->\(x y:cA B) -> cH B (transRefl (cA B) x @ j) (transRefl (cA B) y @ j) + ] + f21 : Id ((x y : e1@-i) -> U) + (\(x y : e1@-i) -> cH B (transport (e1@-i\/j) x) (transport (e1@-i\/j) y)) + e21 + = fill (<_> (x y : e1@-i) -> U) + (\(x y : e1@-i) -> cH B (transport (e1@-i\/j) x) (transport (e1@-i\/j) y)) + [(i=1)-><_>\(x y:cA A) -> cH B (transport e1 x) (transport e1 y) + ,(i=0)->\(x y:cA B) -> cH B (transRefl (cA B) x @ j) (transRefl (cA B) y @ j) + ] + in + (e2 : IdP ( (x y : e1@j/\-i) -> U) (cH A) e21) + * (_ : IdP ( (x : e1@j/\-i) -> (e2@j/\-i) x x) + (cId A) + (comp (<_> (x:e1@-i)->(e2@-i) x x) + (\(x : e1@-i) -> transport ((e2@-i\/-j) x x) (transport ((f21@j) x x) (cId B (transport (e1@-i\/j) x)))) + [(i=1)->\(x:cA A) -> transport ((e2@-j) x x) (transRefl ((f21@0) x x) (cId B (transport e1 x)) @ j) + ,(i=0)->\(x:cA B) -> + transRefl ((e2@1) x x) + (compId (cH B x x) + (transport (cH B (transRefl (cA B) x@k) (transRefl (cA B) x@k)) + (cId B (transport (<_> cA B) x))) + (transport (<_>cH B x x) (cId B x)) + (cId B x) + (transport (cH B (transRefl (cA B) x@j\/k) (transRefl (cA B) x@j\/k)) + (cId B (transRefl (cA B) x @ j))) + (transRefl (cH B x x) (cId B x)) + @ j) @ j + ])) + * (IdP ( (x y z : e1@j/\-i) (f : (e2@j/\-i) x y) (g : (e2@j/\-i) y z) -> (e2@j/\-i) x z) + (cC A) + (comp (<_> (x y z : e1@-i) (f : (e2@-i) x y) (g : (e2@-i) y z) -> (e2@-i) x z) + (\(x y z : e1@-i) (f : (e2@-i) x y) (g : (e2@-i) y z) -> + transport ((e2@-i\/-j) x z) (transport ((f21@j) x z) + (cC B (transport (e1@-i\/j) x) (transport (e1@-i\/j) y) (transport (e1@-i\/j) z) + (transport ((f21@-j) x y) (transport ((e2@-i\/j) x y) f)) + (transport ((f21@-j) y z) (transport ((e2@-i\/j) y z) g))))) + [(i=1)->\(x y z : cA A) (f : cH A x y) (g : cH A y z) -> + transport ((e2@-j) x z) (transRefl ((f21@0) x z) + (cC B (transport e1 x) (transport e1 y) (transport e1 z) + (transRefl ((f21@0) x y) (transport ((e2@j) x y) f) @ j) + (transRefl ((f21@0) y z) (transport ((e2@j) y z) g) @ j)) @ j) + ,(i=0)->\(x y z : cA B) (f : cH B x y) (g : cH B y z) -> + transRefl ((e2@1) x z) + (compId (cH B x z) + (transport (cH B (transRefl (cA B) x@k) (transRefl (cA B) z@k)) + (cC B (transport (<_>cA B) x) (transport (<_>cA B) y) (transport (<_>cA B) z) + (transport (cH B (transRefl (cA B) x@-k) (transRefl (cA B) y@-k)) (transport ((e2@1) x y) f)) + (transport (cH B (transRefl (cA B) y@-k) (transRefl (cA B) z@-k)) (transport ((e2@1) y z) g)))) + (transport (<_>cH B x z) + (cC B x y z + (transport (<_>cH B x y) f) + (transport (<_>cH B y z) g))) + (cC B x y z f g) + (transport (cH B (transRefl (cA B) x@j\/k) (transRefl (cA B) z@j\/k)) + (cC B (transRefl (cA B) x@j) (transRefl (cA B) y@j) (transRefl (cA B) z@j) + (transport (cH B (transRefl (cA B) x@j\/-k) (transRefl (cA B) y@j\/-k)) (transRefl ((e2@1) x y) f@j)) + (transport (cH B (transRefl (cA B) y@j\/-k) (transRefl (cA B) z@j\/-k)) (transRefl ((e2@1) y z) g@j)))) + (transRefl (cH B x z) (cC B x y z (transRefl (cH B x y) f @ j) (transRefl (cH B y z) g @ j)) @ j) + @ j) @ j + ]))) + -- iso (C : precategory) (A B : cA C) : U @@ -69,12 +197,511 @@ iso (C : precategory) (A B : cA C) : U * (_ : Id (cH C A A) (cC C A B A f g) (cId C A)) * (Id (cH C B B) (cC C B A B g f) (cId C B)) -isoId (C : precategory) (A : cA C) : iso C A A = (cId C A, cId C A, cIdL C A A (cId C A), cIdL C A A (cId C A)) +isoEq (C : precategory) (A B : cA C) (f g : iso C A B) (p1 : Id (cH C A B) f.1 g.1) (p2 : Id (cH C B A) f.2.1 g.2.1) + : Id (iso C A B) f g + = (p1@i,p2@i + ,lemIdPProp (Id (cH C A A) (cC C A B A (p1@0) (p2@0)) (cId C A)) + (Id (cH C A A) (cC C A B A (p1@1) (p2@1)) (cId C A)) + (cHSet C A A (cC C A B A (p1@0) (p2@0)) (cId C A)) + (Id (cH C A A) (cC C A B A (p1@i) (p2@i)) (cId C A)) + f.2.2.1 g.2.2.1 @ i + ,lemIdPProp (Id (cH C B B) (cC C B A B (p2@0) (p1@0)) (cId C B)) + (Id (cH C B B) (cC C B A B (p2@1) (p1@1)) (cId C B)) + (cHSet C B B (cC C B A B (p2@0) (p1@0)) (cId C B)) + (Id (cH C B B) (cC C B A B (p2@i) (p1@i)) (cId C B)) + f.2.2.2 g.2.2.2 @ i) +opaque isoEq + +invIso (C : precategory) (A B : cA C) (f : iso C A B) : iso C B A = (f.2.1, f.1, f.2.2.2, f.2.2.1) +idIso (C : precategory) (A : cA C) : iso C A A = (cId C A, cId C A, cIdL C A A (cId C A), cIdL C A A (cId C A)) + +invIsoEquiv (C : precategory) (A B : cA C) : isEquiv (iso C A B) (iso C B A) (invIso C A B) + = gradLemma (iso C A B) (iso C B A) (invIso C A B) (invIso C B A) (\(x : iso C B A) -> <_> x) (\(x : iso C A B) -> <_> x) + +invIsoEq (C : precategory) (A B : cA C) : Id U (iso C A B) (iso C B A) + = equivId (iso C A B) (iso C B A) (invIso C A B) (invIsoEquiv C A B) + +compIsoHelper (X : precategory) (A B C : cA X) (f : iso X A B) (g : iso X B C) + : Id (cH X A A) (cC X A C A (cC X A B C f.1 g.1) (cC X C B A g.2.1 f.2.1)) (cId X A) + = compId (cH X A A) + (cC X A C A (cC X A B C f.1 g.1) (cC X C B A g.2.1 f.2.1)) + (cC X A B A f.1 (cC X B C A g.1 (cC X C B A g.2.1 f.2.1))) + (cId X A) + (cIdC X A B C A f.1 g.1 (cC X C B A g.2.1 f.2.1)) + (compId (cH X A A) + (cC X A B A f.1 (cC X B C A g.1 (cC X C B A g.2.1 f.2.1))) + (cC X A B A f.1 (cC X B B A (cC X B C B g.1 g.2.1) f.2.1)) + (cId X A) + (cC X A B A f.1 (cIdC X B C B A g.1 g.2.1 f.2.1 @ -i)) + (compId (cH X A A) + (cC X A B A f.1 (cC X B B A (cC X B C B g.1 g.2.1) f.2.1)) + (cC X A B A f.1 (cC X B B A (cId X B) f.2.1)) + (cId X A) + (cC X A B A f.1 (cC X B B A (g.2.2.1 @ i) f.2.1)) + (compId (cH X A A) + (cC X A B A f.1 (cC X B B A (cId X B) f.2.1)) + (cC X A B A f.1 f.2.1) + (cId X A) + (cC X A B A f.1 (cIdL X B A f.2.1 @ i)) + f.2.2.1))) +opaque compIsoHelper + +compIso (X : precategory) (A B C : cA X) (f : iso X A B) (g : iso X B C) : iso X A C + = (cC X A B C f.1 g.1, cC X C B A g.2.1 f.2.1 + ,compIsoHelper X A B C f g + ,compIsoHelper X C B A (invIso X B C g) (invIso X A B f)) + +IdLIso (C : precategory) (A B : cA C) (f : iso C A B) : Id (iso C A B) (compIso C A A B (idIso C A) f) f + = isoEq C A B (compIso C A A B (idIso C A) f) f (cIdL C A B f.1) (cIdR C B A f.2.1) +opaque IdLIso +IdRIso (C : precategory) (A B : cA C) (f : iso C A B) : Id (iso C A B) (compIso C A B B f (idIso C B)) f + = isoEq C A B (compIso C A B B f (idIso C B)) f (cIdR C A B f.1) (cIdL C B A f.2.1) +opaque IdRIso +IdCIso (X : precategory) (A B C D : cA X) (f : iso X A B) (g : iso X B C) (h : iso X C D) + : Id (iso X A D) (compIso X A C D (compIso X A B C f g) h) (compIso X A B D f (compIso X B C D g h)) + = isoEq X A D (compIso X A C D (compIso X A B C f g) h) (compIso X A B D f (compIso X B C D g h)) + (cIdC X A B C D f.1 g.1 h.1) (cIdC X D C B A h.2.1 g.2.1 f.2.1@-i) +opaque IdCIso +IdInvLIso (X : precategory) (A B : cA X) (f : iso X A B) : Id (iso X B B) (compIso X B A B (invIso X A B f) f) (idIso X B) + = isoEq X B B (compIso X B A B (invIso X A B f) f) (idIso X B) f.2.2.2 f.2.2.2 +opaque IdInvLIso + +opaque compIso + eqToIso (C : precategory) (A B : cA C) (p : Id (cA C) A B) : iso C A B - = J (cA C) A (\(B : cA C) -> \(p : Id (cA C) A B) -> iso C A B) (isoId C A) B p + = J (cA C) A (\(B : cA C) -> \(p : Id (cA C) A B) -> iso C A B) (idIso C A) B p + isCategory (C : precategory) : U = (A : cA C) -> isContr ((B : cA C) * iso C A B) -lemIsCategory (C : precategory) (isC : isCategory C) (A B : cA C) (e : iso C A B) : Id (cA C) A B - = (isContrProp ((B : cA C) * iso C A B) (isC A) (A, isoId C A) (B, e) @ i).1 + +lemIsCategory (C : precategory) (isC : isCategory C) (A B : cA C) (e : iso C A B) : Id ((B : cA C) * iso C A B) (A, idIso C A) (B, e) + = (isContrProp ((B : cA C) * iso C A B) (isC A) (A, idIso C A) (B, e) @ i) + +lemIsCategory2 (C : precategory) (isC : isCategory C) (A B : cA C) : isEquiv (Id (cA C) A B) (iso C A B) (eqToIso C A B) + = equivFunFib (cA C) (Id (cA C) A) (iso C A) (eqToIso C A) (lemSinglContr (cA C) A) (isC A) B + +lemIsCategory3 (C : precategory) (isC : isCategory C) (A B : cA C) : Id U (Id (cA C) A B) (iso C A B) + = equivId (Id (cA C) A B) (iso C A B) (eqToIso C A B) (lemIsCategory2 C isC A B) + +-- + +-- setCat : precategory +-- = ((hSet, \(a b : hSet) -> a.1 -> b.1) +-- ,\(a : hSet) (x : a.1) -> x +-- ,\(a b c : hSet) (f : a.1 -> b.1) (g : b.1 -> c.1) (x : a.1) -> g (f x) +-- ,\(a b : hSet) -> setPi a.1 (\(_ : a.1) -> b.1) (\(_ : a.1) -> b.2) +-- ,\(a b : hSet) (f : a.1 -> b.1) -> <_> \(x : a.1) -> f x +-- ,\(a b : hSet) (f : a.1 -> b.1) -> <_> \(x : a.1) -> f x +-- ,\(a b c d : hSet) (f : a.1 -> b.1) (g : b.1 -> c.1) (h : c.1 -> d.1) -> <_> \(x : a.1) -> h (g (f x))) +-- where hSet : U = Sigma U set + +-- -- setIsCat : isCategory setCat +-- -- = \(A:Sigma U set) -> +-- -- ((A,idIso setCat A), +-- -- \(B:(B1:Sigma U set)*iso setCat A B1)-> +-- -- let p : Id U A.1 B.1.1 = isoId A.1 B.1.1 B.2.1 B.2.2.1 (\(x : B.1.1) -> (B.2.2.2.2@j)x) (\(x:A.1)->(B.2.2.2.1@j)x) @ i +-- -- q : IdP (set(p@i)) A.2 B.1.2 = undefined +-- -- r : Id (iso setCat A A) (transport (iso setCat A (p@-i,q@-i)) B.2) (idIso setCat A) +-- -- = (? +-- -- ,? +-- -- ,? +-- -- ,?) +-- -- in ( ((p@i,q@i) +-- -- ,substIdP (iso setCat A B.1) (iso setCat A A) (iso setCat A (p@-i,q@-i)) +-- -- B.2 (idIso setCat A) r @-i))) + +-- -- sip + +-- structure (X : precategory) : U +-- = (P : cA X -> U) +-- * (H : (x y : cA X) -> (a : P x) -> (b : P y) -> (f : cH X x y) -> U) +-- * (propH : (x y : cA X) -> (a : P x) -> (b : P y) -> (f : cH X x y) -> prop (H x y a b f)) +-- * (Hid : (x : cA X) -> (a : P x) -> H x x a a (cId X x)) +-- * ((x y z : cA X) -> (a : P x) -> (b : P y) -> (c : P z) -> +-- (f : cH X x y) -> (g : cH X y z) -> +-- H x y a b f -> H y z b c g -> H x z a c (cC X x y z f g)) + +-- sP (X : precategory) (S : structure X) : cA X -> U = S.1 +-- sH (X : precategory) (S : structure X) : (x y : cA X) -> (a : sP X S x) -> (b : sP X S y) -> (f : cH X x y) -> U = S.2.1 +-- sHProp (X : precategory) (S : structure X) +-- : (x y : cA X) -> (a : sP X S x) -> (b : sP X S y) -> (f : cH X x y) -> prop (sH X S x y a b f) = S.2.2.1 +-- sHId (X : precategory) (S : structure X) : (x : cA X) -> (a : sP X S x) -> sH X S x x a a (cId X x) = S.2.2.2.1 +-- sHComp (X : precategory) (S : structure X) +-- : (x y z : cA X) -> (a : sP X S x) -> (b : sP X S y) -> (c : sP X S z) -> +-- (f : cH X x y) -> (g : cH X y z) -> +-- sH X S x y a b f -> sH X S y z b c g -> sH X S x z a c (cC X x y z f g) +-- = S.2.2.2.2 + +-- isStandardStructure (X : precategory) (S : structure X) : U +-- = (x : cA X) -> (a b : sP X S x) -> +-- sH X S x x a b (cId X x) -> sH X S x x b a (cId X x) -> +-- Id (sP X S x) a b + +-- sipPrecategory (C : precategory) (S : structure C) : precategory = ((ob, hom), (id, cmp, homSet, idL, idR, idC)) +-- where +-- ob : U = Sigma (cA C) (sP C S) +-- hom (X Y : ob) : U = (f : cH C X.1 Y.1) * sH C S X.1 Y.1 X.2 Y.2 f +-- homSet (X Y : ob) : set (hom X Y) +-- = setSig (cH C X.1 Y.1) (sH C S X.1 Y.1 X.2 Y.2) +-- (cHSet C X.1 Y.1) (\(f : cH C X.1 Y.1) -> propSet (sH C S X.1 Y.1 X.2 Y.2 f) (sHProp C S X.1 Y.1 X.2 Y.2 f)) +-- id (X : ob) : hom X X = (cId C X.1, sHId C S X.1 X.2) +-- cmp (x y z : ob) (f : hom x y) (g : hom y z) : hom x z +-- = (cC C x.1 y.1 z.1 f.1 g.1, sHComp C S x.1 y.1 z.1 x.2 y.2 z.2 f.1 g.1 f.2 g.2) +-- idL (x y : ob) (f : hom x y) : Id (hom x y) (cmp x x y (id x) f) f +-- = (cIdL C x.1 y.1 f.1 @ i +-- ,lemIdPProp (sH C S x.1 y.1 x.2 y.2 (cmp x x y (id x) f).1) +-- (sH C S x.1 y.1 x.2 y.2 f.1) +-- (sHProp C S x.1 y.1 x.2 y.2 (cmp x x y (id x) f).1) +-- (sH C S x.1 y.1 x.2 y.2 (cIdL C x.1 y.1 f.1 @ i)) +-- (cmp x x y (id x) f).2 f.2 @ i) +-- idR (x y : ob) (f : hom x y) : Id (hom x y) (cmp x y y f (id y)) f +-- = (cIdR C x.1 y.1 f.1 @ i +-- ,lemIdPProp (sH C S x.1 y.1 x.2 y.2 (cmp x y y f (id y)).1) +-- (sH C S x.1 y.1 x.2 y.2 f.1) +-- (sHProp C S x.1 y.1 x.2 y.2 (cmp x y y f (id y)).1) +-- (sH C S x.1 y.1 x.2 y.2 (cIdR C x.1 y.1 f.1 @ i)) +-- (cmp x y y f (id y)).2 f.2 @ i) +-- idC (x y z w : ob) (f : hom x y) (g : hom y z) (h : hom z w) : Id (hom x w) (cmp x z w (cmp x y z f g) h) (cmp x y w f (cmp y z w g h)) +-- = (cIdC C x.1 y.1 z.1 w.1 f.1 g.1 h.1 @ i +-- ,lemIdPProp (sH C S x.1 w.1 x.2 w.2 (cmp x z w (cmp x y z f g) h).1) +-- (sH C S x.1 w.1 x.2 w.2 (cmp x y w f (cmp y z w g h)).1) +-- (sHProp C S x.1 w.1 x.2 w.2 (cmp x z w (cmp x y z f g) h).1) +-- (sH C S x.1 w.1 x.2 w.2 (cIdC C x.1y.1 z.1 w.1 f.1 g.1 h.1 @ i)) +-- (cmp x z w (cmp x y z f g) h).2 (cmp x y w f (cmp y z w g h)).2 @ i) + +-- isContrProp (A : U) (p : isContr A) (x y : A) : Id A x y = compId A x p.1 y ( p.2 x @ -i) (p.2 y) +-- isContrSig (A:U) (B:A-> U) (cA:isContr A) (cB : (x:A) -> isContr (B x)) : isContr (Sigma A B) +-- = ((cA.1, (cB cA.1).1), \(x:Sigma A B) -> propSig A B (isContrProp A cA) (\(x:A)->isContrProp (B x) (cB x)) (cA.1, (cB cA.1).1) x) + +-- sip (X : precategory) (isC : isCategory X) (S : structure X) (isS : isStandardStructure X S) : isCategory (sipPrecategory X S) +-- = undefined +-- -- = hole +-- -- where +-- -- D : precategory = sipPrecategory X S +-- -- eq1 (A : cA D) +-- -- : Id U ((B : cA D) * iso D A B) +-- -- ((C : (B1 : cA X) * ( iso X A.1 B1)) +-- -- * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1) +-- -- = isoId +-- -- ((B : cA D) * iso D A B) +-- -- ((C : (B1 : cA X) * ( iso X A.1 B1)) +-- -- * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1) +-- -- F G FG GF +-- -- where +-- -- F (C : (B : cA D) * iso D A B) +-- -- : ((C : (B1 : cA X) * ( iso X A.1 B1)) +-- -- * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1) +-- -- = ((C.1.1, C.2.1.1, C.2.2.1.1, (C.2.2.2.1@i).1, (C.2.2.2.2@i).1), +-- -- C.1.2, C.2.1.2, C.2.2.1.2) +-- -- G (C : ((C : (B1 : cA X) * ( iso X A.1 B1)) +-- -- * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1)) +-- -- : (B : cA D) * iso D A B +-- -- = ((C.1.1, C.2.1), (C.1.2.1, C.2.2.1), (C.1.2.2.1, C.2.2.2) +-- -- , (C.1.2.2.2.1 @ i +-- -- ,lemIdPProp (sH X S A.1 A.1 A.2 A.2 (cC X A.1 C.1.1 A.1 C.1.2.1 C.1.2.2.1)) +-- -- (sH X S A.1 A.1 A.2 A.2 (cId X A.1)) +-- -- (sHProp X S A.1 A.1 A.2 A.2 (cC X A.1 C.1.1 A.1 C.1.2.1 C.1.2.2.1)) +-- -- (sH X S A.1 A.1 A.2 A.2 (C.1.2.2.2.1 @ i)) +-- -- (sHComp X S A.1 C.1.1 A.1 A.2 C.2.1 A.2 C.1.2.1 C.1.2.2.1 C.2.2.1 C.2.2.2) +-- -- (sHId X S A.1 A.2) @ i) +-- -- , (C.1.2.2.2.2 @ i +-- -- ,lemIdPProp (sH X S C.1.1 C.1.1 C.2.1 C.2.1 (cC X C.1.1 A.1 C.1.1 C.1.2.2.1 C.1.2.1)) +-- -- (sH X S C.1.1 C.1.1 C.2.1 C.2.1 (cId X C.1.1)) +-- -- (sHProp X S C.1.1 C.1.1 C.2.1 C.2.1 (cC X C.1.1 A.1 C.1.1 C.1.2.2.1 C.1.2.1)) +-- -- (sH X S C.1.1 C.1.1 C.2.1 C.2.1 (C.1.2.2.2.2 @ i)) +-- -- (sHComp X S C.1.1 A.1 C.1.1 C.2.1 A.2 C.2.1 C.1.2.2.1 C.1.2.1 C.2.2.2 C.2.2.1) +-- -- (sHId X S C.1.1 C.2.1) @ i)) +-- -- FG (C : ((C : (B1 : cA X) * ( iso X A.1 B1)) +-- -- * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1)) +-- -- : Id ((C : (B1 : cA X) * ( iso X A.1 B1)) +-- -- * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1) +-- -- (F (G C)) C +-- -- = <_> C +-- -- GF (C : (B : cA D) * iso D A B) : Id ((B : cA D) * iso D A B) (G (F C)) C +-- -- = (C.1, C.2.1, C.2.2.1 +-- -- , ((C.2.2.2.1 @ j).1 +-- -- ,lemIdPSet (sH X S A.1 A.1 A.2 A.2 (cC X A.1 C.1.1 A.1 C.2.1.1 C.2.2.1.1)) +-- -- (sH X S A.1 A.1 A.2 A.2 (cId X A.1)) +-- -- (propSet (sH X S A.1 A.1 A.2 A.2 (cC X A.1 C.1.1 A.1 C.2.1.1 C.2.2.1.1)) +-- -- (sHProp X S A.1 A.1 A.2 A.2 (cC X A.1 C.1.1 A.1 C.2.1.1 C.2.2.1.1))) +-- -- (sH X S A.1 A.1 A.2 A.2 (C.2.2.2.1 @ j).1) +-- -- (sHComp X S A.1 C.1.1 A.1 A.2 C.1.2 A.2 C.2.1.1 C.2.2.1.1 C.2.1.2 C.2.2.1.2) +-- -- (sHId X S A.1 A.2) +-- -- (((G (F C)).2.2.2.1 @ j).2) +-- -- ((C.2.2.2.1 @ j).2) @i@j) +-- -- , ((C.2.2.2.2 @ j).1 +-- -- ,lemIdPSet (sH X S C.1.1 C.1.1 C.1.2 C.1.2 (cC X C.1.1 A.1 C.1.1 C.2.2.1.1 C.2.1.1)) +-- -- (sH X S C.1.1 C.1.1 C.1.2 C.1.2 (cId X C.1.1)) +-- -- (propSet (sH X S C.1.1 C.1.1 C.1.2 C.1.2 (cC X C.1.1 A.1 C.1.1 C.2.2.1.1 C.2.1.1)) +-- -- (sHProp X S C.1.1 C.1.1 C.1.2 C.1.2 (cC X C.1.1 A.1 C.1.1 C.2.2.1.1 C.2.1.1))) +-- -- (sH X S C.1.1 C.1.1 C.1.2 C.1.2 (C.2.2.2.2 @ j).1) +-- -- (sHComp X S C.1.1 A.1 C.1.1 C.1.2 A.2 C.1.2 C.2.2.1.1 C.2.1.1 C.2.2.1.2 C.2.1.2) +-- -- (sHId X S C.1.1 C.1.2) +-- -- (((G (F C)).2.2.2.2 @ j).2) +-- -- ((C.2.2.2.2 @ j).2) @i@j)) +-- -- hole0 (A : cA D) +-- -- : isContr ((C : (B1 : cA X) * ( iso X A.1 B1)) +-- -- * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1) +-- -- = isContrSig ((B1 : cA X) * ( iso X A.1 B1)) +-- -- (\(C : (B1 : cA X) * ( iso X A.1 B1)) -> +-- -- (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1) +-- -- (isC A.1) +-- -- (\(C : (B1 : cA X) * ( iso X A.1 B1)) -> +-- -- let p : Id ((B1 : cA X) * ( iso X A.1 B1)) (A.1, idIso X A.1) C +-- -- = lemIsCategory X isC A.1 C.1 C.2 +-- -- in transport +-- -- ( isContr ((B2 : sP X S (p@i).1) * (_ : sH X S A.1 (p@i).1 A.2 B2 (p@i).2.1) * sH X S (p@i).1 A.1 B2 A.2 (p@i).2.2.1)) +-- -- ((A.2,sHId X S A.1 A.2,sHId X S A.1 A.2) +-- -- ,\(Y : (B2 : sP X S A.1) * (_ : sH X S A.1 A.1 A.2 B2 (cId X A.1)) * sH X S A.1 A.1 B2 A.2 (cId X A.1)) -> +-- -- (isS A.1 A.2 Y.1 Y.2.1 Y.2.2 @ i +-- -- ,lemIdPProp (sH X S A.1 A.1 A.2 A.2 (cId X A.1)) +-- -- (sH X S A.1 A.1 A.2 Y.1 (cId X A.1)) +-- -- (sHProp X S A.1 A.1 A.2 A.2 (cId X A.1)) +-- -- (sH X S A.1 A.1 A.2 (isS A.1 A.2 Y.1 Y.2.1 Y.2.2 @ i) (cId X A.1)) +-- -- (sHId X S A.1 A.2) Y.2.1 @ i +-- -- ,lemIdPProp (sH X S A.1 A.1 A.2 A.2 (cId X A.1)) +-- -- (sH X S A.1 A.1 Y.1 A.2 (cId X A.1)) +-- -- (sHProp X S A.1 A.1 A.2 A.2 (cId X A.1)) +-- -- (sH X S A.1 A.1 (isS A.1 A.2 Y.1 Y.2.1 Y.2.2 @ i) A.2 (cId X A.1)) +-- -- (sHId X S A.1 A.2) Y.2.2 @ i))) +-- -- hole (A : cA D) : isContr ((B : cA D) * iso D A B) = transport (isContr(eq1 A@-i)) (hole0 A) + +-- + +functor (A B : precategory) : U + = (Fob : cA A -> cA B) + * (Fmor : (x y : cA A) -> cH A x y -> cH B (Fob x) (Fob y)) + * (Fid : (x : cA A) -> Id (cH B (Fob x) (Fob x)) (Fmor x x (cId A x)) (cId B (Fob x))) + * ((x y z : cA A) -> (f : cH A x y) -> (g : cH A y z) -> Id (cH B (Fob x) (Fob z)) (Fmor x z (cC A x y z f g)) (cC B (Fob x) (Fob y) (Fob z) (Fmor x y f) (Fmor y z g))) + +idFunctor (A : precategory) : functor A A + = (\(x : cA A) -> x + ,\(x y : cA A) (h : cH A x y) -> h + ,\(x : cA A) -> <_> cId A x + ,\(x y z : cA A) (f : cH A x y) (g : cH A y z) -> <_> cC A x y z f g) + +compFunctor (A B C : precategory) (F : functor A B) (G : functor B C) : functor A C + = (\(x : cA A) -> G.1 (F.1 x) + ,\(x y : cA A) (h : cH A x y) -> G.2.1 (F.1 x) (F.1 y) (F.2.1 x y h) + ,\(x : cA A) -> compId (cH C (G.1 (F.1 x)) (G.1 (F.1 x))) + (G.2.1 (F.1 x) (F.1 x) (F.2.1 x x (cId A x))) + (G.2.1 (F.1 x) (F.1 x) (cId B (F.1 x))) + (cId C (G.1 (F.1 x))) + (G.2.1 (F.1 x) (F.1 x) (F.2.2.1 x @ i)) + (G.2.2.1 (F.1 x)) + ,\(x y z : cA A) (f : cH A x y) (g : cH A y z) -> + compId (cH C (G.1 (F.1 x)) (G.1 (F.1 z))) + (G.2.1 (F.1 x) (F.1 z) (F.2.1 x z (cC A x y z f g))) + (G.2.1 (F.1 x) (F.1 z) (cC B (F.1 x) (F.1 y) (F.1 z) (F.2.1 x y f) (F.2.1 y z g))) + (cC C (G.1 (F.1 x)) (G.1 (F.1 y)) (G.1 (F.1 z)) (G.2.1 (F.1 x) (F.1 y) (F.2.1 x y f)) (G.2.1 (F.1 y) (F.1 z) (F.2.1 y z g))) + ( G.2.1 (F.1 x) (F.1 z) (F.2.2.2 x y z f g @ i)) + (G.2.2.2 (F.1 x) (F.1 y) (F.1 z) (F.2.1 x y f) (F.2.1 y z g)) + ) + +ffFunctor (A B : precategory) (F : functor A B) : U + = (a b : cA A) -> isEquiv (cH A a b) (cH B (F.1 a) (F.1 b)) (F.2.1 a b) +ffEq (A B : precategory) (F : functor A B) (ff : ffFunctor A B F) (a b : cA A) + : Id U (cH A a b) (cH B (F.1 a) (F.1 b)) + = equivId (cH A a b) (cH B (F.1 a) (F.1 b)) (F.2.1 a b) (ff a b) +propFFFunctor (A B : precategory) (F : functor A B) : prop (ffFunctor A B F) + = propPi (cA A) (\(a : cA A) -> (b : cA A) -> isEquiv (cH A a b) (cH B (F.1 a) (F.1 b)) (F.2.1 a b)) + (\(a : cA A) -> propPi (cA A) (\(b : cA A) -> isEquiv (cH A a b) (cH B (F.1 a) (F.1 b)) (F.2.1 a b)) + (\(b : cA A) -> propIsEquiv (cH A a b) (cH B (F.1 a) (F.1 b)) (F.2.1 a b))) + +lem10 (A B : U) (e : equiv A B) (x y : B) (p : Id A (e.2 x).1.1 (e.2 y).1.1) : Id B x y + = transport + (compId U (Id B (e.1 (e.2 x).1.1) (e.1 (e.2 y).1.1)) (Id B x (e.1 (e.2 y).1.1)) (Id B x y) + ( Id B (retEq A B e x @ i) (e.1 (e.2 y).1.1)) ( Id B x (retEq A B e y @ i))) + (mapOnPath A B e.1 (e.2 x).1.1 (e.2 y).1.1 p) +opaque lem10 + +lem10' (A B : U) (e : equiv A B) (x y : A) (p : Id B (e.1 x) (e.1 y)) : Id A x y + = transport + (compId U (Id A (e.2 (e.1 x)).1.1 (e.2 (e.1 y)).1.1) (Id A x (e.2 (e.1 y)).1.1) (Id A x y) + ( Id A (secEq A B e x @ i) (e.2 (e.1 y)).1.1) ( Id A x (secEq A B e y @ i)) + ) + (mapOnPath B A (invEq A B e) (e.1 x) (e.1 y) p) +opaque lem10' + +lemFF (A B : precategory) (F : functor A B) (ff : ffFunctor A B F) (x y : cA A) + : Id U (iso A x y) (iso B (F.1 x) (F.1 y)) + = hole + where + F0 (f : iso A x y) : iso B (F.1 x) (F.1 y) + = (F.2.1 x y f.1, F.2.1 y x f.2.1 + ,compId (cH B (F.1 x) (F.1 x)) + (cC B (F.1 x) (F.1 y) (F.1 x) (F.2.1 x y f.1) (F.2.1 y x f.2.1)) + (F.2.1 x x (cC A x y x f.1 f.2.1)) + (cId B (F.1 x)) + (F.2.2.2 x y x f.1 f.2.1 @-i) + (compId (cH B (F.1 x) (F.1 x)) + (F.2.1 x x (cC A x y x f.1 f.2.1)) + (F.2.1 x x (cId A x)) + (cId B (F.1 x)) + (F.2.1 x x (f.2.2.1@i)) + (F.2.2.1 x)) + ,compId (cH B (F.1 y) (F.1 y)) + (cC B (F.1 y) (F.1 x) (F.1 y) (F.2.1 y x f.2.1) (F.2.1 x y f.1)) + (F.2.1 y y (cC A y x y f.2.1 f.1)) + (cId B (F.1 y)) + (F.2.2.2 y x y f.2.1 f.1 @-i) + (compId (cH B (F.1 y) (F.1 y)) + (F.2.1 y y (cC A y x y f.2.1 f.1)) + (F.2.1 y y (cId A y)) + (cId B (F.1 y)) + (F.2.1 y y (f.2.2.2@i)) + (F.2.2.1 y))) + G0 (g : iso B (F.1 x) (F.1 y)) : iso A x y + = ((ff x y g.1).1.1 + ,(ff y x g.2.1).1.1 + ,lem10' (cH A x x) (cH B (F.1 x) (F.1 x)) (F.2.1 x x, ff x x) (cC A x y x (ff x y g.1).1.1 (ff y x g.2.1).1.1) (cId A x) + (compId (cH B (F.1 x) (F.1 x)) + (F.2.1 x x (cC A x y x (ff x y g.1).1.1 (ff y x g.2.1).1.1)) + (cC B (F.1 x) (F.1 y) (F.1 x) (F.2.1 x y (ff x y g.1).1.1) (F.2.1 y x (ff y x g.2.1).1.1)) + (F.2.1 x x (cId A x)) + (F.2.2.2 x y x (ff x y g.1).1.1 (ff y x g.2.1).1.1) + (compId (cH B (F.1 x) (F.1 x)) + (cC B (F.1 x) (F.1 y) (F.1 x) (F.2.1 x y (ff x y g.1).1.1) (F.2.1 y x (ff y x g.2.1).1.1)) + (cC B (F.1 x) (F.1 y) (F.1 x) g.1 g.2.1) + (F.2.1 x x (cId A x)) + (cC B (F.1 x) (F.1 y) (F.1 x) ((ff x y g.1).1.2@-i) ((ff y x g.2.1).1.2@-i)) + (compId (cH B (F.1 x) (F.1 x)) + (cC B (F.1 x) (F.1 y) (F.1 x) g.1 g.2.1) + (cId B (F.1 x)) + (F.2.1 x x (cId A x)) + g.2.2.1 + (F.2.2.1 x @ -i)))) + ,lem10' (cH A y y) (cH B (F.1 y) (F.1 y)) (F.2.1 y y, ff y y) (cC A y x y (ff y x g.2.1).1.1 (ff x y g.1).1.1) (cId A y) + (compId (cH B (F.1 y) (F.1 y)) + (F.2.1 y y (cC A y x y (ff y x g.2.1).1.1 (ff x y g.1).1.1)) + (cC B (F.1 y) (F.1 x) (F.1 y) (F.2.1 y x (ff y x g.2.1).1.1) (F.2.1 x y (ff x y g.1).1.1)) + (F.2.1 y y (cId A y)) + (F.2.2.2 y x y (ff y x g.2.1).1.1 (ff x y g.1).1.1) + (compId (cH B (F.1 y) (F.1 y)) + (cC B (F.1 y) (F.1 x) (F.1 y) (F.2.1 y x (ff y x g.2.1).1.1) (F.2.1 x y (ff x y g.1).1.1)) + (cC B (F.1 y) (F.1 x) (F.1 y) g.2.1 g.1) + (F.2.1 y y (cId A y)) + (cC B (F.1 y) (F.1 x) (F.1 y) ((ff y x g.2.1).1.2@-i) ((ff x y g.1).1.2@-i)) + (compId (cH B (F.1 y) (F.1 y)) + (cC B (F.1 y) (F.1 x) (F.1 y) g.2.1 g.1) + (cId B (F.1 y)) + (F.2.1 y y (cId A y)) + g.2.2.2 + (F.2.2.1 y @ -i)))) + ) + FG (g : iso B (F.1 x) (F.1 y)) : Id (iso B (F.1 x) (F.1 y)) (F0 (G0 g)) g + = isoEq B (F.1 x) (F.1 y) (F0 (G0 g)) g + ((ff x y g.1).1.2@-i) ((ff y x g.2.1).1.2@-i) + GF (f : iso A x y) : Id (iso A x y) (G0 (F0 f)) f + = isoEq A x y (G0 (F0 f)) f + ( ((ff x y (F.2.1 x y f.1)).2 (f.1,F.2.1 x y f.1)@i).1) + ( ((ff y x (F.2.1 y x f.2.1)).2 (f.2.1,F.2.1 y x f.2.1)@i).1) + hole : Id U (iso A x y) (iso B (F.1 x) (F.1 y)) = isoId (iso A x y) (iso B (F.1 x) (F.1 y)) F0 G0 FG GF +opaque lemFF + +F12 (A B : precategory) (isC : isCategory A) (F : functor A B) + (p1 : ffFunctor A B F) (x : cA A) : isContr ((y : cA A) * iso B (F.1 y) (F.1 x)) + = transport (isContr ((y : cA A) * (invIsoEq B (F.1 x) (F.1 y)@i))) hole + where + hole2 (y : cA A) : Id U (iso A x y) (iso B (F.1 x) (F.1 y)) + = lemFF A B F p1 x y + hole : isContr ((y : cA A) * iso B (F.1 x) (F.1 y)) + = transport ( isContr ((y : cA A) * (hole2 y @ i))) (isC x) +opaque F12 + +F23 (A B : precategory) (F : functor A B) (p2 : (x : cA A) -> isContr ((y : cA A) * iso B (F.1 y) (F.1 x))) + (x : cA B) + (a b : (y : cA A) * iso B (F.1 y) x) : Id ((y : cA A) * iso B (F.1 y) x) a b + = undefined +-- = transport p hole3 +-- where +-- hole2 : Id ((y : cA A) * iso B (F.1 y) (F.1 a.1)) +-- (a.1, idIso B (F.1 a.1)) (b.1, compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2)) +-- = isContrProp ((y : cA A) * iso B (F.1 y) (F.1 a.1)) (p2 a.1) +-- (a.1, idIso B (F.1 a.1)) (b.1, compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2)) +-- opaque hole2 +-- hole3 : Id ((y : cA A) * iso B (F.1 y) x) +-- (a.1, compIso B (F.1 a.1) (F.1 a.1) x (idIso B (F.1 a.1)) a.2) +-- (b.1, compIso B (F.1 b.1) (F.1 a.1) x (compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2)) a.2) +-- = ((hole2@i).1, compIso B (F.1 (hole2@i).1) (F.1 a.1) x (hole2@i).2 a.2) +-- opaque hole3 +-- p : Id U (Id ((y : cA A) * iso B (F.1 y) x) +-- (a.1, compIso B (F.1 a.1) (F.1 a.1) x (idIso B (F.1 a.1)) a.2) +-- (b.1, compIso B (F.1 b.1) (F.1 a.1) x (compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2)) a.2)) +-- (Id ((y : cA A) * iso B (F.1 y) x) a b) +-- = (Id ((y : cA A) * iso B (F.1 y) x) +-- (a.1, IdLIso B (F.1 a.1) x a.2 @ i) +-- (b.1, compId (iso B (F.1 b.1) x) +-- (compIso B (F.1 b.1) (F.1 a.1) x (compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2)) a.2) +-- (compIso B (F.1 b.1) x x b.2 (compIso B x (F.1 a.1) x (invIso B (F.1 a.1) x a.2) a.2)) +-- b.2 +-- (IdCIso B (F.1 b.1) x (F.1 a.1) x b.2 (invIso B (F.1 a.1) x a.2) a.2) +-- (compId (iso B (F.1 b.1) x) +-- (compIso B (F.1 b.1) x x b.2 (compIso B x (F.1 a.1) x (invIso B (F.1 a.1) x a.2) a.2)) +-- (compIso B (F.1 b.1) x x b.2 (idIso B x)) +-- b.2 +-- (compIso B (F.1 b.1) x x b.2 (IdInvLIso B (F.1 a.1) x a.2 @ i)) +-- (IdRIso B (F.1 b.1) x b.2)) +-- @ i)) +opaque F23 + +catIsEquiv (A B : precategory) (F : functor A B) : U + = (_ : ffFunctor A B F) + * ((b : cA B) -> (a : cA A) * iso B (F.1 a) b) +catEquiv (A B : precategory) : U = (F : functor A B) * catIsEquiv A B F +catPropIsEquiv (A B : precategory) (isC : isCategory A) (F : functor A B) : prop (catIsEquiv A B F) + = propSig (ffFunctor A B F) (\(_ : ffFunctor A B F) -> (b : cA B) -> (a : cA A) * iso B (F.1 a) b) + (propFFFunctor A B F) + (\(ff : ffFunctor A B F) -> propPi (cA B) (\(b : cA B) -> (a : cA A) * iso B (F.1 a) b) + (\(b : cA B) -> F23 A B F (F12 A B isC F ff) b)) + +catIsIso (A B : precategory) (F : functor A B) : U + = (_ : ffFunctor A B F) * isEquiv (cA A) (cA B) F.1 +catPropIsIso (A B : precategory) (F : functor A B) : prop (catIsIso A B F) + = propSig (ffFunctor A B F) (\(_ : ffFunctor A B F) -> isEquiv (cA A) (cA B) F.1) + (propFFFunctor A B F) + (\(_ : ffFunctor A B F) -> propIsEquiv (cA A) (cA B) F.1) +catIso (A B : precategory) : U = (F : functor A B) * catIsIso A B F + +catIso2 (A B : precategory) : U = (e1 : equiv (cA A) (cA B)) + * (e2 : (x y : cA A) -> equiv (cH A x y) (cH B (e1.1 x) (e1.1 y))) + * (_ : (x : cA A) -> Id (cH B (e1.1 x) (e1.1 x)) ((e2 x x).1 (cId A x)) (cId B (e1.1 x))) + * ((x y z : cA A) -> (f : cH A x y) -> (g : cH A y z) -> + Id (cH B (e1.1 x) (e1.1 z)) + ((e2 x z).1 (cC A x y z f g)) + (cC B (e1.1 x) (e1.1 y) (e1.1 z) ((e2 x y).1 f) ((e2 y z).1 g))) + +catIsoIsEquiv (A B : precategory) (F : functor A B) (e : catIsIso A B F) : catIsEquiv A B F + = (e.1,\(b:cA B)->((e.2 b).1.1, eqToIso B (F.1 (e.2 b).1.1) b ((e.2 b).1.2@-i))) + +invEquiv (A:U) (a b:A) : Id U (Id A a b) (Id A b a) + = equivId (Id A a b) (Id A b a) (inv A a b) (gradLemma (Id A a b) (Id A b a) (inv A a b) (inv A b a) (\(x:Id A b a) -> <_> x) (\(x:Id A a b) -> <_> x)) + +catEquivIsIso (A B : precategory) (isCA : isCategory A) (isCB : isCategory B) (F : functor A B) (e : catIsEquiv A B F) + : catIsIso A B F + = (e.1, \(b:cA B)-> + let p : isContr ((a:cA A)*iso B (F.1 a) b) + = (e.2 b, F23 A B F (F12 A B isCA F e.1) b (e.2 b)) + in transport (isContr ((a:cA A)*invEquiv (cA B) (F.1 a) b @ i)) + (transport ( isContr ((a:cA A)*lemIsCategory3 B isCB (F.1 a) b@-i)) p)) + +equivProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A) : equiv A B = + (F, gradLemma A B F G (\(y : B) -> BProp (F (G y)) y) (\(x : A) -> AProp (G (F x)) x)) + +catIsEquivEqIso (A B : precategory) (isCA : isCategory A) (isCB : isCategory B) (F : functor A B) + : equiv (catIsEquiv A B F) (catIsIso A B F) + = equivProp (catIsEquiv A B F) (catIsIso A B F) (catPropIsEquiv A B isCA F) (catPropIsIso A B F) + (catEquivIsIso A B isCA isCB F) (catIsoIsEquiv A B F) + +catEquivEqIso (A B : precategory) (isCA : isCategory A) (isCB : isCategory B) : Id U (catEquiv A B) (catIso A B) + = (F : functor A B) * (transEquivToId (catIsEquiv A B F) (catIsIso A B F) (catIsEquivEqIso A B isCA isCB F) @ i) + +catIsoEqId (A B : precategory) : Id U (catIso A B) (Id precategory A B) + = ? + +-- 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) = + +stop : Unit = U -- f' -- W -----> Z @@ -85,249 +712,222 @@ lemIsCategory (C : precategory) (isC : isCategory C) (A B : cA C) (e : iso C A B -- Y -----> X -- f -homTo (C : precategory) (X : cA C) : U = (Y : cA C) * cH C Y X -cospan (C : precategory) : U - = (X : cA C) * (_ : homTo C X) * homTo C X -cospanCone (C : precategory) (D : cospan C) : U - = (W : cA C) * (f : cH C W D.2.1.1) * (g : cH C W D.2.2.1) - * Id (cH C W D.1) - (cC C W D.2.1.1 D.1 f D.2.1.2) - (cC C W D.2.2.1 D.1 g D.2.2.2) -cospanConeHom (C : precategory) (D : cospan C) (E1 E2 : cospanCone C D) : U - = (h : cH C E1.1 E2.1) - * (_ : Id (cH C E1.1 D.2.1.1) (cC C E1.1 E2.1 D.2.1.1 h E2.2.1) E1.2.1) - * (Id (cH C E1.1 D.2.2.1) (cC C E1.1 E2.1 D.2.2.1 h E2.2.2.1) E1.2.2.1) -cospanConeId (C : precategory) (D : cospan C) (E : cospanCone C D) : cospanConeHom C D E E - = (cId C E.1, cIdL C E.1 D.2.1.1 E.2.1, cIdL C E.1 D.2.2.1 E.2.2.1) -cospanConeComp (C : precategory) (D : cospan C) (X Y Z : cospanCone C D) - (F : cospanConeHom C D X Y) (G : cospanConeHom C D Y Z) : cospanConeHom C D X Z - = (cC C X.1 Y.1 Z.1 F.1 G.1 - ,compId (cH C X.1 D.2.1.1) - (cC C X.1 Z.1 D.2.1.1 (cC C X.1 Y.1 Z.1 F.1 G.1) Z.2.1) - (cC C X.1 Y.1 D.2.1.1 F.1 (cC C Y.1 Z.1 D.2.1.1 G.1 Z.2.1)) - X.2.1 - (cIdC C X.1 Y.1 Z.1 D.2.1.1 F.1 G.1 Z.2.1) - (compId (cH C X.1 D.2.1.1) - (cC C X.1 Y.1 D.2.1.1 F.1 (cC C Y.1 Z.1 D.2.1.1 G.1 Z.2.1)) - (cC C X.1 Y.1 D.2.1.1 F.1 Y.2.1) - X.2.1 - ( cC C X.1 Y.1 D.2.1.1 F.1 (G.2.1 @ i)) - F.2.1) - ,compId (cH C X.1 D.2.2.1) - (cC C X.1 Z.1 D.2.2.1 (cC C X.1 Y.1 Z.1 F.1 G.1) Z.2.2.1) - (cC C X.1 Y.1 D.2.2.1 F.1 (cC C Y.1 Z.1 D.2.2.1 G.1 Z.2.2.1)) - X.2.2.1 - (cIdC C X.1 Y.1 Z.1 D.2.2.1 F.1 G.1 Z.2.2.1) - (compId (cH C X.1 D.2.2.1) - (cC C X.1 Y.1 D.2.2.1 F.1 (cC C Y.1 Z.1 D.2.2.1 G.1 Z.2.2.1)) - (cC C X.1 Y.1 D.2.2.1 F.1 Y.2.2.1) - X.2.2.1 - ( cC C X.1 Y.1 D.2.2.1 F.1 (G.2.2 @ i)) - F.2.2)) - -isPullback (C : precategory) (D : cospan C) (E : cospanCone C D) : U - = (h : cospanCone C D) -> isContr (cospanConeHom C D h E) -isPullbackProp (C : precategory) (D : cospan C) (E : cospanCone C D) : prop (isPullback C D E) - = propPi (cospanCone C D) (\(h : cospanCone C D) -> isContr (cospanConeHom C D h E)) - (\(h : cospanCone C D) -> propIsContr (cospanConeHom C D h E)) -hasPullback (C : precategory) (D : cospan C) : U = (E : cospanCone C D) * isPullback C D E - -cospanConePrecategory (C : precategory) (D : cospan C) : precategory - = ((cospanCone C D, cospanConeHom C D) - ,(\(X Y : cospanCone C D) -> setSig (cH C X.1 Y.1) - (\(h : cH C X.1 Y.1) -> - (_ : Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1) - * (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 h Y.2.2.1) X.2.2.1)) - (cHSet C X.1 Y.1) - (\(h : cH C X.1 Y.1) -> setSig (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1) - (\(_ : Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1) -> - (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 h Y.2.2.1) X.2.2.1)) - (propSet (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1) - (cHSet C X.1 D.2.1.1 (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1)) - (\(_ : Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1) -> - (propSet (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 h Y.2.2.1) X.2.2.1) - (cHSet C X.1 D.2.2.1 (cC C X.1 Y.1 D.2.2.1 h Y.2.2.1) X.2.2.1))))) - ,cospanConeId C D - ,cospanConeComp C D - ,\(X Y : cospanCone C D) (F : cospanConeHom C D X Y) -> - (cIdL C X.1 Y.1 F.1 @ i - ,lemIdPProp (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdL C X.1 Y.1 F.1 @ 0) Y.2.1) X.2.1) - (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdL C X.1 Y.1 F.1 @ 1) Y.2.1) X.2.1) - (cHSet C X.1 D.2.1.1 (cC C X.1 Y.1 D.2.1.1 (cIdL C X.1 Y.1 F.1 @ 0) Y.2.1) X.2.1) - (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdL C X.1 Y.1 F.1 @ i) Y.2.1) X.2.1) - (cospanConeComp C D X X Y (cospanConeId C D X) F).2.1 - F.2.1 @ i - ,lemIdPProp (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdL C X.1 Y.1 F.1 @ 0) Y.2.2.1) X.2.2.1) - (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdL C X.1 Y.1 F.1 @ 1) Y.2.2.1) X.2.2.1) - (cHSet C X.1 D.2.2.1 (cC C X.1 Y.1 D.2.2.1 (cIdL C X.1 Y.1 F.1 @ 0) Y.2.2.1) X.2.2.1) - (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdL C X.1 Y.1 F.1 @ i) Y.2.2.1) X.2.2.1) - (cospanConeComp C D X X Y (cospanConeId C D X) F).2.2 - F.2.2 @ i) - ,\(X Y : cospanCone C D) (F : cospanConeHom C D X Y) -> - (cIdR C X.1 Y.1 F.1 @ i - ,lemIdPProp (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdR C X.1 Y.1 F.1 @ 0) Y.2.1) X.2.1) - (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdR C X.1 Y.1 F.1 @ 1) Y.2.1) X.2.1) - (cHSet C X.1 D.2.1.1 (cC C X.1 Y.1 D.2.1.1 (cIdR C X.1 Y.1 F.1 @ 0) Y.2.1) X.2.1) - (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdR C X.1 Y.1 F.1 @ i) Y.2.1) X.2.1) - (cospanConeComp C D X Y Y F (cospanConeId C D Y)).2.1 - F.2.1 @ i - ,lemIdPProp (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdR C X.1 Y.1 F.1 @ 0) Y.2.2.1) X.2.2.1) - (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdR C X.1 Y.1 F.1 @ 1) Y.2.2.1) X.2.2.1) - (cHSet C X.1 D.2.2.1 (cC C X.1 Y.1 D.2.2.1 (cIdR C X.1 Y.1 F.1 @ 0) Y.2.2.1) X.2.2.1) - (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdR C X.1 Y.1 F.1 @ i) Y.2.2.1) X.2.2.1) - (cospanConeComp C D X Y Y F (cospanConeId C D Y)).2.2 - F.2.2 @ i) - ,\(X Y Z W : cospanCone C D) (F : cospanConeHom C D X Y) (G : cospanConeHom C D Y Z) (H : cospanConeHom C D Z W) -> - (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ i - ,lemIdPProp (Id (cH C X.1 D.2.1.1) (cC C X.1 W.1 D.2.1.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 0) W.2.1) X.2.1) - (Id (cH C X.1 D.2.1.1) (cC C X.1 W.1 D.2.1.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 1) W.2.1) X.2.1) - (cHSet C X.1 D.2.1.1 (cC C X.1 W.1 D.2.1.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 0) W.2.1) X.2.1) - (Id (cH C X.1 D.2.1.1) (cC C X.1 W.1 D.2.1.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ i) W.2.1) X.2.1) - (cospanConeComp C D X Z W (cospanConeComp C D X Y Z F G) H).2.1 - (cospanConeComp C D X Y W F (cospanConeComp C D Y Z W G H)).2.1 @ i - ,lemIdPProp (Id (cH C X.1 D.2.2.1) (cC C X.1 W.1 D.2.2.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 0) W.2.2.1) X.2.2.1) - (Id (cH C X.1 D.2.2.1) (cC C X.1 W.1 D.2.2.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 1) W.2.2.1) X.2.2.1) - (cHSet C X.1 D.2.2.1 (cC C X.1 W.1 D.2.2.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 0) W.2.2.1) X.2.2.1) - (Id (cH C X.1 D.2.2.1) (cC C X.1 W.1 D.2.2.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ i) W.2.2.1) X.2.2.1) - (cospanConeComp C D X Z W (cospanConeComp C D X Y Z F G) H).2.2 - (cospanConeComp C D X Y W F (cospanConeComp C D Y Z W G H)).2.2 @ i)) - -isCategoryCospanCone (C : precategory) (isC : isCategory C) (D : cospan C) - : isCategory (cospanConePrecategory C D) - = undefined - -- = \(A : cospanCone C D) -> - -- let p (X : (B : cospanCone C D) * iso (cospanConePrecategory C D) A B) - -- : Id ((B : cospanCone C D) * iso (cospanConePrecategory C D) A B) (A, isoId (cospanConePrecategory C D) A) X - -- = ((?, ?, ?, ?) - -- ,(?, ?, ?, ?)) - -- in ? - -isFinal (C : precategory) (A : cA C) : U = (B : cA C) -> isContr (cH C B A) -isFinalProp (C : precategory) (A : cA C) : prop (isFinal C A) - = propPi (cA C) (\(B : cA C) -> isContr (cH C B A)) - (\(B : cA C) -> propIsContr (cH C B A)) - -hasFinal (C : precategory) : U = (A : cA C) * isFinal C A - -hasFinalProp (C : precategory) (isC : isCategory C) : prop (hasFinal C) - = \(x y : hasFinal C) -> - let p : iso C x.1 y.1 - = ((y.2 x.1).1, (x.2 y.1).1 - , isContrProp (cH C x.1 x.1) (x.2 x.1) (cC C x.1 y.1 x.1 (y.2 x.1).1 (x.2 y.1).1) (cId C x.1) - , isContrProp (cH C y.1 y.1) (y.2 y.1) (cC C y.1 x.1 y.1 (x.2 y.1).1 (y.2 x.1).1) (cId C y.1)) - in ( lemIsCategory C isC x.1 y.1 p @ i - , lemIdPProp (isFinal C x.1) - (isFinal C y.1) - (isFinalProp C x.1) - ( isFinal C (lemIsCategory C isC x.1 y.1 p @ i)) - x.2 y.2 @ i) - -hasPullbackProp (C : precategory) (isC : isCategory C) (D : cospan C) : prop (hasPullback C D) - = hasFinalProp (cospanConePrecategory C D) (isCategoryCospanCone C isC D) - -isCommutative (CA : precategory) - (A B C D : cA CA) - (f : cH CA A B) (g : cH CA C D) - (h : cH CA A C) (i : cH CA B D) - : U = Id (cH CA A D) (cC CA A C D h g) (cC CA A B D f i) - -pullbackPasting - (CA : precategory) - (A B C D E F : cA CA) - (f : cH CA A B) (g : cH CA B C) - (h : cH CA D E) (i : cH CA E F) - (j : cH CA A D) (k : cH CA B E) (l : cH CA C F) - (cc1 : isCommutative CA A B D E f h j k) - (cc2 : isCommutative CA B C E F g i k l) - (cc3 : isCommutative CA A C D F (cC CA A B C f g) (cC CA D E F h i) j l) - (pb2 : isPullback CA (F, (E, i), (C, l)) (B, k, g, cc2)) - (pb3 : isPullback CA (F, (D, cC CA D E F h i), (C, l)) (A, j, cC CA A B C f g, cc3)) - : isPullback CA (E, (D, h), (B, k)) (A, j, f, cc1) - = \(c : cospanCone CA (E, (D, h), (B, k))) -> - let hole : Id (cH CA c.1 F) - (cC CA c.1 D F c.2.1 (cC CA D E F h i)) - (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l) - = compId (cH CA c.1 F) - (cC CA c.1 D F c.2.1 (cC CA D E F h i)) - (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i) - (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l) - (cIdC CA c.1 D E F c.2.1 h i@-n) - (compId (cH CA c.1 F) - (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i) - (cC CA c.1 E F (cC CA c.1 B E c.2.2.1 k) i) - (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l) - (cC CA c.1 E F (c.2.2.2@n) i) - (compId (cH CA c.1 F) - (cC CA c.1 E F (cC CA c.1 B E c.2.2.1 k) i) - (cC CA c.1 B F c.2.2.1 (cC CA B E F k i)) - (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l) - (cIdC CA c.1 B E F c.2.2.1 k i) - (compId (cH CA c.1 F) - (cC CA c.1 B F c.2.2.1 (cC CA B E F k i)) - (cC CA c.1 B F c.2.2.1 (cC CA B C F g l)) - (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l) - (cC CA c.1 B F c.2.2.1 (cc2@n)) - (cIdC CA c.1 B C F c.2.2.1 g l@-n)))) - c' : cospanCone CA (F, (D, cC CA D E F h i), (C, l)) - = (c.1 - ,c.2.1 - ,cC CA c.1 B C c.2.2.1 g - ,hole) - - hole2 : Id (cH CA c.1 F) - (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i) - (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l) - = compId (cH CA c.1 F) - (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i) - (cC CA c.1 D F c.2.1 (cC CA D E F h i)) - (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l) - (cIdC CA c.1 D E F c.2.1 h i) - hole - cc : cospanCone CA (F, (E, i), (C, l)) - = (c.1, cC CA c.1 D E c.2.1 h, c'.2.2.1, hole2) - - p0 (h' : cH CA c.1 A) (p : Id (cH CA c.1 D) (cC CA c.1 A D h' j) c.2.1) - : Id U (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1) - (Id (cH CA c.1 C) (cC CA c.1 A C h' (cC CA A B C f g)) c'.2.2.1) - = transport - ( Id U (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1) - (Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ i) c'.2.2.1)) - (idProp (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1) - (Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1) - (cHSet CA c.1 B (cC CA c.1 A B h' f) c.2.2.1) - (cHSet CA c.1 C (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1) - (\(p:Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1) -> - cC CA c.1 B C (p@i) g) - (\(p1:Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1) -> - let h1 : cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2) - = (cC CA c.1 A B h' f - ,compId (cH CA c.1 E) - (cC CA c.1 B E (cC CA c.1 A B h' f) k) - (cC CA c.1 A E h' (cC CA A B E f k)) - (cC CA c.1 D E c.2.1 h) - (cIdC CA c.1 A B E h' f k) - (compId (cH CA c.1 E) - (cC CA c.1 A E h' (cC CA A B E f k)) - (cC CA c.1 A E h' (cC CA A D E j h)) - (cC CA c.1 D E c.2.1 h) - (cC CA c.1 A E h' (cc1@-i)) - (compId (cH CA c.1 E) - (cC CA c.1 A E h' (cC CA A D E j h)) - (cC CA c.1 D E (cC CA c.1 A D h' j) h) - (cC CA c.1 D E c.2.1 h) - ( cIdC CA c.1 A D E h' j h @ -i) - ( cC CA c.1 D E (p@i) h))) - ,p1) - h2 : cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2) - = (c.2.2.1 - ,c.2.2.2@-i - ,<_>c'.2.2.1) - in (isContrProp (cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2)) (pb2 cc) h1 h2 @ n).1 - )) - - p : Id U (cospanConeHom CA (F, (D, cC CA D E F h i), (C, l)) c' (A, j, cC CA A B C f g, cc3)) - (cospanConeHom CA (E, (D, h), (B, k)) c (A, j, f, cc1)) - = (h : cH CA c.1 A) - * (p : Id (cH CA c.1 D) (cC CA c.1 A D h j) c.2.1) - * (p0 h p @ -i) - in transport ( isContr (p@i)) (pb3 c') +-- homTo (C : precategory) (X : cA C) : U = (Y : cA C) * cH C Y X +-- cospan (C : precategory) : U +-- = (X : cA C) * (_ : homTo C X) * homTo C X +-- hasCospanCone (C : precategory) (D : cospan C) (W : cA C) : U +-- = (f : cH C W D.2.1.1) * (g : cH C W D.2.2.1) +-- * Id (cH C W D.1) +-- (cC C W D.2.1.1 D.1 f D.2.1.2) +-- (cC C W D.2.2.1 D.1 g D.2.2.2) +-- cospanCone (C : precategory) (D : cospan C) : U = (W : cA C) * hasCospanCone C D W + +-- isCospanConeHom (C : precategory) (D : cospan C) (E1 E2 : cospanCone C D) (h : cH C E1.1 E2.1) : U +-- = (_ : Id (cH C E1.1 D.2.1.1) (cC C E1.1 E2.1 D.2.1.1 h E2.2.1) E1.2.1) +-- * (Id (cH C E1.1 D.2.2.1) (cC C E1.1 E2.1 D.2.2.1 h E2.2.2.1) E1.2.2.1) +-- isCospanConeHomProp (C : precategory) (D : cospan C) (E1 E2 : cospanCone C D) (h : cH C E1.1 E2.1) +-- : prop (isCospanConeHom C D E1 E2 h) +-- = propAnd (Id (cH C E1.1 D.2.1.1) (cC C E1.1 E2.1 D.2.1.1 h E2.2.1) E1.2.1) +-- (Id (cH C E1.1 D.2.2.1) (cC C E1.1 E2.1 D.2.2.1 h E2.2.2.1) E1.2.2.1) +-- (cHSet C E1.1 D.2.1.1 (cC C E1.1 E2.1 D.2.1.1 h E2.2.1) E1.2.1) +-- (cHSet C E1.1 D.2.2.1 (cC C E1.1 E2.1 D.2.2.1 h E2.2.2.1) E1.2.2.1) + +-- cospanConeHom (C : precategory) (D : cospan C) (E1 E2 : cospanCone C D) : U +-- = (h : cH C E1.1 E2.1) * isCospanConeHom C D E1 E2 h +-- cospanConeId (C : precategory) (D : cospan C) (E : cospanCone C D) : cospanConeHom C D E E +-- = (cId C E.1, cIdL C E.1 D.2.1.1 E.2.1, cIdL C E.1 D.2.2.1 E.2.2.1) +-- cospanConeComp (C : precategory) (D : cospan C) (X Y Z : cospanCone C D) +-- (F : cospanConeHom C D X Y) (G : cospanConeHom C D Y Z) : cospanConeHom C D X Z +-- = (cC C X.1 Y.1 Z.1 F.1 G.1 +-- ,compId (cH C X.1 D.2.1.1) +-- (cC C X.1 Z.1 D.2.1.1 (cC C X.1 Y.1 Z.1 F.1 G.1) Z.2.1) +-- (cC C X.1 Y.1 D.2.1.1 F.1 (cC C Y.1 Z.1 D.2.1.1 G.1 Z.2.1)) +-- X.2.1 +-- (cIdC C X.1 Y.1 Z.1 D.2.1.1 F.1 G.1 Z.2.1) +-- (compId (cH C X.1 D.2.1.1) +-- (cC C X.1 Y.1 D.2.1.1 F.1 (cC C Y.1 Z.1 D.2.1.1 G.1 Z.2.1)) +-- (cC C X.1 Y.1 D.2.1.1 F.1 Y.2.1) +-- X.2.1 +-- ( cC C X.1 Y.1 D.2.1.1 F.1 (G.2.1 @ i)) +-- F.2.1) +-- ,compId (cH C X.1 D.2.2.1) +-- (cC C X.1 Z.1 D.2.2.1 (cC C X.1 Y.1 Z.1 F.1 G.1) Z.2.2.1) +-- (cC C X.1 Y.1 D.2.2.1 F.1 (cC C Y.1 Z.1 D.2.2.1 G.1 Z.2.2.1)) +-- X.2.2.1 +-- (cIdC C X.1 Y.1 Z.1 D.2.2.1 F.1 G.1 Z.2.2.1) +-- (compId (cH C X.1 D.2.2.1) +-- (cC C X.1 Y.1 D.2.2.1 F.1 (cC C Y.1 Z.1 D.2.2.1 G.1 Z.2.2.1)) +-- (cC C X.1 Y.1 D.2.2.1 F.1 Y.2.2.1) +-- X.2.2.1 +-- ( cC C X.1 Y.1 D.2.2.1 F.1 (G.2.2 @ i)) +-- F.2.2)) + +-- isPullback (C : precategory) (D : cospan C) (E : cospanCone C D) : U +-- = (h : cospanCone C D) -> isContr (cospanConeHom C D h E) +-- isPullbackProp (C : precategory) (D : cospan C) (E : cospanCone C D) : prop (isPullback C D E) +-- = propPi (cospanCone C D) (\(h : cospanCone C D) -> isContr (cospanConeHom C D h E)) +-- (\(h : cospanCone C D) -> propIsContr (cospanConeHom C D h E)) +-- hasPullback (C : precategory) (D : cospan C) : U = (E : cospanCone C D) * isPullback C D E + +-- cospanConeStructure (C : precategory) (D : cospan C) : structure C +-- = (hasCospanCone C D +-- ,\(x y : cA C) (a : hasCospanCone C D x) (b : hasCospanCone C D y) -> isCospanConeHom C D (x, a) (y, b) +-- ,\(x y : cA C) (a : hasCospanCone C D x) (b : hasCospanCone C D y) -> isCospanConeHomProp C D (x, a) (y, b) +-- ,\(x : cA C) (a : hasCospanCone C D x) -> (cospanConeId C D (x, a)).2 +-- ,\(x y z : cA C) (a : hasCospanCone C D x) (b : hasCospanCone C D y) (c : hasCospanCone C D z) +-- (f : cH C x y) (g : cH C y z) +-- (Hf : isCospanConeHom C D (x, a) (y, b) f) +-- (Hg : isCospanConeHom C D (y, b) (z, c) g) -> (cospanConeComp C D (x, a) (y, b) (z, c) (f, Hf) (g, Hg)).2 +-- ) + +-- cospanConePrecategory (C : precategory) (D : cospan C) : precategory +-- = sipPrecategory C (cospanConeStructure C D) + +-- isCategoryCospanCone (C : precategory) (D : cospan C) (isC : isCategory C) : isCategory (cospanConePrecategory C D) +-- = sip C isC (cospanConeStructure C D) hole +-- where +-- hole : isStandardStructure C (cospanConeStructure C D) +-- = \(x : cA C) (a b : hasCospanCone C D x) +-- (c : isCospanConeHom C D (x, a) (x, b) (cId C x)) +-- (d : isCospanConeHom C D (x, b) (x, a) (cId C x)) -> +-- (compId (cH C x D.2.1.1) a.1 (cC C x x D.2.1.1 (cId C x) a.1) b.1 (cIdL C x D.2.1.1 a.1 @-i) d.1 @ i +-- ,compId (cH C x D.2.2.1) a.2.1 (cC C x x D.2.2.1 (cId C x) a.2.1) b.2.1 (cIdL C x D.2.2.1 a.2.1 @-i) d.2 @ i +-- ,lemIdPProp (Id (cH C x D.1) (cC C x D.2.1.1 D.1 a.1 D.2.1.2) (cC C x D.2.2.1 D.1 a.2.1 D.2.2.2)) +-- (Id (cH C x D.1) (cC C x D.2.1.1 D.1 b.1 D.2.1.2) (cC C x D.2.2.1 D.1 b.2.1 D.2.2.2)) +-- (cHSet C x D.1 (cC C x D.2.1.1 D.1 a.1 D.2.1.2) (cC C x D.2.2.1 D.1 a.2.1 D.2.2.2)) +-- (Id (cH C x D.1) +-- (cC C x D.2.1.1 D.1 (compId (cH C x D.2.1.1) a.1 (cC C x x D.2.1.1 (cId C x) a.1) b.1 +-- (cIdL C x D.2.1.1 a.1 @-i) d.1 @ i) D.2.1.2) +-- (cC C x D.2.2.1 D.1 (compId (cH C x D.2.2.1) a.2.1 (cC C x x D.2.2.1 (cId C x) a.2.1) b.2.1 +-- (cIdL C x D.2.2.1 a.2.1 @-i) d.2 @ i) D.2.2.2)) +-- a.2.2 b.2.2 @ i) + +-- isFinal (C : precategory) (A : cA C) : U = (B : cA C) -> isContr (cH C B A) +-- isFinalProp (C : precategory) (A : cA C) : prop (isFinal C A) +-- = propPi (cA C) (\(B : cA C) -> isContr (cH C B A)) +-- (\(B : cA C) -> propIsContr (cH C B A)) + +-- hasFinal (C : precategory) : U = (A : cA C) * isFinal C A + +-- hasFinalProp (C : precategory) (isC : isCategory C) : prop (hasFinal C) +-- = \(x y : hasFinal C) -> +-- let p : iso C x.1 y.1 +-- = ((y.2 x.1).1, (x.2 y.1).1 +-- , isContrProp (cH C x.1 x.1) (x.2 x.1) (cC C x.1 y.1 x.1 (y.2 x.1).1 (x.2 y.1).1) (cId C x.1) +-- , isContrProp (cH C y.1 y.1) (y.2 y.1) (cC C y.1 x.1 y.1 (x.2 y.1).1 (y.2 x.1).1) (cId C y.1)) +-- in ( (lemIsCategory C isC x.1 y.1 p @ i).1 +-- , lemIdPProp (isFinal C x.1) +-- (isFinal C y.1) +-- (isFinalProp C x.1) +-- ( isFinal C (lemIsCategory C isC x.1 y.1 p @ i).1) +-- x.2 y.2 @ i) + +-- hasPullbackProp (C : precategory) (isC : isCategory C) (D : cospan C) : prop (hasPullback C D) +-- = hasFinalProp (cospanConePrecategory C D) (isCategoryCospanCone C D isC) + +-- isCommutative (CA : precategory) +-- (A B C D : cA CA) +-- (f : cH CA A B) (g : cH CA C D) +-- (h : cH CA A C) (i : cH CA B D) +-- : U = Id (cH CA A D) (cC CA A C D h g) (cC CA A B D f i) + +-- pullbackPasting +-- (CA : precategory) +-- (A B C D E F : cA CA) +-- (f : cH CA A B) (g : cH CA B C) +-- (h : cH CA D E) (i : cH CA E F) +-- (j : cH CA A D) (k : cH CA B E) (l : cH CA C F) +-- (cc1 : isCommutative CA A B D E f h j k) +-- (cc2 : isCommutative CA B C E F g i k l) +-- (cc3 : isCommutative CA A C D F (cC CA A B C f g) (cC CA D E F h i) j l) +-- (pb2 : isPullback CA (F, (E, i), (C, l)) (B, k, g, cc2)) +-- (pb3 : isPullback CA (F, (D, cC CA D E F h i), (C, l)) (A, j, cC CA A B C f g, cc3)) +-- : isPullback CA (E, (D, h), (B, k)) (A, j, f, cc1) +-- = \(c : cospanCone CA (E, (D, h), (B, k))) -> +-- let hole : Id (cH CA c.1 F) +-- (cC CA c.1 D F c.2.1 (cC CA D E F h i)) +-- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l) +-- = compId (cH CA c.1 F) +-- (cC CA c.1 D F c.2.1 (cC CA D E F h i)) +-- (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i) +-- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l) +-- (cIdC CA c.1 D E F c.2.1 h i@-n) +-- (compId (cH CA c.1 F) +-- (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i) +-- (cC CA c.1 E F (cC CA c.1 B E c.2.2.1 k) i) +-- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l) +-- (cC CA c.1 E F (c.2.2.2@n) i) +-- (compId (cH CA c.1 F) +-- (cC CA c.1 E F (cC CA c.1 B E c.2.2.1 k) i) +-- (cC CA c.1 B F c.2.2.1 (cC CA B E F k i)) +-- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l) +-- (cIdC CA c.1 B E F c.2.2.1 k i) +-- (compId (cH CA c.1 F) +-- (cC CA c.1 B F c.2.2.1 (cC CA B E F k i)) +-- (cC CA c.1 B F c.2.2.1 (cC CA B C F g l)) +-- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l) +-- (cC CA c.1 B F c.2.2.1 (cc2@n)) +-- (cIdC CA c.1 B C F c.2.2.1 g l@-n)))) +-- c' : cospanCone CA (F, (D, cC CA D E F h i), (C, l)) +-- = (c.1 +-- ,c.2.1 +-- ,cC CA c.1 B C c.2.2.1 g +-- ,hole) + +-- hole2 : Id (cH CA c.1 F) +-- (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i) +-- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l) +-- = compId (cH CA c.1 F) +-- (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i) +-- (cC CA c.1 D F c.2.1 (cC CA D E F h i)) +-- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l) +-- (cIdC CA c.1 D E F c.2.1 h i) +-- hole +-- cc : cospanCone CA (F, (E, i), (C, l)) +-- = (c.1, cC CA c.1 D E c.2.1 h, c'.2.2.1, hole2) + +-- p0 (h' : cH CA c.1 A) (p : Id (cH CA c.1 D) (cC CA c.1 A D h' j) c.2.1) +-- : Id U (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1) +-- (Id (cH CA c.1 C) (cC CA c.1 A C h' (cC CA A B C f g)) c'.2.2.1) +-- = transport +-- ( Id U (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1) +-- (Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ i) c'.2.2.1)) +-- (idProp (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1) +-- (Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1) +-- (cHSet CA c.1 B (cC CA c.1 A B h' f) c.2.2.1) +-- (cHSet CA c.1 C (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1) +-- (\(p:Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1) -> +-- cC CA c.1 B C (p@i) g) +-- (\(p1:Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1) -> +-- let h1 : cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2) +-- = (cC CA c.1 A B h' f +-- ,compId (cH CA c.1 E) +-- (cC CA c.1 B E (cC CA c.1 A B h' f) k) +-- (cC CA c.1 A E h' (cC CA A B E f k)) +-- (cC CA c.1 D E c.2.1 h) +-- (cIdC CA c.1 A B E h' f k) +-- (compId (cH CA c.1 E) +-- (cC CA c.1 A E h' (cC CA A B E f k)) +-- (cC CA c.1 A E h' (cC CA A D E j h)) +-- (cC CA c.1 D E c.2.1 h) +-- (cC CA c.1 A E h' (cc1@-i)) +-- (compId (cH CA c.1 E) +-- (cC CA c.1 A E h' (cC CA A D E j h)) +-- (cC CA c.1 D E (cC CA c.1 A D h' j) h) +-- (cC CA c.1 D E c.2.1 h) +-- ( cIdC CA c.1 A D E h' j h @ -i) +-- ( cC CA c.1 D E (p@i) h))) +-- ,p1) +-- h2 : cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2) +-- = (c.2.2.1 +-- ,c.2.2.2@-i +-- ,<_>c'.2.2.1) +-- in (isContrProp (cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2)) (pb2 cc) h1 h2 @ n).1 +-- )) + +-- p : Id U (cospanConeHom CA (F, (D, cC CA D E F h i), (C, l)) c' (A, j, cC CA A B C f g, cc3)) +-- (cospanConeHom CA (E, (D, h), (B, k)) c (A, j, f, cc1)) +-- = (h : cH CA c.1 A) +-- * (p : Id (cH CA c.1 D) (cC CA c.1 A D h j) c.2.1) +-- * (p0 h p @ -i) +-- in transport ( isContr (p@i)) (pb3 c')