categoryData : U = (A : U) * (A -> A -> U)
+-- Propositional data of a precategory
isPrecategory2 (C : categoryData) (id : (x : C.1) -> C.2 x x) (c : (x y z : C.1) -> C.2 x y -> C.2 y z -> C.2 x z) : U
= let A : U = C.1
hom : A -> A -> U = C.2
cIdC (C : precategory) (x y z w : cA C) (f : cH C x y) (g : cH C y z) (h : cH C z w)
: Id (cH C x w) (cC C x z w (cC C x y z f g) h) (cC C x y w f (cC C y z w g h)) = C.2.2.2.2.2.2 x y z w f g h
-catIso3 (A B : precategory) : U = (e1 : Id U (cA A) (cA B))
- * (e2 : IdP (<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))
+--
+-- Isomorphisms
+--
-eCatIso3 (A B : precategory) : Id U (Id precategory A B) (catIso3 A B)
- = isoId (Id precategory A B) (catIso3 A B)
- F G FG GF
- where
- F (e:Id precategory A B):catIso3 A B = (<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)
- (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
- =<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)
- (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))
-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)
- (\(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))
- * (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)
- (\(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)
- (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)
- ,(i=0)-><j>\(x:cA B) ->
- transRefl ((e2@1) x x)
- (compId (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)
- (<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))
- @ 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)
- (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)
- (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
+ = <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))
+ 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))
+ f.2.2.2 g.2.2.2 @ i)
+opaque isoEq
-catIso311 (A B : precategory) (e1:Id U (cA A) (cA B)) : U
- = Id ((x y : cA A)->U) (cH A) (\(x y:cA A)->cH B (transport e1 x) (transport e1 y))
-catIso312 (A B : precategory) (e1:Id U (cA A) (cA B)) (e2:catIso311 A B e1) : U
- = Id ((x:cA A)->cH B (transport e1 x) (transport e1 x))
- (\(x:cA A)->transport (<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))
- (\(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))
- * (e2 : catIso311 A B e1)
- * (_ : catIso312 A B e1 e2)
- * ( catIso313 A B e1 e2)
+invIso (C : precategory) (A B : cA C) (f : iso C A B) : iso C B A = (f.2.1, f.1, f.2.2.2, f.2.2.1)
+idIso (C : precategory) (A : cA C) : iso C A A = (cId C A, cId C A, cIdL C A A (cId C A), cIdL C A A (cId C A))
-eCatIso31 (A B : precategory) : Id U (catIso30 A B) (catIso31 A B)
- = <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)))
- * (_: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)
- ])
- * (comp (<_> U)
- (Id ((x y z:cA A)->cH A x y->cH A y z->(e2@i) x z)
- (\(x y z:cA A)(f:cH A x y)(g:cH A y z)->
- transport (<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)
- (\(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)
- (\(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)
- : Id (Id 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)))
- (((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)
-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'):Id (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
- = <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)
- ((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)
+ (cC X A C A (cC X A B C f.1 g.1) (cC X C B A g.2.1 f.2.1))
+ (cC X A B A f.1 (cC X B C A g.1 (cC X C B A g.2.1 f.2.1)))
+ (cId X A)
+ (cIdC X A B C A f.1 g.1 (cC X C B A g.2.1 f.2.1))
+ (compId (cH X A A)
+ (cC X A B A f.1 (cC X B C A g.1 (cC X C B A g.2.1 f.2.1)))
+ (cC X A B A f.1 (cC X B B A (cC X B C B g.1 g.2.1) f.2.1))
+ (cId X A)
+ (<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)
+ (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)
+ (<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))
+ (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))
+ f.2.2.1)))
+opaque compIsoHelper
-sigEquivLem' (A A':U) (B:A->U) (B':A'->U)
- (e:equiv A A')
- (f:(x:A)->Id U (B x) (B' (e.1 x)))
- : Id U (Sigma A B) (Sigma A' B')
- = transEquivToId (Sigma A B) (Sigma A' B') (sigEquivLem A A' B B' e (\(x:A)->transEquiv' (B' (e.1 x)) (B x) (f x)))
-
-catIso321 (A B : precategory) (e1:Id U (cA A) (cA B)) : U
- = (x y:cA A) -> Id U (cH A x y) (cH B (transport e1 x) (transport e1 y))
-catIso322 (A B : precategory) (e1:Id U (cA A) (cA B)) (e2:catIso321 A B e1) : U
- = (x:cA A) -> Id (cH B (transport e1 x) (transport e1 x))
- (transport (e2 x x) (cId A x))
- (cId B (transport e1 x))
-catIso323 (A B : precategory) (e1:Id U (cA A) (cA B)) (e2:catIso321 A B e1) : U
- = (x y z:cA A)(f:cH A x y)(g:cH A y z)->
- Id (cH B (transport e1 x) (transport e1 z))
- (transport (e2 x z) (cC A x y z f g))
- (cC B (transport e1 x) (transport e1 y) (transport e1 z)
- (transport (e2 x y) f)
- (transport (e2 y z) g))
-catIso32 (A B : precategory) : U = (e1 : Id U (cA A) (cA B))
- * (e2 : catIso321 A B e1)
- * (_ : catIso322 A B e1 e2)
- * ( catIso323 A B e1 e2)
-
-eCatIso32 (A B : precategory) : Id U (catIso31 A B) (catIso32 A B)
- = <i> (e1 : Id 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
- ((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)
- * (_ : Id (cH C A A) (cC C A B A f g) (cId C A))
- * (Id (cH C B B) (cC C B A B g f) (cId C B))
-
-isoEq (C : precategory) (A B : cA C) (f g : iso C A B) (p1 : Id (cH C A B) f.1 g.1) (p2 : Id (cH C B A) f.2.1 g.2.1)
- : Id (iso C A B) f g
- = <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))
- 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))
- f.2.2.2 g.2.2.2 @ i)
-opaque isoEq
-
-invIso (C : precategory) (A B : cA C) (f : iso C A B) : iso C B A = (f.2.1, f.1, f.2.2.2, f.2.2.1)
-idIso (C : precategory) (A : cA C) : iso C A A = (cId C A, cId C A, cIdL C A A (cId C A), cIdL C A A (cId C A))
-
-invIsoEquiv (C : precategory) (A B : cA C) : isEquiv (iso C A B) (iso C B A) (invIso C A B)
- = gradLemma (iso C A B) (iso C B A) (invIso C A B) (invIso C B A) (\(x : iso C B A) -> <_> x) (\(x : iso C A B) -> <_> x)
-
-invIsoEq (C : precategory) (A B : cA C) : Id U (iso C A B) (iso C B A)
- = equivId (iso C A B) (iso C B A) (invIso C A B) (invIsoEquiv C A B)
-
-compIsoHelper (X : precategory) (A B C : cA X) (f : iso X A B) (g : iso X B C)
- : Id (cH X A A) (cC X A C A (cC X A B C f.1 g.1) (cC X C B A g.2.1 f.2.1)) (cId X A)
- = compId (cH X A A)
- (cC X A C A (cC X A B C f.1 g.1) (cC X C B A g.2.1 f.2.1))
- (cC X A B A f.1 (cC X B C A g.1 (cC X C B A g.2.1 f.2.1)))
- (cId X A)
- (cIdC X A B C A f.1 g.1 (cC X C B A g.2.1 f.2.1))
- (compId (cH X A A)
- (cC X A B A f.1 (cC X B C A g.1 (cC X C B A g.2.1 f.2.1)))
- (cC X A B A f.1 (cC X B B A (cC X B C B g.1 g.2.1) f.2.1))
- (cId X A)
- (<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)
- (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)
- (<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))
- (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))
- 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 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
,\(a b c d : hSet) (f : a.1 -> b.1) (g : b.1 -> c.1) (h : c.1 -> d.1) -> <_> \(x : a.1) -> h (g (f x)))
where hSet : U = Sigma U set
--- sip
+--
+-- the structure identity principle
+--
structure (X : precategory) : U
= (P : cA X -> U)
isContrSig (A:U) (B:A-> U) (cA:isContr A) (cB : (x:A) -> isContr (B x)) : isContr (Sigma A B)
= ((cA.1, (cB cA.1).1), \(x:Sigma A B) -> propSig A B (isContrProp A cA) (\(x:A)->isContrProp (B x) (cB x)) (cA.1, (cB cA.1).1) x)
+-- the uncommented definition is a bit slow to typecheck
sip (X : precategory) (isC : isCategory X) (S : structure X) (isS : isStandardStructure X S) : isCategory (sipPrecategory X S)
= undefined
-- = hole
-- hole (A : cA D) : isContr ((B : cA D) * iso D A B) = transport (<i>isContr(eq1 A@-i)) (hole0 A)
opaque sip
+--
+-- Functors
--
functor (A B : precategory) : U
(mapOnPath B A (invEq A B e) (e.1 x) (e.1 y) p)
opaque lem10'
-lemFF (A B : precategory) (F : functor A B) (ff : ffFunctor A B F) (x y : cA A)
- : Id U (iso A x y) (iso B (F.1 x) (F.1 y))
- = hole
- where
- F0 (f : iso A x y) : iso B (F.1 x) (F.1 y)
- = (F.2.1 x y f.1, F.2.1 y x f.2.1
- ,compId (cH B (F.1 x) (F.1 x))
- (cC B (F.1 x) (F.1 y) (F.1 x) (F.2.1 x y f.1) (F.2.1 y x f.2.1))
- (F.2.1 x x (cC A x y x f.1 f.2.1))
- (cId B (F.1 x))
- (<i>F.2.2.2 x y x f.1 f.2.1 @-i)
- (compId (cH B (F.1 x) (F.1 x))
- (F.2.1 x x (cC A x y x f.1 f.2.1))
- (F.2.1 x x (cId A x))
- (cId B (F.1 x))
- (<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))
- (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))
- (<i>F.2.2.2 y x y f.2.1 f.1 @-i)
- (compId (cH B (F.1 y) (F.1 y))
- (F.2.1 y y (cC A y x y f.2.1 f.1))
- (F.2.1 y y (cId A y))
- (cId B (F.1 y))
- (<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))
- (F.2.1 x x (cC A x y x (ff x y g.1).1.1 (ff y x g.2.1).1.1))
- (cC B (F.1 x) (F.1 y) (F.1 x) (F.2.1 x y (ff x y g.1).1.1) (F.2.1 y x (ff y x g.2.1).1.1))
- (F.2.1 x x (cId A x))
- (F.2.2.2 x y x (ff x y g.1).1.1 (ff y x g.2.1).1.1)
- (compId (cH B (F.1 x) (F.1 x))
- (cC B (F.1 x) (F.1 y) (F.1 x) (F.2.1 x y (ff x y g.1).1.1) (F.2.1 y x (ff y x g.2.1).1.1))
- (cC B (F.1 x) (F.1 y) (F.1 x) g.1 g.2.1)
- (F.2.1 x x (cId A x))
- (<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))
- (cC B (F.1 x) (F.1 y) (F.1 x) g.1 g.2.1)
- (cId B (F.1 x))
- (F.2.1 x x (cId A x))
- g.2.2.1
- (<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))
- (F.2.1 y y (cC A y x y (ff y x g.2.1).1.1 (ff x y g.1).1.1))
- (cC B (F.1 y) (F.1 x) (F.1 y) (F.2.1 y x (ff y x g.2.1).1.1) (F.2.1 x y (ff x y g.1).1.1))
- (F.2.1 y y (cId A y))
- (F.2.2.2 y x y (ff y x g.2.1).1.1 (ff x y g.1).1.1)
- (compId (cH B (F.1 y) (F.1 y))
- (cC B (F.1 y) (F.1 x) (F.1 y) (F.2.1 y x (ff y x g.2.1).1.1) (F.2.1 x y (ff x y g.1).1.1))
- (cC B (F.1 y) (F.1 x) (F.1 y) g.2.1 g.1)
- (F.2.1 y y (cId A y))
- (<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))
- (cC B (F.1 y) (F.1 x) (F.1 y) g.2.1 g.1)
- (cId B (F.1 y))
- (F.2.1 y y (cId A y))
- g.2.2.2
- (<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
- = 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
- = 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
-opaque lemFF
+lemFF (A B : precategory) (F : functor A B) (ff : ffFunctor A B F) (x y : cA A)
+ : Id U (iso A x y) (iso B (F.1 x) (F.1 y))
+ = hole
+ where
+ F0 (f : iso A x y) : iso B (F.1 x) (F.1 y)
+ = (F.2.1 x y f.1, F.2.1 y x f.2.1
+ ,compId (cH B (F.1 x) (F.1 x))
+ (cC B (F.1 x) (F.1 y) (F.1 x) (F.2.1 x y f.1) (F.2.1 y x f.2.1))
+ (F.2.1 x x (cC A x y x f.1 f.2.1))
+ (cId B (F.1 x))
+ (<i>F.2.2.2 x y x f.1 f.2.1 @-i)
+ (compId (cH B (F.1 x) (F.1 x))
+ (F.2.1 x x (cC A x y x f.1 f.2.1))
+ (F.2.1 x x (cId A x))
+ (cId B (F.1 x))
+ (<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))
+ (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))
+ (<i>F.2.2.2 y x y f.2.1 f.1 @-i)
+ (compId (cH B (F.1 y) (F.1 y))
+ (F.2.1 y y (cC A y x y f.2.1 f.1))
+ (F.2.1 y y (cId A y))
+ (cId B (F.1 y))
+ (<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))
+ (F.2.1 x x (cC A x y x (ff x y g.1).1.1 (ff y x g.2.1).1.1))
+ (cC B (F.1 x) (F.1 y) (F.1 x) (F.2.1 x y (ff x y g.1).1.1) (F.2.1 y x (ff y x g.2.1).1.1))
+ (F.2.1 x x (cId A x))
+ (F.2.2.2 x y x (ff x y g.1).1.1 (ff y x g.2.1).1.1)
+ (compId (cH B (F.1 x) (F.1 x))
+ (cC B (F.1 x) (F.1 y) (F.1 x) (F.2.1 x y (ff x y g.1).1.1) (F.2.1 y x (ff y x g.2.1).1.1))
+ (cC B (F.1 x) (F.1 y) (F.1 x) g.1 g.2.1)
+ (F.2.1 x x (cId A x))
+ (<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))
+ (cC B (F.1 x) (F.1 y) (F.1 x) g.1 g.2.1)
+ (cId B (F.1 x))
+ (F.2.1 x x (cId A x))
+ g.2.2.1
+ (<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))
+ (F.2.1 y y (cC A y x y (ff y x g.2.1).1.1 (ff x y g.1).1.1))
+ (cC B (F.1 y) (F.1 x) (F.1 y) (F.2.1 y x (ff y x g.2.1).1.1) (F.2.1 x y (ff x y g.1).1.1))
+ (F.2.1 y y (cId A y))
+ (F.2.2.2 y x y (ff y x g.2.1).1.1 (ff x y g.1).1.1)
+ (compId (cH B (F.1 y) (F.1 y))
+ (cC B (F.1 y) (F.1 x) (F.1 y) (F.2.1 y x (ff y x g.2.1).1.1) (F.2.1 x y (ff x y g.1).1.1))
+ (cC B (F.1 y) (F.1 x) (F.1 y) g.2.1 g.1)
+ (F.2.1 y y (cId A y))
+ (<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))
+ (cC B (F.1 y) (F.1 x) (F.1 y) g.2.1 g.1)
+ (cId B (F.1 y))
+ (F.2.1 y y (cId A y))
+ g.2.2.2
+ (<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
+ = 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
+ = 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
+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))
+ = 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
+ = undefined
+-- = transport p hole3
+-- where
+-- hole2 : Id ((y : cA A) * iso B (F.1 y) (F.1 a.1))
+-- (a.1, idIso B (F.1 a.1)) (b.1, compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2))
+-- = isContrProp ((y : cA A) * iso B (F.1 y) (F.1 a.1)) (p2 a.1)
+-- (a.1, idIso B (F.1 a.1)) (b.1, compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2))
+-- opaque hole2
+-- hole3 : Id ((y : cA A) * iso B (F.1 y) x)
+-- (a.1, compIso B (F.1 a.1) (F.1 a.1) x (idIso B (F.1 a.1)) a.2)
+-- (b.1, compIso B (F.1 b.1) (F.1 a.1) x (compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2)) a.2)
+-- = <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)
+-- (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)
+-- (compIso B (F.1 b.1) (F.1 a.1) x (compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2)) a.2)
+-- (compIso B (F.1 b.1) x x b.2 (compIso B x (F.1 a.1) x (invIso B (F.1 a.1) x a.2) a.2))
+-- b.2
+-- (IdCIso B (F.1 b.1) x (F.1 a.1) x b.2 (invIso B (F.1 a.1) x a.2) a.2)
+-- (compId (iso B (F.1 b.1) x)
+-- (compIso B (F.1 b.1) x x b.2 (compIso B x (F.1 a.1) x (invIso B (F.1 a.1) x a.2) a.2))
+-- (compIso B (F.1 b.1) x x b.2 (idIso B x))
+-- b.2
+-- (<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))
+opaque F23
+
+--
+-- Equivalences of precategories
+--
+
+catIsEquiv (A B : precategory) (F : functor A B) : U
+ = (_ : ffFunctor A B F)
+ * ((b : cA B) -> (a : cA A) * iso B (F.1 a) b)
+catEquiv (A B : precategory) : U = (F : functor A B) * catIsEquiv A B F
+catPropIsEquiv (A B : precategory) (isC : isCategory A) (F : functor A B) : prop (catIsEquiv A B F)
+ = propSig (ffFunctor A B F) (\(_ : ffFunctor A B F) -> (b : cA B) -> (a : cA A) * iso B (F.1 a) b)
+ (propFFFunctor A B F)
+ (\(ff : ffFunctor A B F) -> propPi (cA B) (\(b : cA B) -> (a : cA A) * iso B (F.1 a) b)
+ (\(b : cA B) -> F23 A B F (F12 A B isC F ff) b))
+catIdIsEquiv (A : precategory) : catIsEquiv A A (idFunctor A)
+ = (\(a b : cA A) -> idIsEquiv (cH A a b)
+ ,\(b:cA A) -> (b, idIso A b))
+catIdEquiv (A : precategory) : catEquiv A A = (idFunctor A, catIdIsEquiv A)
+
+catIsIso (A B : precategory) (F : functor A B) : U
+ = (_ : ffFunctor A B F) * isEquiv (cA A) (cA B) F.1
+catPropIsIso (A B : precategory) (F : functor A B) : prop (catIsIso A B F)
+ = propSig (ffFunctor A B F) (\(_ : ffFunctor A B F) -> isEquiv (cA A) (cA B) F.1)
+ (propFFFunctor A B F)
+ (\(_ : ffFunctor A B F) -> propIsEquiv (cA A) (cA B) F.1)
+catIso (A B : precategory) : U = (F : functor A B) * catIsIso A B F
+
+--------------------------------------------------------------------------------
+catIso3 (A B : precategory) : U = (e1 : Id U (cA A) (cA B))
+ * (e2 : IdP (<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))
+
+eCatIso3 (A B : precategory) : Id U (Id precategory A B) (catIso3 A B)
+ = isoId (Id precategory A B) (catIso3 A B)
+ F G FG GF
+ where
+ F (e:Id precategory A B):catIso3 A B = (<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)
+ (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
+ =<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)
+ (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)
+ (\(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))
+ * (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)
+ (\(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)
+ (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)
+ ,(i=0)-><j>\(x:cA B) ->
+ transRefl ((e2@1) x x)
+ (compId (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)
+ (<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))
+ @ 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)
+ (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)
+ (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))
+ (\(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))
+ * (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)))
+ * (_: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)
+ ])
+ * (comp (<_> U)
+ (Id ((x y z:cA A)->cH A x y->cH A y z->(e2@i) x z)
+ (\(x y z:cA A)(f:cH A x y)(g:cH A y z)->
+ transport (<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)
+ (\(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)
+ (\(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))))
+ (<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)))
+ (((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) : Id U (iso A x y) (iso B (F.1 x) (F.1 y))
- = lemFF A B F p1 x y
- hole : isContr ((y : cA A) * iso B (F.1 x) (F.1 y))
- = transport (<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
+ = <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
+ = <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)
+ ((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) : Id ((y : cA A) * iso B (F.1 y) x) a b
- = undefined
--- = transport p hole3
--- where
--- hole2 : Id ((y : cA A) * iso B (F.1 y) (F.1 a.1))
--- (a.1, idIso B (F.1 a.1)) (b.1, compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2))
--- = isContrProp ((y : cA A) * iso B (F.1 y) (F.1 a.1)) (p2 a.1)
--- (a.1, idIso B (F.1 a.1)) (b.1, compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2))
--- opaque hole2
--- hole3 : Id ((y : cA A) * iso B (F.1 y) x)
--- (a.1, compIso B (F.1 a.1) (F.1 a.1) x (idIso B (F.1 a.1)) a.2)
--- (b.1, compIso B (F.1 b.1) (F.1 a.1) x (compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2)) a.2)
--- = <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)
--- (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)
--- (compIso B (F.1 b.1) (F.1 a.1) x (compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2)) a.2)
--- (compIso B (F.1 b.1) x x b.2 (compIso B x (F.1 a.1) x (invIso B (F.1 a.1) x a.2) a.2))
--- b.2
--- (IdCIso B (F.1 b.1) x (F.1 a.1) x b.2 (invIso B (F.1 a.1) x a.2) a.2)
--- (compId (iso B (F.1 b.1) x)
--- (compIso B (F.1 b.1) x x b.2 (compIso B x (F.1 a.1) x (invIso B (F.1 a.1) x a.2) a.2))
--- (compIso B (F.1 b.1) x x b.2 (idIso B x))
--- b.2
--- (<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))
-opaque F23
+sigEquivLem' (A A':U) (B:A->U) (B':A'->U)
+ (e:equiv A A')
+ (f:(x:A)->Id U (B x) (B' (e.1 x)))
+ : Id U (Sigma A B) (Sigma A' B')
+ = transEquivToId (Sigma A B) (Sigma A' B') (sigEquivLem A A' B B' e (\(x:A)->transEquiv' (B' (e.1 x)) (B x) (f x)))
-catIsEquiv (A B : precategory) (F : functor A B) : U
- = (_ : ffFunctor A B F)
- * ((b : cA B) -> (a : cA A) * iso B (F.1 a) b)
-catEquiv (A B : precategory) : U = (F : functor A B) * catIsEquiv A B F
-catPropIsEquiv (A B : precategory) (isC : isCategory A) (F : functor A B) : prop (catIsEquiv A B F)
- = propSig (ffFunctor A B F) (\(_ : ffFunctor A B F) -> (b : cA B) -> (a : cA A) * iso B (F.1 a) b)
- (propFFFunctor A B F)
- (\(ff : ffFunctor A B F) -> propPi (cA B) (\(b : cA B) -> (a : cA A) * iso B (F.1 a) b)
- (\(b : cA B) -> F23 A B F (F12 A B isC F ff) b))
-catIdIsEquiv (A : precategory) : catIsEquiv A A (idFunctor A)
- = (\(a b : cA A) -> idIsEquiv (cH A a b)
- ,\(b:cA A) -> (b, idIso A b))
-catIdEquiv (A : precategory) : catEquiv A A = (idFunctor A, catIdIsEquiv A)
+catIso321 (A B : precategory) (e1:Id U (cA A) (cA B)) : U
+ = (x y:cA A) -> Id U (cH A x y) (cH B (transport e1 x) (transport e1 y))
+catIso322 (A B : precategory) (e1:Id U (cA A) (cA B)) (e2:catIso321 A B e1) : U
+ = (x:cA A) -> Id (cH B (transport e1 x) (transport e1 x))
+ (transport (e2 x x) (cId A x))
+ (cId B (transport e1 x))
+catIso323 (A B : precategory) (e1:Id U (cA A) (cA B)) (e2:catIso321 A B e1) : U
+ = (x y z:cA A)(f:cH A x y)(g:cH A y z)->
+ Id (cH B (transport e1 x) (transport e1 z))
+ (transport (e2 x z) (cC A x y z f g))
+ (cC B (transport e1 x) (transport e1 y) (transport e1 z)
+ (transport (e2 x y) f)
+ (transport (e2 y z) g))
+catIso32 (A B : precategory) : U = (e1 : Id U (cA A) (cA B))
+ * (e2 : catIso321 A B e1)
+ * (_ : catIso322 A B e1 e2)
+ * ( catIso323 A B e1 e2)
-catIsIso (A B : precategory) (F : functor A B) : U
- = (_ : ffFunctor A B F) * isEquiv (cA A) (cA B) F.1
-catPropIsIso (A B : precategory) (F : functor A B) : prop (catIsIso A B F)
- = propSig (ffFunctor A B F) (\(_ : ffFunctor A B F) -> isEquiv (cA A) (cA B) F.1)
- (propFFFunctor A B F)
- (\(_ : ffFunctor A B F) -> propIsEquiv (cA A) (cA B) F.1)
-catIso (A B : precategory) : U = (F : functor A B) * catIsIso A B F
+eCatIso32 (A B : precategory) : Id U (catIso31 A B) (catIso32 A B)
+ = <i> (e1 : Id 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
+ ((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))
(cC B (transport e1 x) (transport e1 y) (transport e1 z) (p2 x y f@i) (p2 y z g@i)))
)))
+--------------------------------------------------------------------------------
catIsoIsEquiv (A B : precategory) (F : functor A B) (e : catIsIso A B F) : catIsEquiv A B F
= (e.1,\(b:cA B)->((e.2 b).1.1, eqToIso B (F.1 (e.2 b).1.1) b (<i>(e.2 b).1.2@-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
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))
(<i> isCategory (BB.2@i))
A.2 BB.1.2 @ i)
,<j> BB.2@i/\j))
+opaque catEquivEqId'
+
+--
+-- Pullbacks
+--
-- f'
-- W -----> Z
zero -> \(x : ob zero) -> (zero, x)
suc n -> \(x : ob (suc n)) -> (n, ft0 n x)
+--
+-- C0-Systems
+-- Objects of C0-systems are given by a length indexed family "ob : nat -> U", to avoid equalities on object lengths
+-- The ??? morphisms (p : (x y : A) -> Id A (ft x) y -> hom x y) depend on a path in "Id A (ft x) y" because we can't
+-- enforce a definitional equality in "Id A (ft f*(X)) Y" in this square :
+--
+-- q(f, X)
+-- f*(X) ----> X
+-- | |
+-- | | p_X
+-- | |
+-- Y -------> ft(X)
+-- f
+--
isC0System (ob : nat -> U) (hom : Sigma nat ob -> Sigma nat ob -> U) (isC : isPrecategory (Sigma nat ob, hom)) : U
= let A : U = Sigma nat ob
CD : categoryData = (A,hom)
c0FtH (C : C0System) (Y X : cA (c0C C)) (f : cH (c0C C) Y X) : cH (c0C C) Y (c0Ft C X)
= cC (c0C C) Y X (c0Ft C X) f (c0P C X (c0Ft C X) (<_> c0Ft C X))
-isCSystem2Cospan (C : C0System) (T : c0CanSq C) : cospan (c0C C)
+--
+-- A C0-system is a C-system if all of its canonical squares ("c0CanSq C") are pullback squares
+--
+
+isCSystemCospan (C : C0System) (T : c0CanSq C) : cospan (c0C C)
= let X : cA (c0C C) = (suc T.1, T.2.1) in
(c0Ft C X,
(T.2.2.1, T.2.2.2),
(X, c0P C X (c0Ft C X) (<_>c0Ft C X)))
-isCSystem2CospanCone (C : C0System) (T : c0CanSq C) : cospanCone (c0C C) (isCSystem2Cospan C T)
+isCSystemCospanCone (C : C0System) (T : c0CanSq C) : cospanCone (c0C C) (isCSystemCospan C T)
= (c0Star C T,
c0P C (c0Star C T) T.2.2.1 (c0FtStar C T),
c0Q C T,
c0Square C T)
-isCSystem2Type (C : C0System) (T : c0CanSq C) : U
+isCSystemType (C : C0System) (T : c0CanSq C) : U
= isPullback (c0C C)
- (isCSystem2Cospan C T)
- (isCSystem2CospanCone C T)
-isCSystem2 (C : C0System) : U
- = (T : c0CanSq C) -> isCSystem2Type C T
+ (isCSystemCospan C T)
+ (isCSystemCospanCone C T)
+isCSystem (C : C0System) : U
+ = (T : c0CanSq C) -> isCSystemType C T
+
+isCSystemProp (C : C0System) : prop (isCSystem C)
+ = propPi (c0CanSq C) (\(T : c0CanSq C) -> isCSystemType C T)
+ (\(T : c0CanSq C) -> isPullbackProp (c0C C) (isCSystemCospan C T) (isCSystemCospanCone C T))
-isCSystem2Prop (C : C0System) : prop (isCSystem2 C)
- = propPi (c0CanSq C) (\(T : c0CanSq C) -> isCSystem2Type C T)
- (\(T : c0CanSq C) -> isPullbackProp (c0C C) (isCSystem2Cospan C T) (isCSystem2CospanCone C T))
+CSystem : U = (ob : nat -> U) * (hom : Sigma nat ob -> Sigma nat ob -> U) * (isC : isPrecategory (Sigma nat ob, hom))
+ * (c0 : isC0System ob hom isC) * isCSystem (ob, hom, isC, c0)
--
+-- Definition of a universe category
+--
uc : U
= (C : precategory)
* (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)
ucEquivId (A B : uc) (e : ucEquiv A B) : Id uc A B
= let p : Id ((C:category)*catEquiv A.1 C.1) ((A.1, A.2.1), catIdEquiv A.1) ((B.1, B.2.1), e.1)
= isContrProp ((C:category)*catEquiv A.1 C.1) (catEquivEqId' (A.1, A.2.1)) ((A.1, A.2.1), catIdEquiv A.1) ((B.1, B.2.1), e.1)
+ opaque p
+ pFinal : IdP (<i> hasFinal (p@i).1.1) A.2.2.1 B.2.2.1
+ = lemIdPProp (hasFinal A.1)
+ (hasFinal B.1)
+ (hasFinalProp A.1 A.2.1)
+ (<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
= <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]
(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]
+ opaque pV
+ opaque pVT
+ opaque pP
+ 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))
+ ((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
- ,lemIdPProp (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
- ,lemIdPProp ((f : homTo A.1 (pV@0)) -> hasPullback A.1 (pV@0, f, pVT@0, pP@0))
- ((f : homTo B.1 (pV@1)) -> hasPullback B.1 (pV@1, f, pVT@1, pP@1))
- (propPi (homTo A.1 (pV@0)) (\(f : homTo A.1 (pV@0)) -> hasPullback A.1 (pV@0, f, pVT@0, pP@0))
- (\(f : homTo A.1 (pV@0)) -> hasPullbackProp A.1 A.2.1 (pV@0, f, pVT@0, pP@0)))
- (<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
D : isPrecategory DD
= (DId, DC, homDSet, DIdL, DIdR, DIdC)
DC : precategory = (DD, D)
+ -- ^ Definition of the precategory
ft0 (n : nat) (x : ob (suc n)) : ob n = x.1
ft (x : obD) : obD = mkFt ob ft0 x.1 x.2
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))
pbD (intD A.1, A.2.1, A.2.2.1, A.2.2.2)
)
+ sqD0 (n : nat) (X : ob (suc n)) (Y : obD) (f : homD Y (n, X.1))
+ : (f_star : ob (suc Y.1)) * (ftf : Id obD (Y.1, ft0 Y.1 f_star) Y)
+ * (q : homD (suc Y.1, f_star) (suc n, X))
+ * (qSq : Id (homD (suc Y.1, f_star) (n, X.1))
+ (cC DC (suc Y.1, f_star) Y (n, X.1) (pD (suc Y.1, f_star) Y ftf) f)
+ (cC DC (suc Y.1, f_star) (suc n, X) (n, X.1) q (pD (suc n, X) (n, X.1) (<_> (n, X.1)))))
+ * isPullback DC ((n, X.1), (Y, f), ((suc n, X), pD (suc n, X) (n, X.1) (<_> (n, X.1))))
+ ((suc Y.1, f_star), pD (suc Y.1, f_star) Y ftf, q, qSq)
+ = ((fstar n X Y f).2, <_> Y, (q_ n X Y f).1,
+ transport
+ (<i> (qSq : Id (homD (fstar n X Y f) (n, X.1))
+ (cC DC (fstar n X Y f) Y (n, X.1) (transRefl (cH DC (fstar n X Y f) Y) (p0 (suc Y.1) (fstar n X Y f).2) @ -i) f)
+ (cC DC (fstar n X Y f) (suc n, X) (n, X.1) (q_ n X Y f).1 (transRefl (cH DC (suc n, X) (n, X.1)) (p0 (suc n) X) @ -i))
+ )
+ * isPullback DC ((n, X.1), (Y, f), ((suc n, X), (transRefl (cH DC (suc n, X) (n, X.1)) (p0 (suc n) X) @ -i)))
+ (fstar n X Y f, (transRefl (cH DC (fstar n X Y f) Y) (p0 (suc Y.1) (fstar n X Y f).2) @ -i), (q_ n X Y f).1, qSq)
+ )
+ ((q_ n X Y f).2.1, (q_ n X Y f).2.2.2))
+
+ -- Projections of the previous proof to the actual datum of the C system
sqD (n : nat) (X : ob (suc n)) (Y : obD) (f : homD Y (n, X.1))
: (f_star : ob (suc Y.1)) * (ftf : Id obD (Y.1, ft0 Y.1 f_star) Y)
* (q : homD (suc Y.1, f_star) (suc n, X))
* Id (homD (suc Y.1, f_star) (n, X.1))
(cC DC (suc Y.1, f_star) Y (n, X.1) (pD (suc Y.1, f_star) Y ftf) f)
(cC DC (suc Y.1, f_star) (suc n, X) (n, X.1) q (pD (suc n, X) (n, X.1) (<_> (n, X.1))))
- = ((fstar n X Y f).2, <_> Y, (q_ n X Y f).1,
- transport
- (<i> Id (homD (fstar n X Y f) (n, X.1))
- (cC DC (fstar n X Y f) Y (n, X.1) (transRefl (cH DC (fstar n X Y f) Y) (p0 (suc Y.1) (fstar n X Y f).2) @ -i) f)
- (cC DC (fstar n X Y f) (suc n, X) (n, X.1) (q_ n X Y f).1 (transRefl (cH DC (suc n, X) (n, X.1)) (p0 (suc n) X) @ -i)))
- (q_ n X Y f).2.1)
+ = ((sqD0 n X Y f).1, (sqD0 n X Y f).2.1, (sqD0 n X Y f).2.2.1, (sqD0 n X Y f).2.2.2.1)
+
+ pbSq (sq : (n : nat) * (X : ob (suc n)) * (Y : obD) * (homD Y (n, X.1)))
+ : isPullback DC ((sq.1, sq.2.1.1), (sq.2.2.1, sq.2.2.2), ((suc sq.1, sq.2.1), pD (suc sq.1, sq.2.1) (sq.1, sq.2.1.1) (<_> (sq.1, sq.2.1.1))))
+ (fstar sq.1 sq.2.1 sq.2.2.1 sq.2.2.2
+ ,pD (suc sq.2.2.1.1, (fstar sq.1 sq.2.1 sq.2.2.1 sq.2.2.2).2) sq.2.2.1 (sqD sq.1 sq.2.1 sq.2.2.1 sq.2.2.2).2.1
+ ,(sqD sq.1 sq.2.1 sq.2.2.1 sq.2.2.2).2.2.1
+ ,(sqD sq.1 sq.2.1 sq.2.2.1 sq.2.2.2).2.2.2)
+ = (sqD0 sq.1 sq.2.1 sq.2.2.1 sq.2.2.2).2.2.2.2
qId (n : nat) (X : ob (suc n)) :
(p0 : Id obD (fstar n X (n, X.1) (cId DC (n, X.1))) (suc n, X))
(q_ n X Z (cC DC Z Y (n, X.1) g f)).1)
(qComp n X Y f Z g)
- hole : C0System
- = (ob, homD, D, obSet, ft0, pD, sqD, qId, qComp')
+ hole : CSystem
+ = (ob, homD, D, (obSet, ft0, pD, sqD, qId, qComp'), pbSq)
projects / cubicaltt.git / commitdiff