From: Rafaël Bocquet Date: Thu, 7 Jul 2016 15:33:06 +0000 (+0200) Subject: add some comments in category.ctt and csystem.ctt X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=aae6ae5bd321337450865f5802363f32c3fecdc1;p=cubicaltt.git add some comments in category.ctt and csystem.ctt --- diff --git a/examples/category.ctt b/examples/category.ctt index 0bf48de..7209535 100644 --- a/examples/category.ctt +++ b/examples/category.ctt @@ -63,6 +63,7 @@ opaque lemTransEquiv categoryData : U = (A : U) * (A -> A -> U) +-- Propositional data of a precategory isPrecategory2 (C : categoryData) (id : (x : C.1) -> C.2 x x) (c : (x y z : C.1) -> C.2 x y -> C.2 y z -> C.2 x z) : U = let A : U = C.1 hom : A -> A -> U = C.2 @@ -126,322 +127,69 @@ 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)) +-- +-- Isomorphisms +-- -eCatIso3 (A B : precategory) : Id U (Id precategory A B) (catIso3 A B) - = isoId (Id precategory A B) (catIso3 A B) - F G FG GF - where - F (e:Id precategory A B):catIso3 A B = ((e@i).1.1, (e@i).1.2, (e@i).2.1, (e@i).2.2.1) - G (e:catIso3 A B):Id precategory A B = ((e.1@i, e.2.1@i), e.2.2.1@i, e.2.2.2@i - ,lemIdPProp (isPrecategory2 A.1 A.2.1 A.2.2.1) - (isPrecategory2 B.1 B.2.1 B.2.2.1) - (propIsPrecategory2 A.1 A.2.1 A.2.2.1) - (isPrecategory2 (e.1@i, e.2.1@i) (e.2.2.1@i) (e.2.2.2@i)) - A.2.2.2 B.2.2.2 @ i) - FG(e:catIso3 A B):Id (catIso3 A B) (F (G e)) e=<_>e - GF(e:Id precategory A B):Id (Id precategory A B) (G (F e)) e - =((e@j).1, (e@j).2.1, (e@j).2.2.1 - ,lemIdPSet (isPrecategory2 A.1 A.2.1 A.2.2.1) - (isPrecategory2 B.1 B.2.1 B.2.2.1) - (propSet (isPrecategory2 A.1 A.2.1 A.2.2.1) (propIsPrecategory2 A.1 A.2.1 A.2.2.1)) - (isPrecategory2 (e@i).1 (e@i).2.1 (e@i).2.2.1) - A.2.2.2 B.2.2.2 - ( (G (F e)@j).2.2.2) ((e@j).2.2.2) - @ i @ j) +iso (C : precategory) (A B : cA C) : U + = (f : cH C A B) * (g : cH C B A) + * (_ : 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)) -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)))) -eCatIso30 (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 - ]))) +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 -catIso311 (A B : precategory) (e1:Id U (cA A) (cA B)) : U - = Id ((x y : cA A)->U) (cH A) (\(x y:cA A)->cH B (transport e1 x) (transport e1 y)) -catIso312 (A B : precategory) (e1:Id U (cA A) (cA B)) (e2:catIso311 A B e1) : U - = Id ((x:cA A)->cH B (transport e1 x) (transport e1 x)) - (\(x:cA A)->transport ( (e2@i) x x) (cId A x)) - (\(x : cA A) -> cId B (transport e1 x)) -catIso313 (A B : precategory) (e1:Id U (cA A) (cA B)) (e2:catIso311 A B e1) : U - = Id ((x y z:cA A)->cH A x y->cH A y z->cH B (transport e1 x) (transport e1 z)) - (\(x y z:cA A)(f:cH A x y)(g:cH A y z)->transport ((e2@i)x z) (cC A x y z f g)) - (\(x y z:cA A)(f:cH A x y)(g:cH A y 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 : catIso311 A B e1) - * (_ : catIso312 A B e1 e2) - * ( catIso313 A B e1 e2) +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)) -eCatIso31 (A B : precategory) : Id U (catIso30 A B) (catIso31 A B) - = (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))) - * (_:comp (<_> U) - (Id ((x:cA A)->(e2@i) x x) - (\(x:cA A)->transport ( (e2@i/\j) x x) (cId A x)) - (\(x:cA A)->transport ( (e2@i\/-j) x x) (cId B (transport e1 x)))) - [(i=0)->Id ((x:cA A)->cH A x x) - (\(x:cA A)->transRefl (cH A x x) (cId A x) @ k) - (\(x:cA A)->transport ( (e2@-j) x x) (cId B (transport e1 x))) - ,(i=1)->Id ((x:cA A)->(e2@i) x x) - (\(x:cA A)->transport ( (e2@j) x x) (cId A x)) - (\(x:cA A)->transRefl ((e2@1) x x) (cId B (transport e1 x)) @ k) - ]) - * (comp (<_> U) - (Id ((x y z:cA A)->cH A x y->cH A y z->(e2@i) x z) - (\(x y z:cA A)(f:cH A x y)(g:cH A y z)-> - transport ( (e2@i/\j) x 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\/-j) x z) - (cC B (transport e1 x) (transport e1 y) (transport e1 z) - (transport ((e2@j) x y) f) - (transport ((e2@j) y z) g)))) - [(i=0)->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)-> - transRefl ((e2@0) x z) (cC A x y z f g) @ k) - (\(x y z:cA A)(f:cH A x y)(g:cH A y z)-> - transport ((e2@-j) x z) - (cC B (transport e1 x) (transport e1 y) (transport e1 z) - (transport ((e2@j) x y) f) - (transport ((e2@j) y z) g))) - ,(i=1)->Id ((x y z:cA A)->cH A x y->cH A y z->(e2@1) x z) - (\(x y z:cA A)(f:cH A x y)(g:cH A y z)-> - transport ((e2@j) x z) (cC A x y z f g)) - (\(x y z:cA A)(f:cH A x y)(g:cH A y z)-> - transRefl ((e2@1) x z) - (cC B (transport e1 x) (transport e1 y) (transport e1 z) - (transport ((e2@j) x y) f) - (transport ((e2@j) y z) g)) @ k) - ]) +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) -lemEquivCoh (A B:U) (e:equiv A B) (x:A) - : Id (Id B (e.1 x) (e.1 (invEq A B e (e.1 x)))) - (e.1(secEq A B e x@-j)) - (retEq A B e (e.1 x)@-j) - = comp ( Id B (e.1 x) (e.1 (secEq A B e x @ -i /\ -j))) - (((e.2 (e.1 x)).2 (x,<_>e.1 x)@-i).2) - [(i=0)->e.1 (secEq A B e x@-k\/-j) - ,(i=1)->retEq A B e (e.1 x)@-k - ] +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) -sigEquivLem (A A':U) (B:A->U) (B':A'->U) - (e:equiv A A') - (f:(x:A)->equiv (B x) (B' (e.1 x))) - : equiv (Sigma A B) (Sigma A' B') - = (F, gradLemma (Sigma A B) (Sigma A' B') F G FG GF) - where - F (x:Sigma A B):Sigma A' B' = (e.1 x.1, (f x.1).1 x.2) - G (x:Sigma A' B'):Sigma A B = ((e.2 x.1).1.1, ((f (e.2 x.1).1.1).2 (transport ( B' ((e.2 x.1).1.2 @ i)) x.2)).1.1) - FG (x:Sigma A' B'):Id (Sigma A' B') (F (G x)) x - = ((e.2 x.1).1.2 @ -i - ,comp (<_> B' ((e.2 x.1).1.2 @ -i)) - (transport ( B' ((e.2 x.1).1.2 @ j/\-i)) x.2) - [(i=0)->((f (e.2 x.1).1.1).2 (transport ( B' ((e.2 x.1).1.2 @ i)) x.2)).1.2 @ j - ,(i=1)->transRefl (B' ((e.2 x.1).1.2 @ 0)) x.2@j - ]) - GF (x:Sigma A B):Id (Sigma A B) (G (F x)) x - = (secEq A A' e x.1 @ i - ,comp (<_> B (secEq A A' e x.1 @ i)) - ((f (secEq A A' e x.1 @ i)).2 (transport ( B' (e.1 (secEq A A' e x.1 @ i\/-j))) ((f x.1).1 x.2))).1.1 - [(i=0)->((f (secEq A A' e x.1 @ 0)).2 (transport ( B' (lemEquivCoh A A' e x.1@k@i)) ((f x.1).1 x.2))).1.1 - ,(i=1)->compId (B x.1) - ((f x.1).2 (transport ( B' (e.1 x.1)) ((f x.1).1 x.2))).1.1 - ((f x.1).2 ((f x.1).1 x.2)).1.1 - x.2 - (((f x.1).2 (transRefl (B' (e.1 x.1)) ((f x.1).1 x.2)@k)).1.1) - (secEq (B x.1) (B' (e.1 x.1)) (f x.1) x.2) @ k - ]) +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 -sigEquivLem' (A A':U) (B:A->U) (B':A'->U) - (e:equiv A A') - (f:(x:A)->Id U (B x) (B' (e.1 x))) - : Id U (Sigma A B) (Sigma A' B') - = transEquivToId (Sigma A B) (Sigma A' B') (sigEquivLem A A' B B' e (\(x:A)->transEquiv' (B' (e.1 x)) (B x) (f x))) - -catIso321 (A B : precategory) (e1:Id U (cA A) (cA B)) : U - = (x y:cA A) -> Id U (cH A x y) (cH B (transport e1 x) (transport e1 y)) -catIso322 (A B : precategory) (e1:Id U (cA A) (cA B)) (e2:catIso321 A B e1) : U - = (x:cA A) -> Id (cH B (transport e1 x) (transport e1 x)) - (transport (e2 x x) (cId A x)) - (cId B (transport e1 x)) -catIso323 (A B : precategory) (e1:Id U (cA A) (cA B)) (e2:catIso321 A B e1) : U - = (x y z:cA A)(f:cH A x y)(g:cH A y z)-> - Id (cH B (transport e1 x) (transport e1 z)) - (transport (e2 x z) (cC A x y z f g)) - (cC B (transport e1 x) (transport e1 y) (transport e1 z) - (transport (e2 x y) f) - (transport (e2 y z) g)) -catIso32 (A B : precategory) : U = (e1 : Id U (cA A) (cA B)) - * (e2 : catIso321 A B e1) - * (_ : catIso322 A B e1 e2) - * ( catIso323 A B e1 e2) - -eCatIso32 (A B : precategory) : Id U (catIso31 A B) (catIso32 A B) - = (e1 : Id U (cA A) (cA B)) - * (let F(e2:catIso311 A B e1):catIso321 A B e1 = \(x y:cA A)->(e2@i) x y in - transEquivToId - ((e2 : catIso311 A B e1) * (_ : catIso312 A B e1 e2) * ( catIso313 A B e1 e2)) - ((e2 : catIso321 A B e1) * (_ : catIso322 A B e1 e2) * ( catIso323 A B e1 e2)) - (sigEquivLem (catIso311 A B e1) (catIso321 A B e1) - (\(e2 : catIso311 A B e1) -> (_ : catIso312 A B e1 e2) * ( catIso313 A B e1 e2)) - (\(e2 : catIso321 A B e1) -> (_ : catIso322 A B e1 e2) * ( catIso323 A B e1 e2)) - (F, gradLemma (catIso311 A B e1) (catIso321 A B e1) - F (\(e2:catIso321 A B e1)->\(x y:cA A)->(e2 x y)@i) - (\(e2:catIso321 A B e1)-><_>e2) (\(e2:catIso311 A B e1)-><_>e2)) - (\(e2:catIso311 A B e1)-> - (sigEquivLem (catIso312 A B e1 e2) (catIso322 A B e1 (F e2)) - (\(_ : catIso312 A B e1 e2) -> (catIso313 A B e1 e2)) - (\(_ : catIso322 A B e1 (F e2)) -> (catIso323 A B e1 (F e2))) - (let F2(e:catIso312 A B e1 e2):catIso322 A B e1 (F e2)=\(x:cA A)->(e@i)x in - (F2, gradLemma (catIso312 A B e1 e2) (catIso322 A B e1 (F e2)) - F2 (\(e:catIso322 A B e1 (F e2))->\(x:cA A)->(e x)@i) - (\(e:catIso322 A B e1 (F e2))-><_>e) (\(e:catIso312 A B e1 e2)-><_>e))) - (\(_:catIso312 A B e1 e2)-> - (let F3(e:catIso313 A B e1 e2):catIso323 A B e1 (F e2)=\(x y z:cA A)(f:cH A x y)(g:cH A y z)->(e@i)x y z f g in - (F3, gradLemma (catIso313 A B e1 e2) (catIso323 A B e1 (F e2)) - F3 (\(e:catIso323 A B e1 (F e2))->\(x y z:cA A)(f:cH A x y)(g:cH A y z)->(e x y z f g)@i) - (\(e:catIso323 A B e1 (F e2))-><_>e) (\(e:catIso313 A B e1 e2)-><_>e)) - )))))) @ i - --- - -iso (C : precategory) (A B : cA C) : U - = (f : cH C A B) * (g : cH C B A) - * (_ : 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)) - -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)) +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) @@ -460,6 +208,10 @@ opaque IdInvLIso opaque compIso +-- +-- Categories +-- + 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) (idIso C A) B p @@ -490,7 +242,9 @@ setCat : precategory ,\(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 --- sip +-- +-- the structure identity principle +-- structure (X : precategory) : U = (P : cA X -> U) @@ -553,6 +307,7 @@ isContrProp (A : U) (p : isContr A) (x y : A) : Id A x y = compId A x p.1 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) +-- the uncommented definition is a bit slow to typecheck sip (X : precategory) (isC : isCategory X) (S : structure X) (isS : isStandardStructure X S) : isCategory (sipPrecategory X S) = undefined -- = hole @@ -647,6 +402,8 @@ sip (X : precategory) (isC : isCategory X) (S : structure X) (isS : isStandardSt -- hole (A : cA D) : isContr ((B : cA D) * iso D A B) = transport (isContr(eq1 A@-i)) (hole0 A) opaque sip +-- +-- Functors -- functor (A B : precategory) : U @@ -704,149 +461,411 @@ lem10' (A B : U) (e : equiv A B) (x y : A) (p : Id B (e.1 x) (e.1 y)) : Id A x y (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 +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 + +-- the uncommented definition is a bit slow to typecheck +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 + +-- +-- Equivalences of precategories +-- + +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)) +catIdIsEquiv (A : precategory) : catIsEquiv A A (idFunctor A) + = (\(a b : cA A) -> idIsEquiv (cH A a b) + ,\(b:cA A) -> (b, idIso A b)) +catIdEquiv (A : precategory) : catEquiv A A = (idFunctor A, catIdIsEquiv A) + +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 + +-------------------------------------------------------------------------------- +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)) + +eCatIso3 (A B : precategory) : Id U (Id precategory A B) (catIso3 A B) + = isoId (Id precategory A B) (catIso3 A B) + F G FG GF + where + F (e:Id precategory A B):catIso3 A B = ((e@i).1.1, (e@i).1.2, (e@i).2.1, (e@i).2.2.1) + G (e:catIso3 A B):Id precategory A B = ((e.1@i, e.2.1@i), e.2.2.1@i, e.2.2.2@i + ,lemIdPProp (isPrecategory2 A.1 A.2.1 A.2.2.1) + (isPrecategory2 B.1 B.2.1 B.2.2.1) + (propIsPrecategory2 A.1 A.2.1 A.2.2.1) + (isPrecategory2 (e.1@i, e.2.1@i) (e.2.2.1@i) (e.2.2.2@i)) + A.2.2.2 B.2.2.2 @ i) + FG(e:catIso3 A B):Id (catIso3 A B) (F (G e)) e=<_>e + GF(e:Id precategory A B):Id (Id precategory A B) (G (F e)) e + =((e@j).1, (e@j).2.1, (e@j).2.2.1 + ,lemIdPSet (isPrecategory2 A.1 A.2.1 A.2.2.1) + (isPrecategory2 B.1 B.2.1 B.2.2.1) + (propSet (isPrecategory2 A.1 A.2.1 A.2.2.1) (propIsPrecategory2 A.1 A.2.1 A.2.2.1)) + (isPrecategory2 (e@i).1 (e@i).2.1 (e@i).2.2.1) + A.2.2.2 B.2.2.2 + ( (G (F e)@j).2.2.2) ((e@j).2.2.2) + @ i @ j) + +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)))) + +eCatIso30 (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 + ]))) + +catIso311 (A B : precategory) (e1:Id U (cA A) (cA B)) : U + = Id ((x y : cA A)->U) (cH A) (\(x y:cA A)->cH B (transport e1 x) (transport e1 y)) +catIso312 (A B : precategory) (e1:Id U (cA A) (cA B)) (e2:catIso311 A B e1) : U + = Id ((x:cA A)->cH B (transport e1 x) (transport e1 x)) + (\(x:cA A)->transport ( (e2@i) x x) (cId A x)) + (\(x : cA A) -> cId B (transport e1 x)) +catIso313 (A B : precategory) (e1:Id U (cA A) (cA B)) (e2:catIso311 A B e1) : U + = Id ((x y z:cA A)->cH A x y->cH A y z->cH B (transport e1 x) (transport e1 z)) + (\(x y z:cA A)(f:cH A x y)(g:cH A y z)->transport ((e2@i)x z) (cC A x y z f g)) + (\(x y z:cA A)(f:cH A x y)(g:cH A y 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 : catIso311 A B e1) + * (_ : catIso312 A B e1 e2) + * ( catIso313 A B e1 e2) + +eCatIso31 (A B : precategory) : Id U (catIso30 A B) (catIso31 A B) + = (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))) + * (_:comp (<_> U) + (Id ((x:cA A)->(e2@i) x x) + (\(x:cA A)->transport ( (e2@i/\j) x x) (cId A x)) + (\(x:cA A)->transport ( (e2@i\/-j) x x) (cId B (transport e1 x)))) + [(i=0)->Id ((x:cA A)->cH A x x) + (\(x:cA A)->transRefl (cH A x x) (cId A x) @ k) + (\(x:cA A)->transport ( (e2@-j) x x) (cId B (transport e1 x))) + ,(i=1)->Id ((x:cA A)->(e2@i) x x) + (\(x:cA A)->transport ( (e2@j) x x) (cId A x)) + (\(x:cA A)->transRefl ((e2@1) x x) (cId B (transport e1 x)) @ k) + ]) + * (comp (<_> U) + (Id ((x y z:cA A)->cH A x y->cH A y z->(e2@i) x z) + (\(x y z:cA A)(f:cH A x y)(g:cH A y z)-> + transport ( (e2@i/\j) x 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\/-j) x z) + (cC B (transport e1 x) (transport e1 y) (transport e1 z) + (transport ((e2@j) x y) f) + (transport ((e2@j) y z) g)))) + [(i=0)->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)-> + transRefl ((e2@0) x z) (cC A x y z f g) @ k) + (\(x y z:cA A)(f:cH A x y)(g:cH A y z)-> + transport ((e2@-j) x z) + (cC B (transport e1 x) (transport e1 y) (transport e1 z) + (transport ((e2@j) x y) f) + (transport ((e2@j) y z) g))) + ,(i=1)->Id ((x y z:cA A)->cH A x y->cH A y z->(e2@1) x z) + (\(x y z:cA A)(f:cH A x y)(g:cH A y z)-> + transport ((e2@j) x z) (cC A x y z f g)) + (\(x y z:cA A)(f:cH A x y)(g:cH A y z)-> + transRefl ((e2@1) x z) + (cC B (transport e1 x) (transport e1 y) (transport e1 z) + (transport ((e2@j) x y) f) + (transport ((e2@j) y z) g)) @ k) + ]) + +lemEquivCoh (A B:U) (e:equiv A B) (x:A) + : Id (Id B (e.1 x) (e.1 (invEq A B e (e.1 x)))) + (e.1(secEq A B e x@-j)) + (retEq A B e (e.1 x)@-j) + = comp ( Id B (e.1 x) (e.1 (secEq A B e x @ -i /\ -j))) + (((e.2 (e.1 x)).2 (x,<_>e.1 x)@-i).2) + [(i=0)->e.1 (secEq A B e x@-k\/-j) + ,(i=1)->retEq A B e (e.1 x)@-k + ] -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 +sigEquivLem (A A':U) (B:A->U) (B':A'->U) + (e:equiv A A') + (f:(x:A)->equiv (B x) (B' (e.1 x))) + : equiv (Sigma A B) (Sigma A' B') + = (F, gradLemma (Sigma A B) (Sigma A' B') F G FG GF) 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 + F (x:Sigma A B):Sigma A' B' = (e.1 x.1, (f x.1).1 x.2) + G (x:Sigma A' B'):Sigma A B = ((e.2 x.1).1.1, ((f (e.2 x.1).1.1).2 (transport ( B' ((e.2 x.1).1.2 @ i)) x.2)).1.1) + FG (x:Sigma A' B'):Id (Sigma A' B') (F (G x)) x + = ((e.2 x.1).1.2 @ -i + ,comp (<_> B' ((e.2 x.1).1.2 @ -i)) + (transport ( B' ((e.2 x.1).1.2 @ j/\-i)) x.2) + [(i=0)->((f (e.2 x.1).1.1).2 (transport ( B' ((e.2 x.1).1.2 @ i)) x.2)).1.2 @ j + ,(i=1)->transRefl (B' ((e.2 x.1).1.2 @ 0)) x.2@j + ]) + GF (x:Sigma A B):Id (Sigma A B) (G (F x)) x + = (secEq A A' e x.1 @ i + ,comp (<_> B (secEq A A' e x.1 @ i)) + ((f (secEq A A' e x.1 @ i)).2 (transport ( B' (e.1 (secEq A A' e x.1 @ i\/-j))) ((f x.1).1 x.2))).1.1 + [(i=0)->((f (secEq A A' e x.1 @ 0)).2 (transport ( B' (lemEquivCoh A A' e x.1@k@i)) ((f x.1).1 x.2))).1.1 + ,(i=1)->compId (B x.1) + ((f x.1).2 (transport ( B' (e.1 x.1)) ((f x.1).1 x.2))).1.1 + ((f x.1).2 ((f x.1).1 x.2)).1.1 + x.2 + (((f x.1).2 (transRefl (B' (e.1 x.1)) ((f x.1).1 x.2)@k)).1.1) + (secEq (B x.1) (B' (e.1 x.1)) (f x.1) x.2) @ k + ]) -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 +sigEquivLem' (A A':U) (B:A->U) (B':A'->U) + (e:equiv A A') + (f:(x:A)->Id U (B x) (B' (e.1 x))) + : Id U (Sigma A B) (Sigma A' B') + = transEquivToId (Sigma A B) (Sigma A' B') (sigEquivLem A A' B B' e (\(x:A)->transEquiv' (B' (e.1 x)) (B x) (f x))) -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)) -catIdIsEquiv (A : precategory) : catIsEquiv A A (idFunctor A) - = (\(a b : cA A) -> idIsEquiv (cH A a b) - ,\(b:cA A) -> (b, idIso A b)) -catIdEquiv (A : precategory) : catEquiv A A = (idFunctor A, catIdIsEquiv A) +catIso321 (A B : precategory) (e1:Id U (cA A) (cA B)) : U + = (x y:cA A) -> Id U (cH A x y) (cH B (transport e1 x) (transport e1 y)) +catIso322 (A B : precategory) (e1:Id U (cA A) (cA B)) (e2:catIso321 A B e1) : U + = (x:cA A) -> Id (cH B (transport e1 x) (transport e1 x)) + (transport (e2 x x) (cId A x)) + (cId B (transport e1 x)) +catIso323 (A B : precategory) (e1:Id U (cA A) (cA B)) (e2:catIso321 A B e1) : U + = (x y z:cA A)(f:cH A x y)(g:cH A y z)-> + Id (cH B (transport e1 x) (transport e1 z)) + (transport (e2 x z) (cC A x y z f g)) + (cC B (transport e1 x) (transport e1 y) (transport e1 z) + (transport (e2 x y) f) + (transport (e2 y z) g)) +catIso32 (A B : precategory) : U = (e1 : Id U (cA A) (cA B)) + * (e2 : catIso321 A B e1) + * (_ : catIso322 A B e1 e2) + * ( catIso323 A B e1 e2) -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 +eCatIso32 (A B : precategory) : Id U (catIso31 A B) (catIso32 A B) + = (e1 : Id U (cA A) (cA B)) + * (let F(e2:catIso311 A B e1):catIso321 A B e1 = \(x y:cA A)->(e2@i) x y in + transEquivToId + ((e2 : catIso311 A B e1) * (_ : catIso312 A B e1 e2) * ( catIso313 A B e1 e2)) + ((e2 : catIso321 A B e1) * (_ : catIso322 A B e1 e2) * ( catIso323 A B e1 e2)) + (sigEquivLem (catIso311 A B e1) (catIso321 A B e1) + (\(e2 : catIso311 A B e1) -> (_ : catIso312 A B e1 e2) * ( catIso313 A B e1 e2)) + (\(e2 : catIso321 A B e1) -> (_ : catIso322 A B e1 e2) * ( catIso323 A B e1 e2)) + (F, gradLemma (catIso311 A B e1) (catIso321 A B e1) + F (\(e2:catIso321 A B e1)->\(x y:cA A)->(e2 x y)@i) + (\(e2:catIso321 A B e1)-><_>e2) (\(e2:catIso311 A B e1)-><_>e2)) + (\(e2:catIso311 A B e1)-> + (sigEquivLem (catIso312 A B e1 e2) (catIso322 A B e1 (F e2)) + (\(_ : catIso312 A B e1 e2) -> (catIso313 A B e1 e2)) + (\(_ : catIso322 A B e1 (F e2)) -> (catIso323 A B e1 (F e2))) + (let F2(e:catIso312 A B e1 e2):catIso322 A B e1 (F e2)=\(x:cA A)->(e@i)x in + (F2, gradLemma (catIso312 A B e1 e2) (catIso322 A B e1 (F e2)) + F2 (\(e:catIso322 A B e1 (F e2))->\(x:cA A)->(e x)@i) + (\(e:catIso322 A B e1 (F e2))-><_>e) (\(e:catIso312 A B e1 e2)-><_>e))) + (\(_:catIso312 A B e1 e2)-> + (let F3(e:catIso313 A B e1 e2):catIso323 A B e1 (F e2)=\(x y z:cA A)(f:cH A x y)(g:cH A y z)->(e@i)x y z f g in + (F3, gradLemma (catIso313 A B e1 e2) (catIso323 A B e1 (F e2)) + F3 (\(e:catIso323 A B e1 (F e2))->\(x y z:cA A)(f:cH A x y)(g:cH A y z)->(e x y z f g)@i) + (\(e:catIso323 A B e1 (F e2))-><_>e) (\(e:catIso313 A B e1 e2)-><_>e)) + )))))) @ i catIso21 (A B : precategory) (e1:equiv (cA A) (cA B)) : U = (x y:cA A) -> equiv (cH A x y) (cH B (e1.1 x) (e1.1 y)) @@ -930,6 +949,7 @@ eCatIso2 (A B:precategory):Id U (catIso32 A B) (catIso2 A B) (cC B (transport e1 x) (transport e1 y) (transport e1 z) (p2 x y f@i) (p2 y z g@i))) ))) +-------------------------------------------------------------------------------- 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))) @@ -971,6 +991,7 @@ catIsoEqId (A B : precategory) : Id U (catIso A B) (Id precategory A B) catEquivEqId (A B : precategory) (isCA : isCategory A) (isCB : isCategory B) : Id U (catEquiv A B) (Id precategory A B) = compId U (catEquiv A B) (catIso A B) (Id precategory A B) (catEquivEqIso A B isCA isCB) (catIsoEqId A B) +opaque catEquivEqId catEquivEqId' (A : category) : isContr ((B : category) * catEquiv A.1 B.1) = transport ( isContr ((B : category) * catEquivEqId A.1 B.1 A.2 B.2@-i)) @@ -983,6 +1004,11 @@ catEquivEqId' (A : category) : isContr ((B : category) * catEquiv A.1 B.1) ( isCategory (BB.2@i)) A.2 BB.1.2 @ i) , BB.2@i/\j)) +opaque catEquivEqId' + +-- +-- Pullbacks +-- -- f' -- W -----> Z diff --git a/examples/csystem.ctt b/examples/csystem.ctt index 7fd2875..d4ade76 100644 --- a/examples/csystem.ctt +++ b/examples/csystem.ctt @@ -9,6 +9,20 @@ mkFt (ob : nat -> U) (ft0 : (n : nat) -> ob (suc n) -> ob n) : (n : nat) -> ob n zero -> \(x : ob zero) -> (zero, x) suc n -> \(x : ob (suc n)) -> (n, ft0 n x) +-- +-- C0-Systems +-- Objects of C0-systems are given by a length indexed family "ob : nat -> U", to avoid equalities on object lengths +-- The ??? morphisms (p : (x y : A) -> Id A (ft x) y -> hom x y) depend on a path in "Id A (ft x) y" because we can't +-- enforce a definitional equality in "Id A (ft f*(X)) Y" in this square : +-- +-- q(f, X) +-- f*(X) ----> X +-- | | +-- | | p_X +-- | | +-- Y -------> ft(X) +-- f +-- isC0System (ob : nat -> U) (hom : Sigma nat ob -> Sigma nat ob -> U) (isC : isPrecategory (Sigma nat ob, hom)) : U = let A : U = Sigma nat ob CD : categoryData = (A,hom) @@ -74,30 +88,39 @@ c0Square (C : C0System) (T : c0CanSq C) c0FtH (C : C0System) (Y X : cA (c0C C)) (f : cH (c0C C) Y X) : cH (c0C C) Y (c0Ft C X) = cC (c0C C) Y X (c0Ft C X) f (c0P C X (c0Ft C X) (<_> c0Ft C X)) -isCSystem2Cospan (C : C0System) (T : c0CanSq C) : cospan (c0C C) +-- +-- A C0-system is a C-system if all of its canonical squares ("c0CanSq C") are pullback squares +-- + +isCSystemCospan (C : C0System) (T : c0CanSq C) : cospan (c0C C) = let X : cA (c0C C) = (suc T.1, T.2.1) in (c0Ft C X, (T.2.2.1, T.2.2.2), (X, c0P C X (c0Ft C X) (<_>c0Ft C X))) -isCSystem2CospanCone (C : C0System) (T : c0CanSq C) : cospanCone (c0C C) (isCSystem2Cospan C T) +isCSystemCospanCone (C : C0System) (T : c0CanSq C) : cospanCone (c0C C) (isCSystemCospan C T) = (c0Star C T, c0P C (c0Star C T) T.2.2.1 (c0FtStar C T), c0Q C T, c0Square C T) -isCSystem2Type (C : C0System) (T : c0CanSq C) : U +isCSystemType (C : C0System) (T : c0CanSq C) : U = isPullback (c0C C) - (isCSystem2Cospan C T) - (isCSystem2CospanCone C T) -isCSystem2 (C : C0System) : U - = (T : c0CanSq C) -> isCSystem2Type C T + (isCSystemCospan C T) + (isCSystemCospanCone C T) +isCSystem (C : C0System) : U + = (T : c0CanSq C) -> isCSystemType C T + +isCSystemProp (C : C0System) : prop (isCSystem C) + = propPi (c0CanSq C) (\(T : c0CanSq C) -> isCSystemType C T) + (\(T : c0CanSq C) -> isPullbackProp (c0C C) (isCSystemCospan C T) (isCSystemCospanCone C T)) -isCSystem2Prop (C : C0System) : prop (isCSystem2 C) - = propPi (c0CanSq C) (\(T : c0CanSq C) -> isCSystem2Type C T) - (\(T : c0CanSq C) -> isPullbackProp (c0C C) (isCSystem2Cospan C T) (isCSystem2CospanCone C T)) +CSystem : U = (ob : nat -> U) * (hom : Sigma nat ob -> Sigma nat ob -> U) * (isC : isPrecategory (Sigma nat ob, hom)) + * (c0 : isC0System ob hom isC) * isCSystem (ob, hom, isC, c0) -- +-- Definition of a universe category +-- uc : U = (C : precategory) @@ -106,6 +129,7 @@ uc : U * (V : cA C) * (VT : cA C) * (p : cH C VT V) * ((f : homTo C V) -> hasPullback C (V, f, VT, p)) +-- An equivalence of universe categories is an equivalence of categories compatible with the "p" morphism ucEquiv (A B : uc) : U = (e : catEquiv A.1 B.1) * (V : Id (cA B.1) (e.1.1 A.2.2.2.1) B.2.2.2.1) @@ -115,6 +139,14 @@ ucEquiv (A B : uc) : U ucEquivId (A B : uc) (e : ucEquiv A B) : Id uc A B = let p : Id ((C:category)*catEquiv A.1 C.1) ((A.1, A.2.1), catIdEquiv A.1) ((B.1, B.2.1), e.1) = isContrProp ((C:category)*catEquiv A.1 C.1) (catEquivEqId' (A.1, A.2.1)) ((A.1, A.2.1), catIdEquiv A.1) ((B.1, B.2.1), e.1) + opaque p + pFinal : IdP ( hasFinal (p@i).1.1) A.2.2.1 B.2.2.1 + = lemIdPProp (hasFinal A.1) + (hasFinal B.1) + (hasFinalProp A.1 A.2.1) + (hasFinal (p@i).1.1) + A.2.2.1 B.2.2.1 + opaque pFinal pV : IdP ( cA (p@i).1.1) A.2.2.2.1 B.2.2.2.1 = comp (<_> cA (p@i).1.1) ((p@i).2.1.1 A.2.2.2.1) [(i=0)-><_>A.2.2.2.1 ,(i=1)->e.2.1@k] @@ -127,22 +159,29 @@ ucEquivId (A B : uc) (e : ucEquiv A B) : Id uc A B (fill (<_> cA (p@i).1.1) ((p@i).2.1.1 A.2.2.2.1) [(i=0)-><_>A.2.2.2.1 ,(i=1)->e.2.1@k]@k)) ((p@i).2.1.2.1 A.2.2.2.2.1 A.2.2.2.1 A.2.2.2.2.2.1) [(i=0)-><_>A.2.2.2.2.2.1, (i=1)->e.2.2.2@k] + opaque pV + opaque pVT + opaque pP + pPb : IdP ( (f : homTo (p@i).1.1 (pV@i)) -> hasPullback (p@i).1.1 (pV@i, f, pVT@i, pP@i)) A.2.2.2.2.2.2 B.2.2.2.2.2.2 + = lemIdPProp ((f : homTo A.1 (pV@0)) -> hasPullback A.1 (pV@0, f, pVT@0, pP@0)) + ((f : homTo B.1 (pV@1)) -> hasPullback B.1 (pV@1, f, pVT@1, pP@1)) + (propPi (homTo A.1 (pV@0)) (\(f : homTo A.1 (pV@0)) -> hasPullback A.1 (pV@0, f, pVT@0, pP@0)) + (\(f : homTo A.1 (pV@0)) -> hasPullbackProp A.1 A.2.1 (pV@0, f, pVT@0, pP@0))) + ((f : homTo (p@i).1.1 (pV@i)) -> hasPullback (p@i).1.1 (pV@i, f, pVT@i, pP@i)) + A.2.2.2.2.2.2 B.2.2.2.2.2.2 + opaque pPb + t:nat=zero in ((p@i).1.1 ,(p@i).1.2 - ,lemIdPProp (hasFinal A.1) - (hasFinal B.1) - (hasFinalProp A.1 A.2.1) - (hasFinal (p@i).1.1) - A.2.2.1 B.2.2.1 @ i + ,pFinal@i ,pV@i, pVT@i, pP@i - ,lemIdPProp ((f : homTo A.1 (pV@0)) -> hasPullback A.1 (pV@0, f, pVT@0, pP@0)) - ((f : homTo B.1 (pV@1)) -> hasPullback B.1 (pV@1, f, pVT@1, pP@1)) - (propPi (homTo A.1 (pV@0)) (\(f : homTo A.1 (pV@0)) -> hasPullback A.1 (pV@0, f, pVT@0, pP@0)) - (\(f : homTo A.1 (pV@0)) -> hasPullbackProp A.1 A.2.1 (pV@0, f, pVT@0, pP@0))) - ((f : homTo (p@i).1.1 (pV@i)) -> hasPullback (p@i).1.1 (pV@i, f, pVT@i, pP@i)) - A.2.2.2.2.2.2 B.2.2.2.2.2.2 @ i) - -ucToC0 (C : uc) : C0System = hole + ,pPb@i) + + +-- +-- Definition of a C0-system from a universe category +-- +ucToC0 (C : uc) : CSystem = hole where V : cA C.1 = C.2.2.2.1 VT : cA C.1 = C.2.2.2.2.1 @@ -176,6 +215,7 @@ ucToC0 (C : uc) : C0System = hole D : isPrecategory DD = (DId, DC, homDSet, DIdL, DIdR, DIdC) DC : precategory = (DD, D) + -- ^ Definition of the precategory ft0 (n : nat) (x : ob (suc n)) : ob n = x.1 ft (x : obD) : obD = mkFt ob ft0 x.1 x.2 @@ -187,6 +227,11 @@ ucToC0 (C : uc) : C0System = hole fstar (n : nat) (X : ob (suc n)) (Y : obD) (f : homD Y (n, X.1)) : obD = (suc Y.1, Y.2, cC C.1 (intD Y) (int n X.1) V f X.2) + -- The C-system constructed from the universe category has the definitional equality ft(f*(X)) = Y, + -- but this cannot be required to hold definitionally in the definition of C-systems, so what we need + -- to prove contains transports by reflexivity. + -- To simplify the proofs, the proofs are done without this transport first, and transported to the + -- right types afterwards. q_ (n : nat) (X : ob (suc n)) (Y : obD) (f : homD Y (n, X.1)) : (q : homD (fstar n X Y f) (suc n, X)) * (qSq : Id (homD (fstar n X Y f) (n, X.1)) @@ -257,18 +302,41 @@ ucToC0 (C : uc) : C0System = hole pbD (intD A.1, A.2.1, A.2.2.1, A.2.2.2) ) + sqD0 (n : nat) (X : ob (suc n)) (Y : obD) (f : homD Y (n, X.1)) + : (f_star : ob (suc Y.1)) * (ftf : Id obD (Y.1, ft0 Y.1 f_star) Y) + * (q : homD (suc Y.1, f_star) (suc n, X)) + * (qSq : Id (homD (suc Y.1, f_star) (n, X.1)) + (cC DC (suc Y.1, f_star) Y (n, X.1) (pD (suc Y.1, f_star) Y ftf) f) + (cC DC (suc Y.1, f_star) (suc n, X) (n, X.1) q (pD (suc n, X) (n, X.1) (<_> (n, X.1))))) + * isPullback DC ((n, X.1), (Y, f), ((suc n, X), pD (suc n, X) (n, X.1) (<_> (n, X.1)))) + ((suc Y.1, f_star), pD (suc Y.1, f_star) Y ftf, q, qSq) + = ((fstar n X Y f).2, <_> Y, (q_ n X Y f).1, + transport + ( (qSq : Id (homD (fstar n X Y f) (n, X.1)) + (cC DC (fstar n X Y f) Y (n, X.1) (transRefl (cH DC (fstar n X Y f) Y) (p0 (suc Y.1) (fstar n X Y f).2) @ -i) f) + (cC DC (fstar n X Y f) (suc n, X) (n, X.1) (q_ n X Y f).1 (transRefl (cH DC (suc n, X) (n, X.1)) (p0 (suc n) X) @ -i)) + ) + * isPullback DC ((n, X.1), (Y, f), ((suc n, X), (transRefl (cH DC (suc n, X) (n, X.1)) (p0 (suc n) X) @ -i))) + (fstar n X Y f, (transRefl (cH DC (fstar n X Y f) Y) (p0 (suc Y.1) (fstar n X Y f).2) @ -i), (q_ n X Y f).1, qSq) + ) + ((q_ n X Y f).2.1, (q_ n X Y f).2.2.2)) + + -- Projections of the previous proof to the actual datum of the C system sqD (n : nat) (X : ob (suc n)) (Y : obD) (f : homD Y (n, X.1)) : (f_star : ob (suc Y.1)) * (ftf : Id obD (Y.1, ft0 Y.1 f_star) Y) * (q : homD (suc Y.1, f_star) (suc n, X)) * Id (homD (suc Y.1, f_star) (n, X.1)) (cC DC (suc Y.1, f_star) Y (n, X.1) (pD (suc Y.1, f_star) Y ftf) f) (cC DC (suc Y.1, f_star) (suc n, X) (n, X.1) q (pD (suc n, X) (n, X.1) (<_> (n, X.1)))) - = ((fstar n X Y f).2, <_> Y, (q_ n X Y f).1, - transport - ( Id (homD (fstar n X Y f) (n, X.1)) - (cC DC (fstar n X Y f) Y (n, X.1) (transRefl (cH DC (fstar n X Y f) Y) (p0 (suc Y.1) (fstar n X Y f).2) @ -i) f) - (cC DC (fstar n X Y f) (suc n, X) (n, X.1) (q_ n X Y f).1 (transRefl (cH DC (suc n, X) (n, X.1)) (p0 (suc n) X) @ -i))) - (q_ n X Y f).2.1) + = ((sqD0 n X Y f).1, (sqD0 n X Y f).2.1, (sqD0 n X Y f).2.2.1, (sqD0 n X Y f).2.2.2.1) + + pbSq (sq : (n : nat) * (X : ob (suc n)) * (Y : obD) * (homD Y (n, X.1))) + : isPullback DC ((sq.1, sq.2.1.1), (sq.2.2.1, sq.2.2.2), ((suc sq.1, sq.2.1), pD (suc sq.1, sq.2.1) (sq.1, sq.2.1.1) (<_> (sq.1, sq.2.1.1)))) + (fstar sq.1 sq.2.1 sq.2.2.1 sq.2.2.2 + ,pD (suc sq.2.2.1.1, (fstar sq.1 sq.2.1 sq.2.2.1 sq.2.2.2).2) sq.2.2.1 (sqD sq.1 sq.2.1 sq.2.2.1 sq.2.2.2).2.1 + ,(sqD sq.1 sq.2.1 sq.2.2.1 sq.2.2.2).2.2.1 + ,(sqD sq.1 sq.2.1 sq.2.2.1 sq.2.2.2).2.2.2) + = (sqD0 sq.1 sq.2.1 sq.2.2.1 sq.2.2.2).2.2.2.2 qId (n : nat) (X : ob (suc n)) : (p0 : Id obD (fstar n X (n, X.1) (cId DC (n, X.1))) (suc n, X)) @@ -491,5 +559,5 @@ ucToC0 (C : uc) : C0System = hole (q_ n X Z (cC DC Z Y (n, X.1) g f)).1) (qComp n X Y f Z g) - hole : C0System - = (ob, homD, D, obSet, ft0, pD, sqD, qId, qComp') + hole : CSystem + = (ob, homD, D, (obSet, ft0, pD, sqD, qId, qComp'), pbSq) diff --git a/examples/equiv.ctt b/examples/equiv.ctt index d8c1105..2856e23 100644 --- a/examples/equiv.ctt +++ b/examples/equiv.ctt @@ -12,7 +12,7 @@ isEquiv (A B : U) (f : A -> B) : U = (y : B) -> isContr (fiber A B f y) equiv (A B : U) : U = (f : A -> B) * isEquiv A B f propIsEquiv (A B : U) (f : A -> B) - : prop (isEquiv A B f) = + : prop (isEquiv A B f) = \ (u0 u1:isEquiv A B f) -> \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i equivLemma (A B : U) @@ -34,6 +34,7 @@ retEq (A B:U) (w:equiv A B) (y:B) : Id B (w.1 (invEq A B w y)) y = secEq (A B:U) (w:equiv A B) (x:A) : Id A (invEq A B w (w.1 x)) x = ((w.2 (w.1 x)).2 (x,w.1 x)@i).1 + -- transEquiv (A B:U) (p:Id U A B) : equiv A B = (f,p) where @@ -161,4 +162,3 @@ isoId (A B : U) (f : A -> B) (g : B -> A) idIsEquivGrad (A : U) : isEquiv A A (idfun A) = gradLemma A A (idfun A) (idfun A) (\(a : A) -> a) (\(a : A) -> a) - diff --git a/examples/prelude.ctt b/examples/prelude.ctt index 75f2bce..44a4fac 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -80,7 +80,7 @@ lemCompInv (A:U) (a b c:A) (p:Id A a b) (q:Id A b c) lemInv (A:U) (a b:A) (p:Id A a b) : Id (Id A b b) (compId A b a b (inv A a b p) p) (refl A b) = comp (A) (p @ (-i \/ j)) [(i=0) -> b, (j=1) -> b, (i=1) -> p @ (j \/ k)] - + test0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0) test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1) @@ -107,7 +107,7 @@ lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c) , (k = 1) -> s @ j ] IdPathTest1 (A : U) (a b : A) (p : Id A a b) : - Id (Id A a b) p ( comp ( A) (p @ i) [(i=0) -> a,(i=1) -> b]) = + Id (Id A a b) p ( comp ( A) (p @ i) [(i=0) -> a,(i=1) -> b]) = fill ( A) (p @ i) [(i=0) -> a,(i=1) -> b] @ j idfun (A : U) (a : A) : A = a @@ -162,12 +162,12 @@ propPi (A : U) (B : A -> U) (h : (x : A) -> prop (B x)) (f0 f1 : (x : A) -> B x) : Id ((x : A) -> B x) f0 f1 = \ (x:A) -> (h x (f0 x) (f1 x)) @ i -lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 :A) +lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 :A) (p : Id A a0 a1) (b0 : P a0) (b1 : P a1) : IdP (P (p@i)) b0 b1 = pP (p@i) (comp (P (p@i/\j)) b0 [(i=0) -> <_>b0]) (comp (P (p@i\/-j)) b1 [(i=1) -> <_>b1])@i -- other proof --- lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a :A) : +-- lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a :A) : -- (a1 : A) (p : Id A a a1) (b0 : P a) (b1 : P a1) -> IdP (P (p@i)) b0 b1 = -- J A a (\ (a1 : A) (p : Id A a a1) -> -- (b0 : P a) (b1 : P a1) -> IdP (P (p@i)) b0 b1) @@ -285,4 +285,3 @@ and (A B : U) : U = (_ : A) * B propAnd (A B : U) (pA : prop A) (pB : prop B) : prop (and A B) = propSig A (\(_ : A) -> B) pA (\(_ : A) -> pB) -