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 (<i>(x y : e1@i)->U) (cH A) (cH B))
- * (_ : PathP (<i> (x:e1@i)->(e2@i) x x) (cPath A) (cPath B))
- * (PathP (<i> (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 = (<i>(e@i).1.1, <i>(e@i).1.2, <i>(e@i).2.1, <i>(e@i).2.2.1)
- G (e:catIso3 A B):Path precategory A B = <i> ((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)
- (<i>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
- =<i j>((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))
- (<i>isPrecategory2 (e@i).1 (e@i).2.1 (e@i).2.2.1)
- A.2.2.2 B.2.2.2
- (<j> (G (F e)@j).2.2.2) (<j>(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 (<j>(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 (<i>(e2@-i) x z)
- (cC B (transport e1 x) (transport e1 y) (transport e1 z)
- (transport (<i>(e2@i) x y) f)
- (transport (<i>(e2@i) y z) g))))
- eCatIso30 (A B : precategory) : Path U (catIso3 A B) (catIso30 A B)
- = <i> (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 (<j>e1@-i\/j) x) (transport (<j>e1@-i\/j) y))
- [(i=1)-><_>\(x y:cA A) -> cH B (transport e1 x) (transport e1 y)
- ,(i=0)-><j>\(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 (<j>e1@-i\/j) x) (transport (<j>e1@-i\/j) y))
- e21
- = fill (<_> (x y : e1@-i) -> U)
- (\(x y : e1@-i) -> cH B (transport (<j>e1@-i\/j) x) (transport (<j>e1@-i\/j) y))
- [(i=1)-><_>\(x y:cA A) -> cH B (transport e1 x) (transport e1 y)
- ,(i=0)-><j>\(x y:cA B) -> cH B (transRefl (cA B) x @ j) (transRefl (cA B) y @ j)
- ]
- in
- (e2 : PathP (<j> (x y : e1@j/\-i) -> U) (cH A) e21)
- * (_ : PathP (<j> (x : e1@j/\-i) -> (e2@j/\-i) x x)
- (cPath A)
- (comp (<_> (x:e1@-i)->(e2@-i) x x)
- (\(x : e1@-i) -> transport (<j>(e2@-i\/-j) x x) (transport (<j>(f21@j) x x) (cPath B (transport (<j>e1@-i\/j) x))))
- [(i=1)-><j>\(x:cA A) -> transport (<j>(e2@-j) x x) (transRefl ((f21@0) x x) (cPath B (transport e1 x)) @ j)
- ,(i=0)-><j>\(x:cA B) ->
- transRefl ((e2@1) x x)
- (compPath (cH B x x)
- (transport (<k>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)
- (<j>transport (<k>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 (<j> (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 (<j>(e2@-i\/-j) x z) (transport (<j>(f21@j) x z)
- (cC B (transport (<j>e1@-i\/j) x) (transport (<j>e1@-i\/j) y) (transport (<j>e1@-i\/j) z)
- (transport (<j>(f21@-j) x y) (transport (<j>(e2@-i\/j) x y) f))
- (transport (<j>(f21@-j) y z) (transport (<j>(e2@-i\/j) y z) g)))))
- [(i=1)-><j>\(x y z : cA A) (f : cH A x y) (g : cH A y z) ->
- transport (<j>(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 (<j>(e2@j) x y) f) @ j)
- (transRefl ((f21@0) y z) (transport (<j>(e2@j) y z) g) @ j)) @ j)
- ,(i=0)-><j>\(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 (<k>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 (<k>cH B (transRefl (cA B) x@-k) (transRefl (cA B) y@-k)) (transport (<j>(e2@1) x y) f))
- (transport (<k>cH B (transRefl (cA B) y@-k) (transRefl (cA B) z@-k)) (transport (<j>(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)
- (<j>transport (<k>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 (<k>cH B (transRefl (cA B) x@j\/-k) (transRefl (cA B) y@j\/-k)) (transRefl ((e2@1) x y) f@j))
- (transport (<k>cH B (transRefl (cA B) y@j\/-k) (transRefl (cA B) z@j\/-k)) (transRefl ((e2@1) y z) g@j))))
- (<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
+ = <i> (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))
- (<i>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))
++ (<i>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))
- (<i>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))
++ (<i>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 (<i> (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 (<i>(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 (<i>(e2@i) x y) f)
- (transport (<i>(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)
- = <i> (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 (<j> (e2@i/\j) x x) (cPath A x))
- (\(x:cA A)->transport (<j> (e2@i\/-j) x x) (cPath B (transport e1 x))))
- [(i=0)-><k>Path ((x:cA A)->cH A x x)
- (\(x:cA A)->transRefl (cH A x x) (cPath A x) @ k)
- (\(x:cA A)->transport (<j> (e2@-j) x x) (cPath B (transport e1 x)))
- ,(i=1)-><k>Path ((x:cA A)->(e2@i) x x)
- (\(x:cA A)->transport (<j> (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 (<j> (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 (<j>(e2@i\/-j) x z)
- (cC B (transport e1 x) (transport e1 y) (transport e1 z)
- (transport (<j>(e2@j) x y) f)
- (transport (<j>(e2@j) y z) g))))
- [(i=0)-><k>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 (<j>(e2@-j) x z)
- (cC B (transport e1 x) (transport e1 y) (transport e1 z)
- (transport (<j>(e2@j) x y) f)
- (transport (<j>(e2@j) y z) g)))
- ,(i=1)-><k>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 (<j>(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 (<j>(e2@j) x y) f)
- (transport (<j>(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))))
- (<j>e.1(secEq A B e x@-j))
- (<j>retEq A B e (e.1 x)@-j)
- = <i> comp (<j> 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)-><j><k>e.1 (secEq A B e x@-k\/-j)
- ,(i=1)-><j><k>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 (<i> 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
- = <i> ((e.2 x.1).1.2 @ -i
- ,comp (<_> B' ((e.2 x.1).1.2 @ -i))
- (transport (<j> B' ((e.2 x.1).1.2 @ j/\-i)) x.2)
- [(i=0)-><j>((f (e.2 x.1).1.1).2 (transport (<i> B' ((e.2 x.1).1.2 @ i)) x.2)).1.2 @ j
- ,(i=1)-><j>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
- = <i> (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 (<j> B' (e.1 (secEq A A' e x.1 @ i\/-j))) ((f x.1).1 x.2))).1.1
- [(i=0)-><k>((f (secEq A A' e x.1 @ 0)).2 (transport (<i> B' (lemEquivCoh A A' e x.1@k@i)) ((f x.1).1 x.2))).1.1
- ,(i=1)-><k>compPath (B x.1)
- ((f x.1).2 (transport (<j> 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
- (<k>((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)
- (<i>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)
++ (<i>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)
+ (<i>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)
- (<i>cC X A B A f.1 (cIdL X B A f.2.1 @ i))
++ (cPath X A)
++ (<i>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)
- = <i> (e1 : Path U (cA A) (cA B))
- * (let F(e2:catIso311 A B e1):catIso321 A B e1 = \(x y:cA A)-><i>(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)-><i>\(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)-><i>(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))-><i>\(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)-><i>(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))-><i>\(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
- = <i> (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))
- (<i>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))
- (<i>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)
- (<i>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)
- (<i>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)
- (<i>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) (<i>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) (<i>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
-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
+ --
+ -- Categories
+ --
+
+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)
(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))
- (<i>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))
- (<i>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))
- (<i>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))
- (<i>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))
- (<i>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
- (<i>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))
- (<i>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
- (<i>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
- (<i>(ff x y g.1).1.2@-i) (<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
- (<i> ((ff x y (F.2.1 x y f.1)).2 (f.1,<j>F.2.1 x y f.1)@i).1)
- (<i> ((ff y x (F.2.1 y x f.2.1)).2 (f.2.1,<j>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))
+ (<i>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))
+ (<i>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))
+ (<i>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))
+ (<i>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))
+ (<i>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
+ (<i>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))
+ (<i>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
+ (<i>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
+ (<i>(ff x y g.1).1.2@-i) (<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
+ (<i> ((ff x y (F.2.1 x y f.1)).2 (f.1,<j>F.2.1 x y f.1)@i).1)
+ (<i> ((ff y x (F.2.1 y x f.2.1)).2 (f.2.1,<j>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 (<i>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 (<i> 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)
+ -- = <i> ((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)
--- = (<i>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)
++-- = (<i>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
--- (<i>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>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 (<i>(x y : e1@i)->U) (cH A) (cH B))
- * (_ : IdP (<i> (x:e1@i)->(e2@i) x x) (cId A) (cId B))
- * (IdP (<i> (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 (<i>(x y : e1@i)->U) (cH A) (cH B))
++ * (_ : PathP (<i> (x:e1@i)->(e2@i) x x) (cPath A) (cPath B))
++ * (PathP (<i> (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 = (<i>(e@i).1.1, <i>(e@i).1.2, <i>(e@i).2.1, <i>(e@i).2.2.1)
- G (e:catIso3 A B):Id precategory A B = <i> ((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 = (<i>(e@i).1.1, <i>(e@i).1.2, <i>(e@i).2.1, <i>(e@i).2.2.1)
++ G (e:catIso3 A B):Path precategory A B = <i> ((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)
+ (<i>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
+ =<i j>((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))
+ (<i>isPrecategory2 (e@i).1 (e@i).2.1 (e@i).2.2.1)
+ A.2.2.2 B.2.2.2
+ (<j> (G (F e)@j).2.2.2) (<j>(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 (<j>(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 (<j>(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 (<i>(e2@-i) x z)
+ (cC B (transport e1 x) (transport e1 y) (transport e1 z)
+ (transport (<i>(e2@i) x y) f)
+ (transport (<i>(e2@i) y z) g))))
+
-eCatIso30 (A B : precategory) : Id U (catIso3 A B) (catIso30 A B)
- = <i> (e1 : Id U (cA A) (cA B))
++eCatIso30 (A B : precategory) : Path U (catIso3 A B) (catIso30 A B)
++ = <i> (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 (<j>e1@-i\/j) x) (transport (<j>e1@-i\/j) y))
+ [(i=1)-><_>\(x y:cA A) -> cH B (transport e1 x) (transport e1 y)
+ ,(i=0)-><j>\(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 (<j>e1@-i\/j) x) (transport (<j>e1@-i\/j) y))
+ e21
+ = fill (<_> (x y : e1@-i) -> U)
+ (\(x y : e1@-i) -> cH B (transport (<j>e1@-i\/j) x) (transport (<j>e1@-i\/j) y))
+ [(i=1)-><_>\(x y:cA A) -> cH B (transport e1 x) (transport e1 y)
+ ,(i=0)-><j>\(x y:cA B) -> cH B (transRefl (cA B) x @ j) (transRefl (cA B) y @ j)
+ ]
+ in
- (e2 : IdP (<j> (x y : e1@j/\-i) -> U) (cH A) e21)
- * (_ : IdP (<j> (x : e1@j/\-i) -> (e2@j/\-i) x x)
- (cId A)
++ (e2 : PathP (<j> (x y : e1@j/\-i) -> U) (cH A) e21)
++ * (_ : PathP (<j> (x : e1@j/\-i) -> (e2@j/\-i) x x)
++ (cPath A)
+ (comp (<_> (x:e1@-i)->(e2@-i) x x)
- (\(x : e1@-i) -> transport (<j>(e2@-i\/-j) x x) (transport (<j>(f21@j) x x) (cId B (transport (<j>e1@-i\/j) x))))
- [(i=1)-><j>\(x:cA A) -> transport (<j>(e2@-j) x x) (transRefl ((f21@0) x x) (cId B (transport e1 x)) @ j)
++ (\(x : e1@-i) -> transport (<j>(e2@-i\/-j) x x) (transport (<j>(f21@j) x x) (cPath B (transport (<j>e1@-i\/j) x))))
++ [(i=1)-><j>\(x:cA A) -> transport (<j>(e2@-j) x x) (transRefl ((f21@0) x x) (cPath B (transport e1 x)) @ j)
+ ,(i=0)-><j>\(x:cA B) ->
+ transRefl ((e2@1) x x)
- (compId (cH B x x)
++ (compPath (cH B x x)
+ (transport (<k>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)
+ (<j>transport (<k>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 (<j> (x y z : e1@j/\-i) (f : (e2@j/\-i) x y) (g : (e2@j/\-i) y z) -> (e2@j/\-i) x z)
++ * (PathP (<j> (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 (<j>(e2@-i\/-j) x z) (transport (<j>(f21@j) x z)
+ (cC B (transport (<j>e1@-i\/j) x) (transport (<j>e1@-i\/j) y) (transport (<j>e1@-i\/j) z)
+ (transport (<j>(f21@-j) x y) (transport (<j>(e2@-i\/j) x y) f))
+ (transport (<j>(f21@-j) y z) (transport (<j>(e2@-i\/j) y z) g)))))
+ [(i=1)-><j>\(x y z : cA A) (f : cH A x y) (g : cH A y z) ->
+ transport (<j>(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 (<j>(e2@j) x y) f) @ j)
+ (transRefl ((f21@0) y z) (transport (<j>(e2@j) y z) g) @ j)) @ j)
+ ,(i=0)-><j>\(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 (<k>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 (<k>cH B (transRefl (cA B) x@-k) (transRefl (cA B) y@-k)) (transport (<j>(e2@1) x y) f))
+ (transport (<k>cH B (transRefl (cA B) y@-k) (transRefl (cA B) z@-k)) (transport (<j>(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)
+ (<j>transport (<k>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 (<k>cH B (transRefl (cA B) x@j\/-k) (transRefl (cA B) y@j\/-k)) (transRefl ((e2@1) x y) f@j))
+ (transport (<k>cH B (transRefl (cA B) y@j\/-k) (transRefl (cA B) z@j\/-k)) (transRefl ((e2@1) y z) g@j))))
+ (<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 (<i> (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 (<i> (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 (<i>(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 (<i>(e2@i) x y) f)
+ (transport (<i>(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)
- = <i> (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)
++ = <i> (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 (<j> (e2@i/\j) x x) (cId A x))
- (\(x:cA A)->transport (<j> (e2@i\/-j) x x) (cId B (transport e1 x))))
- [(i=0)-><k>Id ((x:cA A)->cH A x x)
- (\(x:cA A)->transRefl (cH A x x) (cId A x) @ k)
- (\(x:cA A)->transport (<j> (e2@-j) x x) (cId B (transport e1 x)))
- ,(i=1)-><k>Id ((x:cA A)->(e2@i) x x)
- (\(x:cA A)->transport (<j> (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 (<j> (e2@i/\j) x x) (cPath A x))
++ (\(x:cA A)->transport (<j> (e2@i\/-j) x x) (cPath B (transport e1 x))))
++ [(i=0)-><k>Path ((x:cA A)->cH A x x)
++ (\(x:cA A)->transRefl (cH A x x) (cPath A x) @ k)
++ (\(x:cA A)->transport (<j> (e2@-j) x x) (cPath B (transport e1 x)))
++ ,(i=1)-><k>Path ((x:cA A)->(e2@i) x x)
++ (\(x:cA A)->transport (<j> (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 (<j> (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 (<j>(e2@i\/-j) x z)
+ (cC B (transport e1 x) (transport e1 y) (transport e1 z)
+ (transport (<j>(e2@j) x y) f)
+ (transport (<j>(e2@j) y z) g))))
- [(i=0)-><k>Id ((x y z:cA A)->cH A x y->cH A y z->cH A x z)
++ [(i=0)-><k>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 (<j>(e2@-j) x z)
+ (cC B (transport e1 x) (transport e1 y) (transport e1 z)
+ (transport (<j>(e2@j) x y) f)
+ (transport (<j>(e2@j) y z) g)))
- ,(i=1)-><k>Id ((x y z:cA A)->cH A x y->cH A y z->(e2@1) x z)
++ ,(i=1)-><k>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 (<j>(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 (<j>(e2@j) x y) f)
+ (transport (<j>(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))))
+ (<j>e.1(secEq A B e x@-j))
+ (<j>retEq A B e (e.1 x)@-j)
- = <i> comp (<j> Id B (e.1 x) (e.1 (secEq A B e x @ -i /\ -j)))
++ = <i> comp (<j> 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)-><j><k>e.1 (secEq A B e x@-k\/-j)
+ ,(i=1)-><j><k>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 (<i>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 (<i> 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 (<i> 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
+ = <i> ((e.2 x.1).1.2 @ -i
+ ,comp (<_> B' ((e.2 x.1).1.2 @ -i))
+ (transport (<j> B' ((e.2 x.1).1.2 @ j/\-i)) x.2)
+ [(i=0)-><j>((f (e.2 x.1).1.1).2 (transport (<i> B' ((e.2 x.1).1.2 @ i)) x.2)).1.2 @ j
+ ,(i=1)-><j>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
+ = <i> (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 (<j> B' (e.1 (secEq A A' e x.1 @ i\/-j))) ((f x.1).1 x.2))).1.1
+ [(i=0)-><k>((f (secEq A A' e x.1 @ 0)).2 (transport (<i> B' (lemEquivCoh A A' e x.1@k@i)) ((f x.1).1 x.2))).1.1
- ,(i=1)-><k>compId (B x.1)
++ ,(i=1)-><k>compPath (B x.1)
+ ((f x.1).2 (transport (<j> 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
+ (<k>((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)
- -- = <i> ((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)
- -- = (<i>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
- -- (<i>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)
- = <i> (e1 : Id U (cA A) (cA B))
++eCatIso32 (A B : precategory) : Path U (catIso31 A B) (catIso32 A B)
++ = <i> (e1 : Path U (cA A) (cA B))
+ * (let F(e2:catIso311 A B e1):catIso321 A B e1 = \(x y:cA A)-><i>(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)-><i>\(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)-><i>(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))-><i>\(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)-><i>(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))-><i>\(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))
)
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
- (<i> Id U ((e2:catIso321 A B e1)*(_:catIso322 A B e1 e2)*(catIso323 A B e1 e2))
+ (<i> 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))))
)
(<i>eCatIso30 A B@-i)
(<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 (<i> 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 (<i> 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))->
<i>((BB.2@i
- ,lemIdPProp (isCategory A.1)
+ ,lemPathPProp (isCategory A.1)
(isCategory BB.1.1)
(propIsCategory A.1)
(<i> isCategory (BB.2@i))
A.2 BB.1.2 @ i)
,<j> BB.2@i/\j))
-opaque catEquivEqId'
++opaque catEquivEqPath'
+
+ --
+ -- Pullbacks
+ --
-- f'
-- W -----> Z
zero -> \(x : ob zero) -> (zero, x)
suc n -> \(x : ob (suc n)) -> (n, ft0 n x)
--- 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 :
+ --
+ -- 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) -> 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)
* (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 (<i>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 (<i>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 (<i> hasFinal (p@i).1.1) A.2.2.1 B.2.2.1
- = lemIdPProp (hasFinal A.1)
++ pFinal : PathP (<i> 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)
+ (<i>hasFinal (p@i).1.1)
+ A.2.2.1 B.2.2.1
+ opaque pFinal
- pV : IdP (<i> cA (p@i).1.1) A.2.2.2.1 B.2.2.2.1
+ pV : PathP (<i> cA (p@i).1.1) A.2.2.2.1 B.2.2.2.1
= <i> 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)-><k>e.2.1@k]
- pVT : IdP (<i> cA (p@i).1.1) A.2.2.2.2.1 B.2.2.2.2.1
+ pVT : PathP (<i> cA (p@i).1.1) A.2.2.2.2.1 B.2.2.2.2.1
= <i> 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)-><k>e.2.2.1@k]
- pP : IdP (<i> 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 (<i> cH (p@i).1.1 (pVT@i) (pV@i)) A.2.2.2.2.2.1 B.2.2.2.2.2.1
= <i> comp (<k> 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)-><k>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)-><k>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)-><k>e.2.2.2@k]
- pPb : IdP (<i> (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))
+ opaque pV
+ opaque pVT
+ opaque pP
++ pPb : PathP (<i> (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)))
+ (<i>(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 <i> ((p@i).1.1
,(p@i).1.2
- ,lemPathPProp (hasFinal A.1)
- (hasFinal B.1)
- (hasFinalProp A.1 A.2.1)
- (<i>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)))
- (<i>(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
= 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
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)
pbD (intD A.1, A.2.1, A.2.2.1, A.2.2.2)
)
- : (f_star : ob (suc Y.1)) * (ftf : Id obD (Y.1, ft0 Y.1 f_star) Y)
+ sqD0 (n : nat) (X : ob (suc n)) (Y : obD) (f : homD Y (n, X.1))
- * (qSq : Id (homD (suc Y.1, f_star) (n, X.1))
++ : (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))
- (<i> (qSq : Id (homD (fstar n X Y f) (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
++ (<i> (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
- (<i> 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 (<i>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) = <i> (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 (<i>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) = <i> (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)
(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)
projects / cubicaltt.git / commitdiff