From: Rafaël Bocquet Date: Fri, 8 Jul 2016 07:58:02 +0000 (+0200) Subject: Merge branch 'csystems' X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=fab3ae660054bcc5e5e66e8a8267dd9969a52be8;p=cubicaltt.git Merge branch 'csystems' --- fab3ae660054bcc5e5e66e8a8267dd9969a52be8 diff --cc Eval.hs index 3626107,9203c90..9780c87 --- a/Eval.hs +++ b/Eval.hs @@@ -828,11 -816,9 +816,9 @@@ instance Convertible Val wher (VApp u v,VApp u' v') -> conv ns u u' && conv ns v v' (VSplit u v,VSplit u' v') -> conv ns u u' && conv ns v v' (VOpaque x _, VOpaque x' _) -> x == x' - (VVar x _, VVar x' _) -> x == x' - (VIdP a b c,VIdP a' b' c') -> conv ns a a' && conv ns b b' && conv ns c c' - (VPath i a,VPath i' a') -> conv ns (a `swap` (i,j)) (a' `swap` (i',j)) + (VVar x _, VVar x' _) -> x == x' + (VPathP a b c,VPathP a' b' c') -> conv ns a a' && conv ns b b' && conv ns c c' + (VPLam i a,VPLam i' a') -> conv ns (a `swap` (i,j)) (a' `swap` (i',j)) - (VPLam i a,p') -> conv ns (a `swap` (i,j)) (p' @@ j) - (p,VPLam i' a') -> conv ns (p @@ j) (a' `swap` (i',j)) (VAppFormula u x,VAppFormula u' x') -> conv ns (u,x) (u',x') (VComp a u ts,VComp a' u' ts') -> conv ns (a,u,ts) (a',u',ts') (VHComp a u ts,VHComp a' u' ts') -> conv ns (a,u,ts) (a',u',ts') @@@ -841,6 -827,20 +827,20 @@@ (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u' (VUnGlueElem u ts,VUnGlueElem u' ts') -> conv ns (u,ts) (u',ts') (VCompU u es,VCompU u' es') -> conv ns (u,es) (u',es') + _ | u == v -> True + (Ter (Lam x a u) e,Ter (Lam x' a' u') e') -> + let v@(VVar n _) = mkVarNice ns x (eval e a) + in conv (n:ns) (eval (upd (x,v) e) u) (eval (upd (x',v) e') u') + (Ter (Lam x a u) e,u') -> + let v@(VVar n _) = mkVarNice ns x (eval e a) + in conv (n:ns) (eval (upd (x,v) e) u) (app u' v) + (u',Ter (Lam x a u) e) -> + let v@(VVar n _) = mkVarNice ns x (eval e a) + in conv (n:ns) (app u' v) (eval (upd (x,v) e) u) + (VPair u v,w) -> conv ns u (fstVal w) && conv ns v (sndVal w) + (w,VPair u v) -> conv ns (fstVal w) u && conv ns (sndVal w) v - (VPath i a,p') -> conv ns (a `swap` (i,j)) (p' @@ j) - (p,VPath i' a') -> conv ns (p @@ j) (a' `swap` (i',j)) ++ (VPLam i a,p') -> conv ns (a `swap` (i,j)) (p' @@ j) ++ (p,VPLam i' a') -> conv ns (p @@ j) (a' `swap` (i',j)) _ -> False instance Convertible Ctxt where diff --cc examples/category.ctt index b1e4d23,7209535..a4e1d73 --- a/examples/category.ctt +++ b/examples/category.ctt @@@ -118,350 -119,101 +119,101 @@@ cA (C : precategory) : U = C.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.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) - : Id (cH C x y) (cC C x y y f (cId C y)) f = C.2.2.2.2.2.1 x y f -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 +cPath (C : precategory) (x : cA C) : cH C x x = C.2.1 x +cPathL (C : precategory) (x y : cA C) (f : cH C x y) + : Path (cH C x y) (cC C x x y (cPath C x) f) f = C.2.2.2.2.1 x y f +cPathR (C : precategory) (x y : cA C) (f : cH C x y) + : Path (cH C x y) (cC C x y y f (cPath C y)) f = C.2.2.2.2.2.1 x y f +cPathC (C : precategory) (x y z w : cA C) (f : cH C x y) (g : cH C y z) (h : cH C z w) + : Path (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 : Path U (cA A) (cA B)) - * (e2 : PathP ((x y : e1@i)->U) (cH A) (cH B)) - * (_ : PathP ( (x:e1@i)->(e2@i) x x) (cPath A) (cPath B)) - * (PathP ( (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) : Path U (Path precategory A B) (catIso3 A B) - = isoPath (Path precategory A B) (catIso3 A B) - F G FG GF - where - F (e:Path 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):Path precategory A B = ((e.1@i, e.2.1@i), e.2.2.1@i, e.2.2.2@i - ,lemPathPProp (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):Path (catIso3 A B) (F (G e)) e=<_>e - GF(e:Path precategory A B):Path (Path precategory A B) (G (F e)) e - =((e@j).1, (e@j).2.1, (e@j).2.2.1 - ,lemPathPSet (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)) ++ * (_ : Path (cH C A A) (cC C A B A f g) (cPath C A)) ++ * (Path (cH C B B) (cC C B A B g f) (cPath C B)) - catIso30 (A B : precategory) : U = (e1 : Path U (cA A) (cA B)) - * (e2 : Path ((x y : cA A)->U) (cH A) (\(x y:cA A)->cH B (transport e1 x) (transport e1 y))) - * (_ : Path ((x:cA A)->cH A x x) - (cPath A) - (\(x : cA A) -> transport ((e2@-j) x x) (cPath B (transport e1 x)))) - * (Path ((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) : Path U (catIso3 A B) (catIso30 A B) - = (e1 : Path 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 : Path ((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 : PathP ( (x y : e1@j/\-i) -> U) (cH A) e21) - * (_ : PathP ( (x : e1@j/\-i) -> (e2@j/\-i) x x) - (cPath A) - (comp (<_> (x:e1@-i)->(e2@-i) x x) - (\(x : e1@-i) -> transport ((e2@-i\/-j) x x) (transport ((f21@j) x x) (cPath B (transport (e1@-i\/j) x)))) - [(i=1)->\(x:cA A) -> transport ((e2@-j) x x) (transRefl ((f21@0) x x) (cPath B (transport e1 x)) @ j) - ,(i=0)->\(x:cA B) -> - transRefl ((e2@1) x x) - (compPath (cH B x x) - (transport (cH B (transRefl (cA B) x@k) (transRefl (cA B) x@k)) - (cPath B (transport (<_> cA B) x))) - (transport (<_>cH B x x) (cPath B x)) - (cPath B x) - (transport (cH B (transRefl (cA B) x@j\/k) (transRefl (cA B) x@j\/k)) - (cPath B (transRefl (cA B) x @ j))) - (transRefl (cH B x x) (cPath B x)) - @ j) @ j - ])) - * (PathP ( (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) - (compPath (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 ++isoEq (C : precategory) (A B : cA C) (f g : iso C A B) (p1 : Path (cH C A B) f.1 g.1) (p2 : Path (cH C B A) f.2.1 g.2.1) ++ : Path (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)) ++ ,lemPathPProp (Path (cH C A A) (cC C A B A (p1@0) (p2@0)) (cPath C A)) ++ (Path (cH C A A) (cC C A B A (p1@1) (p2@1)) (cPath C A)) ++ (cHSet C A A (cC C A B A (p1@0) (p2@0)) (cPath C A)) ++ (Path (cH C A A) (cC C A B A (p1@i) (p2@i)) (cPath 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)) ++ ,lemPathPProp (Path (cH C B B) (cC C B A B (p2@0) (p1@0)) (cPath C B)) ++ (Path (cH C B B) (cC C B A B (p2@1) (p1@1)) (cPath C B)) ++ (cHSet C B B (cC C B A B (p2@0) (p1@0)) (cPath C B)) ++ (Path (cH C B B) (cC C B A B (p2@i) (p1@i)) (cPath C B)) + f.2.2.2 g.2.2.2 @ i) + opaque isoEq - catIso311 (A B : precategory) (e1:Path U (cA A) (cA B)) : U - = Path ((x y : cA A)->U) (cH A) (\(x y:cA A)->cH B (transport e1 x) (transport e1 y)) - catIso312 (A B : precategory) (e1:Path U (cA A) (cA B)) (e2:catIso311 A B e1) : U - = Path ((x:cA A)->cH B (transport e1 x) (transport e1 x)) - (\(x:cA A)->transport ( (e2@i) x x) (cPath A x)) - (\(x : cA A) -> cPath B (transport e1 x)) - catIso313 (A B : precategory) (e1:Path U (cA A) (cA B)) (e2:catIso311 A B e1) : U - = Path ((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 : Path 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)) ++idIso (C : precategory) (A : cA C) : iso C A A = (cPath C A, cPath C A, cPathL C A A (cPath C A), cPathL C A A (cPath C A)) - eCatIso31 (A B : precategory) : Path U (catIso30 A B) (catIso31 A B) - = (e1 : Path U (cA A) (cA B)) - * (e2 : Path ((x y : cA A)->U) (cH A) (\(x y:cA A)->cH B (transport e1 x) (transport e1 y))) - * (_:comp (<_> U) - (Path ((x:cA A)->(e2@i) x x) - (\(x:cA A)->transport ( (e2@i/\j) x x) (cPath A x)) - (\(x:cA A)->transport ( (e2@i\/-j) x x) (cPath B (transport e1 x)))) - [(i=0)->Path ((x:cA A)->cH A x x) - (\(x:cA A)->transRefl (cH A x x) (cPath A x) @ k) - (\(x:cA A)->transport ( (e2@-j) x x) (cPath B (transport e1 x))) - ,(i=1)->Path ((x:cA A)->(e2@i) x x) - (\(x:cA A)->transport ( (e2@j) x x) (cPath A x)) - (\(x:cA A)->transRefl ((e2@1) x x) (cPath B (transport e1 x)) @ k) - ]) - * (comp (<_> U) - (Path ((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)->Path ((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)->Path ((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) - : Path (Path 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 ( Path 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) ++invIsoEq (C : precategory) (A B : cA C) : Path U (iso C A B) (iso C B A) ++ = equivPath (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'):Path (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):Path (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)->compPath (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) ++ : Path (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)) (cPath X A) ++ = compPath (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) ++ (cPath X A) ++ (cPathC X A B C A f.1 g.1 (cC X C B A g.2.1 f.2.1)) ++ (compPath (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) ++ (cPath X A) ++ (cC X A B A f.1 (cPathC X B C B A g.1 g.2.1 f.2.1 @ -i)) ++ (compPath (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 (cPath X B) f.2.1)) ++ (cPath 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)) ++ (compPath (cH X A A) ++ (cC X A B A f.1 (cC X B B A (cPath 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)) ++ (cPath X A) ++ (cC X A B A f.1 (cPathL 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)->Path U (B x) (B' (e.1 x))) - : Path U (Sigma A B) (Sigma A' B') - = transEquivToPath (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:Path U (cA A) (cA B)) : U - = (x y:cA A) -> Path U (cH A x y) (cH B (transport e1 x) (transport e1 y)) - catIso322 (A B : precategory) (e1:Path U (cA A) (cA B)) (e2:catIso321 A B e1) : U - = (x:cA A) -> Path (cH B (transport e1 x) (transport e1 x)) - (transport (e2 x x) (cPath A x)) - (cPath B (transport e1 x)) - catIso323 (A B : precategory) (e1:Path 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)-> - Path (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 : Path U (cA A) (cA B)) - * (e2 : catIso321 A B e1) - * (_ : catIso322 A B e1 e2) - * ( catIso323 A B e1 e2) - - eCatIso32 (A B : precategory) : Path U (catIso31 A B) (catIso32 A B) - = (e1 : Path 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 - transEquivToPath - ((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) - * (_ : Path (cH C A A) (cC C A B A f g) (cPath C A)) - * (Path (cH C B B) (cC C B A B g f) (cPath C B)) - - isoEq (C : precategory) (A B : cA C) (f g : iso C A B) (p1 : Path (cH C A B) f.1 g.1) (p2 : Path (cH C B A) f.2.1 g.2.1) - : Path (iso C A B) f g - = (p1@i,p2@i - ,lemPathPProp (Path (cH C A A) (cC C A B A (p1@0) (p2@0)) (cPath C A)) - (Path (cH C A A) (cC C A B A (p1@1) (p2@1)) (cPath C A)) - (cHSet C A A (cC C A B A (p1@0) (p2@0)) (cPath C A)) - (Path (cH C A A) (cC C A B A (p1@i) (p2@i)) (cPath C A)) - f.2.2.1 g.2.2.1 @ i - ,lemPathPProp (Path (cH C B B) (cC C B A B (p2@0) (p1@0)) (cPath C B)) - (Path (cH C B B) (cC C B A B (p2@1) (p1@1)) (cPath C B)) - (cHSet C B B (cC C B A B (p2@0) (p1@0)) (cPath C B)) - (Path (cH C B B) (cC C B A B (p2@i) (p1@i)) (cPath 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 = (cPath C A, cPath C A, cPathL C A A (cPath C A), cPathL C A A (cPath 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) : Path U (iso C A B) (iso C B A) - = equivPath (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) - : Path (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)) (cPath X A) - = compPath (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))) - (cPath X A) - (cPathC X A B C A f.1 g.1 (cC X C B A g.2.1 f.2.1)) - (compPath (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)) - (cPath X A) - (cC X A B A f.1 (cPathC X B C B A g.1 g.2.1 f.2.1 @ -i)) - (compPath (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 (cPath X B) f.2.1)) - (cPath X A) - (cC X A B A f.1 (cC X B B A (g.2.2.1 @ i) f.2.1)) - (compPath (cH X A A) - (cC X A B A f.1 (cC X B B A (cPath X B) f.2.1)) - (cC X A B A f.1 f.2.1) - (cPath X A) - (cC X A B A f.1 (cPathL 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) -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)) +PathLIso (C : precategory) (A B : cA C) (f : iso C A B) : Path (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 (cPathL C A B f.1) (cPathR C B A f.2.1) +opaque PathLIso +PathRIso (C : precategory) (A B : cA C) (f : iso C A B) : Path (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 (cPathR C A B f.1) (cPathL C B A f.2.1) +opaque PathRIso +PathCIso (X : precategory) (A B C D : cA X) (f : iso X A B) (g : iso X B C) (h : iso X C D) + : Path (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) + (cPathC X A B C D f.1 g.1 h.1) (cPathC X D C B A h.2.1 g.2.1 f.2.1@-i) +opaque PathCIso +PathInvLIso (X : precategory) (A B : cA X) (f : iso X A B) : Path (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 PathInvLIso 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 +eqToIso (C : precategory) (A B : cA C) (p : Path (cA C) A B) : iso C A B + = J (cA C) A (\(B : cA C) -> \(p : Path (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) propIsCategory (C : precategory) : prop (isCategory C) @@@ -704,149 -461,411 +461,411 @@@ lem10' (A B : U) (e : equiv A B) (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) - : Path 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 - ,compPath (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)) - (cPath B (F.1 x)) - (F.2.2.2 x y x f.1 f.2.1 @-i) - (compPath (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 (cPath A x)) - (cPath B (F.1 x)) - (F.2.1 x x (f.2.2.1@i)) - (F.2.2.1 x)) - ,compPath (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)) - (cPath B (F.1 y)) - (F.2.2.2 y x y f.2.1 f.1 @-i) - (compPath (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 (cPath A y)) - (cPath 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) (cPath A x) - (compPath (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 (cPath A x)) - (F.2.2.2 x y x (ff x y g.1).1.1 (ff y x g.2.1).1.1) - (compPath (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 (cPath 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)) - (compPath (cH B (F.1 x) (F.1 x)) - (cC B (F.1 x) (F.1 y) (F.1 x) g.1 g.2.1) - (cPath B (F.1 x)) - (F.2.1 x x (cPath 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) (cPath A y) - (compPath (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 (cPath A y)) - (F.2.2.2 y x y (ff y x g.2.1).1.1 (ff x y g.1).1.1) - (compPath (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 (cPath 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)) - (compPath (cH B (F.1 y) (F.1 y)) - (cC B (F.1 y) (F.1 x) (F.1 y) g.2.1 g.1) - (cPath B (F.1 y)) - (F.2.1 y y (cPath A y)) - g.2.2.2 - (F.2.2.1 y @ -i)))) - ) - FG (g : iso B (F.1 x) (F.1 y)) : Path (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) : Path (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 : Path U (iso A x y) (iso B (F.1 x) (F.1 y)) = isoPath (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)) ++ : Path 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)) ++ ,compPath (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)) ++ (cPath 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)) ++ (compPath (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 (cPath A x)) ++ (cPath 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)) ++ ,compPath (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)) ++ (cPath 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)) ++ (compPath (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 (cPath A y)) ++ (cPath 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)) ++ ,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) (cPath A x) ++ (compPath (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.1 x x (cPath 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)) ++ (compPath (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)) ++ (F.2.1 x x (cPath 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)) ++ (compPath (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)) ++ (cPath B (F.1 x)) ++ (F.2.1 x x (cPath 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)) ++ ,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) (cPath A y) ++ (compPath (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.1 y y (cPath 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)) ++ (compPath (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)) ++ (F.2.1 y y (cPath 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)) ++ (compPath (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)) ++ (cPath B (F.1 y)) ++ (F.2.1 y y (cPath 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 ++ FG (g : iso B (F.1 x) (F.1 y)) : Path (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 ++ GF (f : iso A x y) : Path (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 ++ hole : Path U (iso A x y) (iso B (F.1 x) (F.1 y)) = isoPath (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)) ++ hole2 (y : cA A) : Path 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 ++ (a b : (y : cA A) * iso B (F.1 y) x) : Path ((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)) ++-- hole2 : Path ((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) ++-- hole3 : Path ((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) ++-- p : Path U (Path ((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) ++-- (Path ((y : cA A) * iso B (F.1 y) x) a b) ++-- = (Path ((y : cA A) * iso B (F.1 y) x) ++-- (a.1, PathLIso B (F.1 a.1) x a.2 @ i) ++-- (b.1, compPath (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) ++-- (PathCIso B (F.1 b.1) x (F.1 a.1) x b.2 (invIso B (F.1 a.1) x a.2) a.2) ++-- (compPath (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)) ++-- (compIso B (F.1 b.1) x x b.2 (PathInvLIso B (F.1 a.1) x a.2 @ i)) ++-- (PathRIso 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) ++catPathIsEquiv (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) ++catPathEquiv (A : precategory) : catEquiv A A = (idFunctor A, catPathIsEquiv 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)) ++catIso3 (A B : precategory) : U = (e1 : Path U (cA A) (cA B)) ++ * (e2 : PathP ((x y : e1@i)->U) (cH A) (cH B)) ++ * (_ : PathP ( (x:e1@i)->(e2@i) x x) (cPath A) (cPath B)) ++ * (PathP ( (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) ++eCatIso3 (A B : precategory) : Path U (Path precategory A B) (catIso3 A B) ++ = isoPath (Path 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) ++ F (e:Path 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):Path precategory A B = ((e.1@i, e.2.1@i), e.2.2.1@i, e.2.2.2@i ++ ,lemPathPProp (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 ++ FG(e:catIso3 A B):Path (catIso3 A B) (F (G e)) e=<_>e ++ GF(e:Path precategory A B):Path (Path 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) ++ ,lemPathPSet (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) ++catIso30 (A B : precategory) : U = (e1 : Path U (cA A) (cA B)) ++ * (e2 : Path ((x y : cA A)->U) (cH A) (\(x y:cA A)->cH B (transport e1 x) (transport e1 y))) ++ * (_ : Path ((x:cA A)->cH A x x) ++ (cPath A) ++ (\(x : cA A) -> transport ((e2@-j) x x) (cPath B (transport e1 x)))) ++ * (Path ((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)) ++eCatIso30 (A B : precategory) : Path U (catIso3 A B) (catIso30 A B) ++ = (e1 : Path 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) ++ f21 : Path ((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) ++ (e2 : PathP ( (x y : e1@j/\-i) -> U) (cH A) e21) ++ * (_ : PathP ( (x : e1@j/\-i) -> (e2@j/\-i) x x) ++ (cPath 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) ++ (\(x : e1@-i) -> transport ((e2@-i\/-j) x x) (transport ((f21@j) x x) (cPath B (transport (e1@-i\/j) x)))) ++ [(i=1)->\(x:cA A) -> transport ((e2@-j) x x) (transRefl ((f21@0) x x) (cPath B (transport e1 x)) @ j) + ,(i=0)->\(x:cA B) -> + transRefl ((e2@1) x x) - (compId (cH B x x) ++ (compPath (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) ++ (cPath B (transport (<_> cA B) x))) ++ (transport (<_>cH B x x) (cPath B x)) ++ (cPath 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)) ++ (cPath B (transRefl (cA B) x @ j))) ++ (transRefl (cH B x x) (cPath 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) ++ * (PathP ( (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) ++ (compPath (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)) ++catIso311 (A B : precategory) (e1:Path U (cA A) (cA B)) : U ++ = Path ((x y : cA A)->U) (cH A) (\(x y:cA A)->cH B (transport e1 x) (transport e1 y)) ++catIso312 (A B : precategory) (e1:Path U (cA A) (cA B)) (e2:catIso311 A B e1) : U ++ = Path ((x:cA A)->cH B (transport e1 x) (transport e1 x)) ++ (\(x:cA A)->transport ( (e2@i) x x) (cPath A x)) ++ (\(x : cA A) -> cPath B (transport e1 x)) ++catIso313 (A B : precategory) (e1:Path U (cA A) (cA B)) (e2:catIso311 A B e1) : U ++ = Path ((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)) ++catIso31 (A B : precategory) : U = (e1 : Path 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))) ++eCatIso31 (A B : precategory) : Path U (catIso30 A B) (catIso31 A B) ++ = (e1 : Path U (cA A) (cA B)) ++ * (e2 : Path ((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) ++ (Path ((x:cA A)->(e2@i) x x) ++ (\(x:cA A)->transport ( (e2@i/\j) x x) (cPath A x)) ++ (\(x:cA A)->transport ( (e2@i\/-j) x x) (cPath B (transport e1 x)))) ++ [(i=0)->Path ((x:cA A)->cH A x x) ++ (\(x:cA A)->transRefl (cH A x x) (cPath A x) @ k) ++ (\(x:cA A)->transport ( (e2@-j) x x) (cPath B (transport e1 x))) ++ ,(i=1)->Path ((x:cA A)->(e2@i) x x) ++ (\(x:cA A)->transport ( (e2@j) x x) (cPath A x)) ++ (\(x:cA A)->transRefl ((e2@1) x x) (cPath 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) ++ (Path ((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) ++ [(i=0)->Path ((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) ++ ,(i=1)->Path ((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)))) ++ : Path (Path 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))) ++ = comp ( Path 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) : Path 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 ++ FG (x:Sigma A' B'):Path (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 ++ GF (x:Sigma A B):Path (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) ++ ,(i=1)->compPath (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) : Path ((y : cA A) * iso B (F.1 y) x) a b - = undefined - -- = transport p hole3 - -- where - -- hole2 : Path ((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 : Path ((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 : Path U (Path ((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)) - -- (Path ((y : cA A) * iso B (F.1 y) x) a b) - -- = (Path ((y : cA A) * iso B (F.1 y) x) - -- (a.1, PathLIso B (F.1 a.1) x a.2 @ i) - -- (b.1, compPath (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 - -- (PathCIso B (F.1 b.1) x (F.1 a.1) x b.2 (invIso B (F.1 a.1) x a.2) a.2) - -- (compPath (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 (PathInvLIso B (F.1 a.1) x a.2 @ i)) - -- (PathRIso 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))) - -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 ++ (f:(x:A)->Path U (B x) (B' (e.1 x))) ++ : Path U (Sigma A B) (Sigma A' B') ++ = transEquivToPath (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)) - catPathIsEquiv (A : precategory) : catIsEquiv A A (idFunctor A) - = (\(a b : cA A) -> idIsEquiv (cH A a b) - ,\(b:cA A) -> (b, idIso A b)) - catPathEquiv (A : precategory) : catEquiv A A = (idFunctor A, catPathIsEquiv A) ++catIso321 (A B : precategory) (e1:Path U (cA A) (cA B)) : U ++ = (x y:cA A) -> Path U (cH A x y) (cH B (transport e1 x) (transport e1 y)) ++catIso322 (A B : precategory) (e1:Path U (cA A) (cA B)) (e2:catIso321 A B e1) : U ++ = (x:cA A) -> Path (cH B (transport e1 x) (transport e1 x)) ++ (transport (e2 x x) (cPath A x)) ++ (cPath B (transport e1 x)) ++catIso323 (A B : precategory) (e1:Path 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)) ++ Path (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)) ++catIso32 (A B : precategory) : U = (e1 : Path 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)) ++eCatIso32 (A B : precategory) : Path U (catIso31 A B) (catIso32 A B) ++ = (e1 : Path 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 ++ transEquivToPath + ((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)) @@@ -891,20 -910,20 +910,20 @@@ equivPi (A:U) (B0 B1:A->U) (e:(a:A)->eq ) where F(f:(a:A)->B0 a)(a:A):B1 a= (e a).1 (f a) -eCatIso2 (A B:precategory):Id U (catIso32 A B) (catIso2 A B) - = sigEquivLem' (Id U (cA A) (cA B)) (equiv (cA A) (cA B)) - (\(e1:Id U (cA A) (cA B)) -> (e2:catIso321 A B e1)*(_:catIso322 A B e1 e2)*(catIso323 A B e1 e2)) +eCatIso2 (A B:precategory):Path U (catIso32 A B) (catIso2 A B) + = sigEquivLem' (Path U (cA A) (cA B)) (equiv (cA A) (cA B)) + (\(e1:Path U (cA A) (cA B)) -> (e2:catIso321 A B e1)*(_:catIso322 A B e1 e2)*(catIso323 A B e1 e2)) (\(e1:equiv (cA A) (cA B)) -> (e2:catIso21 A B e1)*(_:catIso22 A B e1 e2)*(catIso23 A B e1 e2)) (corrUniv' (cA A) (cA B)) - (\(e1:Id U (cA A) (cA B)) -> let e1' : equiv (cA A) (cA B) = transEquiv' (cA B) (cA A) e1 - p0 (x:cA A):Id (cA B) (transport e1 x) (e1'.1 x)=lemTransEquiv (cA A) (cA B) e1 x - in + (\(e1:Path U (cA A) (cA B)) -> let e1' : equiv (cA A) (cA B) = transEquiv' (cA B) (cA A) e1 + p0 (x:cA A):Path (cA B) (transport e1 x) (e1'.1 x)=lemTransEquiv (cA A) (cA B) e1 x - in ++ in transport - ( Id U ((e2:catIso321 A B e1)*(_:catIso322 A B e1 e2)*(catIso323 A B e1 e2)) + ( Path U ((e2:catIso321 A B e1)*(_:catIso322 A B e1 e2)*(catIso323 A B e1 e2)) ((e2 : (x y:cA A) -> equiv (cH A x y) (cH B (p0 x@i) (p0 y@i))) - * (_ : (x:cA A) -> Id (cH B (p0 x@i) (p0 x@i)) ((e2 x x).1 (cId A x)) (cId B (p0 x@i))) + * (_ : (x:cA A) -> Path (cH B (p0 x@i) (p0 x@i)) ((e2 x x).1 (cPath A x)) (cPath B (p0 x@i))) * ((x y z:cA A)(f:cH A x y)(g:cH A y z)-> - Id (cH B (p0 x@i) (p0 z@i)) + Path (cH B (p0 x@i) (p0 z@i)) ((e2 x z).1 (cC A x y z f g)) (cC B (p0 x@i) (p0 y@i) (p0 z@i) ((e2 x y).1 f) ((e2 y z).1 g)))) ) @@@ -969,20 -989,26 +989,26 @@@ catIsoEqPath (A B : precategory) : Pat (eCatIso30 A B@-i) (eCatIso3 A B@-i))))) -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 +catEquivEqPath (A B : precategory) (isCA : isCategory A) (isCB : isCategory B) : Path U (catEquiv A B) (Path precategory A B) + = compPath U (catEquiv A B) (catIso A B) (Path precategory A B) (catEquivEqIso A B isCA isCB) (catIsoEqPath A B) ++opaque catEquivEqPath -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)) +catEquivEqPath' (A : category) : isContr ((B : category) * catEquiv A.1 B.1) + = transport ( isContr ((B : category) * catEquivEqPath A.1 B.1 A.2 B.2@-i)) ((A, <_> A.1) - ,\(BB:((B : category) * Id precategory A.1 B.1))-> + ,\(BB:((B : category) * Path precategory A.1 B.1))-> ((BB.2@i - ,lemIdPProp (isCategory A.1) + ,lemPathPProp (isCategory A.1) (isCategory BB.1.1) (propIsCategory A.1) ( isCategory (BB.2@i)) A.2 BB.1.2 @ i) , BB.2@i/\j)) -opaque catEquivEqId' ++opaque catEquivEqPath' + + -- + -- Pullbacks + -- -- f' -- W -----> Z diff --cc examples/csystem.ctt index 05e2819,d4ade76..80ba0a1 --- a/examples/csystem.ctt +++ b/examples/csystem.ctt @@@ -9,6 -9,20 +9,20 @@@ mkFt (ob : nat -> U) (ft0 : (n : nat) - 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 : ++-- The morphisms (p : (x y : A) -> Path A (ft x) y -> hom x y) depend on a path in "Path A (ft x) y" because we can't ++-- enforce a definitional equality in "Path 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) @@@ -106,43 -129,59 +129,59 @@@ uc : * (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) - * (VT : Id (cA B.1) (e.1.1 A.2.2.2.2.1) B.2.2.2.2.1) - * (IdP (cH B.1 (VT@i) (V@i)) (e.1.2.1 A.2.2.2.2.1 A.2.2.2.1 A.2.2.2.2.2.1) B.2.2.2.2.2.1) + * (V : Path (cA B.1) (e.1.1 A.2.2.2.1) B.2.2.2.1) + * (VT : Path (cA B.1) (e.1.1 A.2.2.2.2.1) B.2.2.2.2.1) + * (PathP (cH B.1 (VT@i) (V@i)) (e.1.2.1 A.2.2.2.2.1 A.2.2.2.1 A.2.2.2.2.2.1) B.2.2.2.2.2.1) -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) +ucEquivPath (A B : uc) (e : ucEquiv A B) : Path uc A B + = let p : Path ((C:category)*catEquiv A.1 C.1) ((A.1, A.2.1), catPathEquiv A.1) ((B.1, B.2.1), e.1) + = isContrProp ((C:category)*catEquiv A.1 C.1) (catEquivEqPath' (A.1, A.2.1)) ((A.1, A.2.1), catPathEquiv 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) ++ pFinal : PathP ( hasFinal (p@i).1.1) A.2.2.1 B.2.2.1 ++ = lemPathPProp (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 + pV : PathP ( 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] - pVT : IdP ( cA (p@i).1.1) A.2.2.2.2.1 B.2.2.2.2.1 + pVT : PathP ( cA (p@i).1.1) A.2.2.2.2.1 B.2.2.2.2.1 = comp (<_> cA (p@i).1.1) ((p@i).2.1.1 A.2.2.2.2.1) [(i=0)-><_>A.2.2.2.2.1 ,(i=1)->e.2.2.1@k] - pP : IdP ( cH (p@i).1.1 (pVT@i) (pV@i)) A.2.2.2.2.2.1 B.2.2.2.2.2.1 + pP : PathP ( cH (p@i).1.1 (pVT@i) (pV@i)) A.2.2.2.2.2.1 B.2.2.2.2.2.1 = comp ( cH (p@i).1.1 (fill (<_> cA (p@i).1.1) ((p@i).2.1.1 A.2.2.2.2.1) [(i=0)-><_>A.2.2.2.2.1 ,(i=1)->e.2.2.1@k]@k) (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)) ++ pPb : PathP ( (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 ++ = lemPathPProp ((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 - ,lemPathPProp (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 - ,lemPathPProp ((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 @@@ -174,8 -213,9 +213,9 @@@ = C.1.2.2.2.2.2.2 (intD a) (intD b) (intD c) (intD d) f g h DD : categoryData = (obD, homD) D : isPrecategory DD - = (DId, DC, homDSet, DIdL, DIdR, DIdC) + = (DPath, DC, homDSet, DPathL, DPathR, DPathC) 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,12 -227,17 +227,17 @@@ 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)) + * (qSq : Path (homD (fstar n X Y f) (n, X.1)) (cC DC (fstar n X Y f) Y (n, X.1) (p0 (suc Y.1) (fstar n X Y f).2) f) (cC DC (fstar n X Y f) (suc n, X) (n, X.1) q (p0 (suc n) X))) - * (_ : Id (cH C.1 (intD (fstar n X Y f)) VT) + * (_ : Path (cH C.1 (intD (fstar n X Y f)) VT) (cC C.1 (intD (fstar n X Y f)) (int (suc n) X) VT q (pb n X).1.2.2.1) (pb Y.1 (Y.2, cC C.1 (intD Y) (int n X.1) V f X.2)).1.2.2.1) * isPullback DC ((n, X.1), (Y, f), ((suc n, X), p0 (suc n) X)) (fstar n X Y f, p0 (suc Y.1) (fstar n X Y f).2, q, qSq) @@@ -257,33 -302,56 +302,56 @@@ 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) ++ : (f_star : ob (suc Y.1)) * (ftf : Path 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)) ++ * (qSq : Path (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)) ++ ( (qSq : Path (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) + : (f_star : ob (suc Y.1)) * (ftf : Path 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)) + * Path (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 - ( Path (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)) - * (IdP (cH DC (p0@i) (suc n, X)) (q_ n X (n, X.1) (cId DC (n, X.1))).1 (cId DC (suc n, X))) - = let f_star : obD = fstar n X (n, X.1) (cId DC (n, X.1)) - p1 : Id obD f_star (suc n, X) = (suc n, X.1, cIdL C.1 (int n X.1) V X.2 @ i) + qPath (n : nat) (X : ob (suc n)) : + (p0 : Path obD (fstar n X (n, X.1) (cPath DC (n, X.1))) (suc n, X)) + * (PathP (cH DC (p0@i) (suc n, X)) (q_ n X (n, X.1) (cPath DC (n, X.1))).1 (cPath DC (suc n, X))) + = let f_star : obD = fstar n X (n, X.1) (cPath DC (n, X.1)) + p1 : Path obD f_star (suc n, X) = (suc n, X.1, cPathL C.1 (int n X.1) V X.2 @ i) if_star : cA C.1 = intD f_star - gF : cH C.1 (int n X.1) V = cC C.1 (int n X.1) (int n X.1) V (cId DC (n, X.1)) X.2 + gF : cH C.1 (int n X.1) V = cC C.1 (int n X.1) (int n X.1) V (cPath DC (n, X.1)) X.2 qq : cH C.1 if_star VT = (pb n (X.1, gF)).1.2.2.1 pg : cH C.1 if_star (int n X.1) - = cC C.1 if_star (int n X.1) (int n X.1) (p0 (suc n) f_star.2) (cId DC (n, X.1)) - hole0 : Id (cH C.1 if_star V) + = cC C.1 if_star (int n X.1) (int n X.1) (p0 (suc n) f_star.2) (cPath DC (n, X.1)) + hole0 : Path (cH C.1 if_star V) (cC C.1 if_star (int n X.1) V pg X.2) (cC C.1 if_star VT V qq p) - = compId (cH C.1 if_star V) + = compPath (cH C.1 if_star V) (cC C.1 if_star (int n X.1) V pg X.2) (cC C.1 if_star (int n X.1) V (pb n (X.1, gF)).1.2.1 gF) (cC C.1 if_star VT V qq p) @@@ -491,5 -559,5 +559,5 @@@ (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, qPath, qComp') + hole : CSystem - = (ob, homD, D, (obSet, ft0, pD, sqD, qId, qComp'), pbSq) ++ = (ob, homD, D, (obSet, ft0, pD, sqD, qPath, qComp'), pbSq) diff --cc examples/equiv.ctt index 1e644cf,2856e23..bb5c88e --- a/examples/equiv.ctt +++ b/examples/equiv.ctt @@@ -12,12 -12,11 +12,12 @@@ isEquiv (A B : U) (f : A -> B) : U = ( 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 + \ (u0 u1:isEquiv A B f) -> + \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i equivLemma (A B : U) - : (v w : equiv A B) -> Id (A -> B) v.1 w.1 -> Id (equiv A B) v w + : (v w : equiv A B) -> Path (A -> B) v.1 w.1 -> Path (equiv A B) v w = lemSig (A -> B) (isEquiv A B) (propIsEquiv A B) idIsEquiv (A : U) : isEquiv A A (idfun A) = @@@ -30,13 -29,14 +30,14 @@@ equivPath (T A : U) (f : T -> A) (p : i -- for univalence invEq (A B:U) (w:equiv A B) (y:B) : A = (w.2 y).1.1 -retEq (A B:U) (w:equiv A B) (y:B) : Id B (w.1 (invEq A B w y)) y = +retEq (A B:U) (w:equiv A B) (y:B) : Path B (w.1 (invEq A B w y)) y = (w.2 y).1.2@-i -secEq (A B:U) (w:equiv A B) (x:A) : Id A (invEq A B w (w.1 x)) x = +secEq (A B:U) (w:equiv A B) (x:A) : Path 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) +transEquiv (A B:U) (p:Path U A B) : equiv A B = (f,p) where f (x:A) : B = comp p x [] g (y:B) : A = comp (p@-i) y [] diff --cc examples/prelude.ctt index ef24e35,44a4fac..e4d0dca --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@@ -78,22 -78,22 +78,22 @@@ lemCompInv (A:U) (a b c:A) (p:Path A a , (j=1) -> p @ i ] -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) = +lemInv (A:U) (a b:A) (p:Path A a b) : Path (Path A b b) (compPath 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) +test0 (A : U) (a b : A) (p : Path A a b) : Path A a a = refl A (p @ 0) +test1 (A : U) (a b : A) (p : Path A a b) : Path A b b = refl A (p @ 1) --- compEmpty (A : U) (a b : A) (p : Id A a b) : Id A a b = +-- compEmpty (A : U) (a b : A) (p : Path A a b) : Path A a b = -- comp A (p @ i) [ ] -kan (A : U) (a b c d : A) (p : Id A a b) (q : Id A a c) - (r : Id A b d) : Id A c d = +kan (A : U) (a b c d : A) (p : Path A a b) (q : Path A a c) + (r : Path A b d) : Path A c d = comp (A) (p @ i) [ (i = 0) -> q, (i = 1) -> r ] -lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c) - (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : - Id (Id A b c) q q' = +lemSimpl (A : U) (a b c : A) (p : Path A a b) (q q' : Path A b c) + (s : Path (Path A a c) (compPath A a b c p q) (compPath A a b c p q')) : + Path (Path A b c) q q' = comp ( A) a [ (j = 0) -> comp ( A) (p @ i) [ (k = 0) -> p @ i @@@ -106,8 -106,8 +106,8 @@@ , (k = 0) -> p , (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]) = +PathPathTest1 (A : U) (a b : A) (p : Path A a b) : - Path (Path A a b) p ( comp ( A) (p @ i) [(i=0) -> a,(i=1) -> b]) = ++ Path (Path 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 @@@ -132,50 -132,47 +132,50 @@@ constSquare (A : U) (a : A) (p : Path (j = 0) -> p @ (i \/ - k), (j = 1) -> p @ (i /\ k)] -prop (A : U) : U = (a b : A) -> Id A a b -set (A : U) : U = (a b : A) -> prop (Id A a b) -groupoid (A : U) : U = (a b : A) -> set (Id A a b) +prop (A : U) : U = (a b : A) -> Path A a b +set (A : U) : U = (a b : A) -> prop (Path A a b) +groupoid (A : U) : U = (a b : A) -> set (Path A a b) -propSet (A : U) (h : prop A) (a b : A) (p q : Id A a b) : Id (Id A a b) p q = - comp (A) a [ (i=0) -> h a a - , (i=1) -> h a b - , (j=0) -> h a (p @ i) - , (j=1) -> h a (q @ i)] +-- the collection of all sets +SET : U = (X:U) * set X +propSet (A : U) (h : prop A) : set A = + \(a b : A) (p q : Path A a b) -> + comp (A) a [ (i=0) -> h a a + , (i=1) -> h a b + , (j=0) -> h a (p @ i) + , (j=1) -> h a (q @ i)] propIsProp (A : U) : prop (prop A) = - \(f g : prop A) -> - \(a b : A) -> (propSet A f a b (f a b) (g a b)) @ i + \(f g : prop A) -> \(a b : A) -> + propSet A f a b (f a b) (g a b) @ i --- propIsProp (A : U) (f g : prop A) : Id (prop A) f g = --- \(a b :A) -> (propSet A f a b (f a b) (g a b)) @ i +setIsProp (A : U) : prop (set A) = + \(f g : set A) -> \(a b :A) -> + propIsProp (Path A a b) (f a b) (g a b) @ i -setIsProp (A : U) (f g : set A) : Id (set A) f g = - \(a b :A) -> (propIsProp (Id A a b) (f a b) (g a b)) @ i +PathS (A : U) (P : A -> U) (a0 a1 : A) + (p : Path A a0 a1) (u0 : P a0) (u1 : P a1) : U = + PathP ( P (p @ i)) u0 u1 -IdS (A : U) (P : A -> U) (a0 a1 : A) (p : Id A a0 a1) (u0 : P a0) (u1 : P a1) : U = - IdP ( P (p @ i)) u0 u1 - -lemProp (A : U) (h : A -> prop A) : prop A = \ (a : A) -> h a a +lemProp (A : U) (h : A -> prop A) : prop A = + \(a : A) -> h a a 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 + (f0 f1 : (x : A) -> B x) : Path ((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 = + (p : Path A a0 a1) (b0 : P a0) (b1 : P a1) : PathP (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) +-- (a1 : A) (p : Path A a a1) (b0 : P a) (b1 : P a1) -> PathP (P (p@i)) b0 b1 = +-- J A a (\ (a1 : A) (p : Path A a a1) -> +-- (b0 : P a) (b1 : P a1) -> PathP (P (p@i)) b0 b1) -- rem --- where rem : (b0 b1:P a) -> Id (P a) b0 b1 = pP a +-- where rem : (b0 b1:P a) -> Path (P a) b0 b1 = pP a Sigma (A : U) (B : A -> U) : U = (x : A) * B x