import sigma
import equiv
import nat
+import univalence
lemReflComp (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) (compId A a a b (<_> a) p) p =
<j i> comp (<k> A) (p @ i /\ j) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> <k> p @ k \/ j ]
<j i> comp (<k> A) (p @ i) [(i=0) -> <_> a, (j=1) -> <_> p @ i, (i=1) -> <_> b ]
opaque lemReflComp'
+setPi (A : U) (B : A -> U) (h : (x : A) -> set (B x))
+ (f0 f1 : (x : A) -> B x)
+ (p1 p2 : Id ((x : A) -> B x) f0 f1)
+ : Id (Id ((x : A) -> B x) f0 f1) p1 p2
+ = <i j> \(x : A) -> (h x (f0 x) (f1 x) (<i> (p1@i) x) (<i> (p2@i) x)) @ i @ j
+opaque setPi
+
lemIdPProp (A B : U) (AProp : prop A) (p : Id U A B) : (x : A) -> (y : B) -> IdP p x y
= J U A (\(B : U) -> \(p : Id U A B) -> (x : A) -> (y : B) -> IdP p x y) AProp B p
opaque lemIdPProp
+lemIdPSet (A B : U) (ASet : set A) (p : Id U A B) : (x : A) (y : B) (s t : IdP p x y) -> Id (IdP p x y) s t
+ = J U A (\(B : U) -> \(p : Id U A B) -> (x : A) (y : B) (s t : IdP p x y) -> Id (IdP p x y) s t) ASet B p
+opaque lemIdPSet
+
+lemIdPSet2 (A B : U) (ASet : set A) (p1 : Id U A B)
+ : (p2 : Id U A B) -> (p : Id (Id U A B) p1 p2) ->
+ (x : A) -> (y : B) -> (s : IdP p1 x y) -> (t : IdP p2 x y) -> IdP (<i> (IdP (p @ i) x y)) s t
+ = J (Id U A B) p1 (\(p2 : Id U A B) -> \(p : Id (Id U A B) p1 p2) -> (x : A) -> (y : B) -> (s : IdP p1 x y) -> (t : IdP p2 x y) -> IdP (<i> (IdP (p @ i) x y)) s t)
+ (lemIdPSet A B ASet p1)
+opaque lemIdPSet2
+
substIdP (A B : U) (p : Id U A B) (x : A) (y : B) (q : Id B (transport p x) y) : IdP p x y
= transport (<i> IdP p x (q@i)) hole
where
isPrecategory (C : categoryData) : U =
let A : U = C.1
hom : A -> A -> U = C.2
- in (homSet : (x y : A) -> set (hom x y))
- * (id : (x : A) -> hom x x) * (c : (x y z : A) -> hom x y -> hom y z -> hom x z)
+ in (id : (x : A) -> hom x x) * (c : (x y z : A) -> hom x y -> hom y z -> hom x z)
+ * (homSet : (x y : A) -> set (hom x y))
* (cIdL : (x y : A) -> (f : hom x y) -> Id (hom x y) (c x x y (id x) f) f)
* (cIdR : (x y : A) -> (f : hom x y) -> Id (hom x y) (c x y y f (id y)) f)
* ( (x y z w : A) -> (f : hom x y) -> (g : hom y z) -> (h : hom z w) -> Id (hom x w) (c x z w (c x y z f g) h) (c x y w f (c y z w g h)))
cA (C : precategory) : U = C.1.1
cH (C : precategory) (a b : cA C) : U = C.1.2 a b
-cHSet (C : precategory) (a b : cA C) : set (cH C a b) = C.2.1 a b
-cC (C : precategory) (x y z : cA C) (f : cH C x y) (g : cH C y z) : cH C x z = C.2.2.2.1 x y z f g
-cId (C : precategory) (x : cA C) : cH C x x = C.2.2.1 x
+cHSet (C : precategory) (a b : cA C) : set (cH C a b) = C.2.2.2.1 a b
+cC (C : precategory) (x y z : cA C) (f : cH C x y) (g : cH C y z) : cH C x z = C.2.2.1 x y z f g
+cId (C : precategory) (x : cA C) : cH C x x = C.2.1 x
cIdL (C : precategory) (x y : cA C) (f : cH C x y)
: Id (cH C x y) (cC C x x y (cId C x) f) f = C.2.2.2.2.1 x y f
cIdR (C : precategory) (x y : cA C) (f : cH C x y)
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))
+
+-- catIso2 (A B : precategory) : U = (e1 : equiv (cA A) (cA B))
+-- * (e2 : (x y : cA A) -> equiv (cH A x y) (cH B (e1.1 x) (e1.1 y)))
+-- * (_ : (x : cA A) -> Id (cH B (e1.1 x) (e1.1 x)) ((e2 x x).1 (cId A x)) (cId B (e1.1 x)))
+-- * ((x y z : cA A) -> (f : cH A x y) -> (g : cH A y z) ->
+-- Id (cH B (e1.1 x) (e1.1 z))
+-- ((e2 x z).1 (cC A x y z f g))
+-- (cC B (e1.1 x) (e1.1 y) (e1.1 z) ((e2 x y).1 f) ((e2 y z).1 g)))
+
+catIso30 (A B : precategory) : U = (e1 : Id U (cA A) (cA B))
+ * (e2 : Id ((x y : cA A)->U) (cH A) (\(x y:cA A)->cH B (transport e1 x) (transport e1 y)))
+ * (_ : Id ((x:cA A)->cH A x x)
+ (cId A)
+ (\(x : cA A) -> transport (<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))))
+
+catIso31 (A B : precategory) : U = (e1 : Id U (cA A) (cA B))
+ * (e2 : Id ((x y : cA A)->U) (cH A) (\(x y:cA A)->cH B (transport e1 x) (transport e1 y)))
+ * (_ : Id ((x:cA A)->cH A x x)
+ (cId A)
+ (\(x : cA A) -> transport (<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))))
+
+
+eCatIso3 (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
+ ])))
+
--
iso (C : precategory) (A B : cA C) : U
* (_ : Id (cH C A A) (cC C A B A f g) (cId C A))
* (Id (cH C B B) (cC C B A B g f) (cId C B))
-isoId (C : precategory) (A : cA C) : iso C A A = (cId C A, cId C A, cIdL C A A (cId C A), cIdL C A A (cId C A))
+isoEq (C : precategory) (A B : cA C) (f g : iso C A B) (p1 : Id (cH C A B) f.1 g.1) (p2 : Id (cH C B A) f.2.1 g.2.1)
+ : Id (iso C A B) f g
+ = <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))
+
+IdLIso (C : precategory) (A B : cA C) (f : iso C A B) : Id (iso C A B) (compIso C A A B (idIso C A) f) f
+ = isoEq C A B (compIso C A A B (idIso C A) f) f (cIdL C A B f.1) (cIdR C B A f.2.1)
+opaque IdLIso
+IdRIso (C : precategory) (A B : cA C) (f : iso C A B) : Id (iso C A B) (compIso C A B B f (idIso C B)) f
+ = isoEq C A B (compIso C A B B f (idIso C B)) f (cIdR C A B f.1) (cIdL C B A f.2.1)
+opaque IdRIso
+IdCIso (X : precategory) (A B C D : cA X) (f : iso X A B) (g : iso X B C) (h : iso X C D)
+ : Id (iso X A D) (compIso X A C D (compIso X A B C f g) h) (compIso X A B D f (compIso X B C D g h))
+ = isoEq X A D (compIso X A C D (compIso X A B C f g) h) (compIso X A B D f (compIso X B C D g h))
+ (cIdC X A B C D f.1 g.1 h.1) (<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)
+ = isoEq X B B (compIso X B A B (invIso X A B f) f) (idIso X B) f.2.2.2 f.2.2.2
+opaque IdInvLIso
+
+opaque compIso
+
eqToIso (C : precategory) (A B : cA C) (p : Id (cA C) A B) : iso C A B
- = J (cA C) A (\(B : cA C) -> \(p : Id (cA C) A B) -> iso C A B) (isoId C A) B p
+ = J (cA C) A (\(B : cA C) -> \(p : Id (cA C) A B) -> iso C A B) (idIso C A) B p
+
isCategory (C : precategory) : U = (A : cA C) -> isContr ((B : cA C) * iso C A B)
-lemIsCategory (C : precategory) (isC : isCategory C) (A B : cA C) (e : iso C A B) : Id (cA C) A B
- = <i> (isContrProp ((B : cA C) * iso C A B) (isC A) (A, isoId C A) (B, e) @ i).1
+
+lemIsCategory (C : precategory) (isC : isCategory C) (A B : cA C) (e : iso C A B) : Id ((B : cA C) * iso C A B) (A, idIso C A) (B, e)
+ = <i> (isContrProp ((B : cA C) * iso C A B) (isC A) (A, idIso C A) (B, e) @ i)
+
+lemIsCategory2 (C : precategory) (isC : isCategory C) (A B : cA C) : isEquiv (Id (cA C) A B) (iso C A B) (eqToIso C A B)
+ = equivFunFib (cA C) (Id (cA C) A) (iso C A) (eqToIso C A) (lemSinglContr (cA C) A) (isC A) B
+
+lemIsCategory3 (C : precategory) (isC : isCategory C) (A B : cA C) : Id U (Id (cA C) A B) (iso C A B)
+ = equivId (Id (cA C) A B) (iso C A B) (eqToIso C A B) (lemIsCategory2 C isC A B)
+
+--
+
+-- setCat : precategory
+-- = ((hSet, \(a b : hSet) -> a.1 -> b.1)
+-- ,\(a : hSet) (x : a.1) -> x
+-- ,\(a b c : hSet) (f : a.1 -> b.1) (g : b.1 -> c.1) (x : a.1) -> g (f x)
+-- ,\(a b : hSet) -> setPi a.1 (\(_ : a.1) -> b.1) (\(_ : a.1) -> b.2)
+-- ,\(a b : hSet) (f : a.1 -> b.1) -> <_> \(x : a.1) -> f x
+-- ,\(a b : hSet) (f : a.1 -> b.1) -> <_> \(x : a.1) -> f x
+-- ,\(a b c d : hSet) (f : a.1 -> b.1) (g : b.1 -> c.1) (h : c.1 -> d.1) -> <_> \(x : a.1) -> h (g (f x)))
+-- where hSet : U = Sigma U set
+
+-- -- setIsCat : isCategory setCat
+-- -- = \(A:Sigma U set) ->
+-- -- ((A,idIso setCat A),
+-- -- \(B:(B1:Sigma U set)*iso setCat A B1)->
+-- -- let p : Id U A.1 B.1.1 = <i>isoId A.1 B.1.1 B.2.1 B.2.2.1 (\(x : B.1.1) -> <j>(B.2.2.2.2@j)x) (\(x:A.1)-><j>(B.2.2.2.1@j)x) @ i
+-- -- q : IdP (<i>set(p@i)) A.2 B.1.2 = undefined
+-- -- r : Id (iso setCat A A) (transport (<i>iso setCat A (p@-i,q@-i)) B.2) (idIso setCat A)
+-- -- = <i> (?
+-- -- ,?
+-- -- ,?
+-- -- ,?)
+-- -- in (<i> ((p@i,q@i)
+-- -- ,substIdP (iso setCat A B.1) (iso setCat A A) (<i>iso setCat A (p@-i,q@-i))
+-- -- B.2 (idIso setCat A) r @-i)))
+
+-- -- sip
+
+-- structure (X : precategory) : U
+-- = (P : cA X -> U)
+-- * (H : (x y : cA X) -> (a : P x) -> (b : P y) -> (f : cH X x y) -> U)
+-- * (propH : (x y : cA X) -> (a : P x) -> (b : P y) -> (f : cH X x y) -> prop (H x y a b f))
+-- * (Hid : (x : cA X) -> (a : P x) -> H x x a a (cId X x))
+-- * ((x y z : cA X) -> (a : P x) -> (b : P y) -> (c : P z) ->
+-- (f : cH X x y) -> (g : cH X y z) ->
+-- H x y a b f -> H y z b c g -> H x z a c (cC X x y z f g))
+
+-- sP (X : precategory) (S : structure X) : cA X -> U = S.1
+-- sH (X : precategory) (S : structure X) : (x y : cA X) -> (a : sP X S x) -> (b : sP X S y) -> (f : cH X x y) -> U = S.2.1
+-- sHProp (X : precategory) (S : structure X)
+-- : (x y : cA X) -> (a : sP X S x) -> (b : sP X S y) -> (f : cH X x y) -> prop (sH X S x y a b f) = S.2.2.1
+-- sHId (X : precategory) (S : structure X) : (x : cA X) -> (a : sP X S x) -> sH X S x x a a (cId X x) = S.2.2.2.1
+-- sHComp (X : precategory) (S : structure X)
+-- : (x y z : cA X) -> (a : sP X S x) -> (b : sP X S y) -> (c : sP X S z) ->
+-- (f : cH X x y) -> (g : cH X y z) ->
+-- sH X S x y a b f -> sH X S y z b c g -> sH X S x z a c (cC X x y z f g)
+-- = S.2.2.2.2
+
+-- isStandardStructure (X : precategory) (S : structure X) : U
+-- = (x : cA X) -> (a b : sP X S x) ->
+-- sH X S x x a b (cId X x) -> sH X S x x b a (cId X x) ->
+-- Id (sP X S x) a b
+
+-- sipPrecategory (C : precategory) (S : structure C) : precategory = ((ob, hom), (id, cmp, homSet, idL, idR, idC))
+-- where
+-- ob : U = Sigma (cA C) (sP C S)
+-- hom (X Y : ob) : U = (f : cH C X.1 Y.1) * sH C S X.1 Y.1 X.2 Y.2 f
+-- homSet (X Y : ob) : set (hom X Y)
+-- = setSig (cH C X.1 Y.1) (sH C S X.1 Y.1 X.2 Y.2)
+-- (cHSet C X.1 Y.1) (\(f : cH C X.1 Y.1) -> propSet (sH C S X.1 Y.1 X.2 Y.2 f) (sHProp C S X.1 Y.1 X.2 Y.2 f))
+-- id (X : ob) : hom X X = (cId C X.1, sHId C S X.1 X.2)
+-- cmp (x y z : ob) (f : hom x y) (g : hom y z) : hom x z
+-- = (cC C x.1 y.1 z.1 f.1 g.1, sHComp C S x.1 y.1 z.1 x.2 y.2 z.2 f.1 g.1 f.2 g.2)
+-- idL (x y : ob) (f : hom x y) : Id (hom x y) (cmp x x y (id x) f) f
+-- = <i> (cIdL C x.1 y.1 f.1 @ i
+-- ,lemIdPProp (sH C S x.1 y.1 x.2 y.2 (cmp x x y (id x) f).1)
+-- (sH C S x.1 y.1 x.2 y.2 f.1)
+-- (sHProp C S x.1 y.1 x.2 y.2 (cmp x x y (id x) f).1)
+-- (<i>sH C S x.1 y.1 x.2 y.2 (cIdL C x.1 y.1 f.1 @ i))
+-- (cmp x x y (id x) f).2 f.2 @ i)
+-- idR (x y : ob) (f : hom x y) : Id (hom x y) (cmp x y y f (id y)) f
+-- = <i> (cIdR C x.1 y.1 f.1 @ i
+-- ,lemIdPProp (sH C S x.1 y.1 x.2 y.2 (cmp x y y f (id y)).1)
+-- (sH C S x.1 y.1 x.2 y.2 f.1)
+-- (sHProp C S x.1 y.1 x.2 y.2 (cmp x y y f (id y)).1)
+-- (<i>sH C S x.1 y.1 x.2 y.2 (cIdR C x.1 y.1 f.1 @ i))
+-- (cmp x y y f (id y)).2 f.2 @ i)
+-- idC (x y z w : ob) (f : hom x y) (g : hom y z) (h : hom z w) : Id (hom x w) (cmp x z w (cmp x y z f g) h) (cmp x y w f (cmp y z w g h))
+-- = <i> (cIdC C x.1 y.1 z.1 w.1 f.1 g.1 h.1 @ i
+-- ,lemIdPProp (sH C S x.1 w.1 x.2 w.2 (cmp x z w (cmp x y z f g) h).1)
+-- (sH C S x.1 w.1 x.2 w.2 (cmp x y w f (cmp y z w g h)).1)
+-- (sHProp C S x.1 w.1 x.2 w.2 (cmp x z w (cmp x y z f g) h).1)
+-- (<i>sH C S x.1 w.1 x.2 w.2 (cIdC C x.1y.1 z.1 w.1 f.1 g.1 h.1 @ i))
+-- (cmp x z w (cmp x y z f g) h).2 (cmp x y w f (cmp y z w g h)).2 @ i)
+
+-- isContrProp (A : U) (p : isContr A) (x y : A) : Id A x y = compId A x p.1 y (<i> p.2 x @ -i) (p.2 y)
+-- isContrSig (A:U) (B:A-> U) (cA:isContr A) (cB : (x:A) -> isContr (B x)) : isContr (Sigma A B)
+-- = ((cA.1, (cB cA.1).1), \(x:Sigma A B) -> propSig A B (isContrProp A cA) (\(x:A)->isContrProp (B x) (cB x)) (cA.1, (cB cA.1).1) x)
+
+-- sip (X : precategory) (isC : isCategory X) (S : structure X) (isS : isStandardStructure X S) : isCategory (sipPrecategory X S)
+-- = undefined
+-- -- = hole
+-- -- where
+-- -- D : precategory = sipPrecategory X S
+-- -- eq1 (A : cA D)
+-- -- : Id U ((B : cA D) * iso D A B)
+-- -- ((C : (B1 : cA X) * ( iso X A.1 B1))
+-- -- * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1)
+-- -- = isoId
+-- -- ((B : cA D) * iso D A B)
+-- -- ((C : (B1 : cA X) * ( iso X A.1 B1))
+-- -- * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1)
+-- -- F G FG GF
+-- -- where
+-- -- F (C : (B : cA D) * iso D A B)
+-- -- : ((C : (B1 : cA X) * ( iso X A.1 B1))
+-- -- * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1)
+-- -- = ((C.1.1, C.2.1.1, C.2.2.1.1, <i>(C.2.2.2.1@i).1, <i>(C.2.2.2.2@i).1),
+-- -- C.1.2, C.2.1.2, C.2.2.1.2)
+-- -- G (C : ((C : (B1 : cA X) * ( iso X A.1 B1))
+-- -- * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1))
+-- -- : (B : cA D) * iso D A B
+-- -- = ((C.1.1, C.2.1), (C.1.2.1, C.2.2.1), (C.1.2.2.1, C.2.2.2)
+-- -- , <i> (C.1.2.2.2.1 @ i
+-- -- ,lemIdPProp (sH X S A.1 A.1 A.2 A.2 (cC X A.1 C.1.1 A.1 C.1.2.1 C.1.2.2.1))
+-- -- (sH X S A.1 A.1 A.2 A.2 (cId X A.1))
+-- -- (sHProp X S A.1 A.1 A.2 A.2 (cC X A.1 C.1.1 A.1 C.1.2.1 C.1.2.2.1))
+-- -- (<i>sH X S A.1 A.1 A.2 A.2 (C.1.2.2.2.1 @ i))
+-- -- (sHComp X S A.1 C.1.1 A.1 A.2 C.2.1 A.2 C.1.2.1 C.1.2.2.1 C.2.2.1 C.2.2.2)
+-- -- (sHId X S A.1 A.2) @ i)
+-- -- , <i> (C.1.2.2.2.2 @ i
+-- -- ,lemIdPProp (sH X S C.1.1 C.1.1 C.2.1 C.2.1 (cC X C.1.1 A.1 C.1.1 C.1.2.2.1 C.1.2.1))
+-- -- (sH X S C.1.1 C.1.1 C.2.1 C.2.1 (cId X C.1.1))
+-- -- (sHProp X S C.1.1 C.1.1 C.2.1 C.2.1 (cC X C.1.1 A.1 C.1.1 C.1.2.2.1 C.1.2.1))
+-- -- (<i>sH X S C.1.1 C.1.1 C.2.1 C.2.1 (C.1.2.2.2.2 @ i))
+-- -- (sHComp X S C.1.1 A.1 C.1.1 C.2.1 A.2 C.2.1 C.1.2.2.1 C.1.2.1 C.2.2.2 C.2.2.1)
+-- -- (sHId X S C.1.1 C.2.1) @ i))
+-- -- FG (C : ((C : (B1 : cA X) * ( iso X A.1 B1))
+-- -- * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1))
+-- -- : Id ((C : (B1 : cA X) * ( iso X A.1 B1))
+-- -- * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1)
+-- -- (F (G C)) C
+-- -- = <_> C
+-- -- GF (C : (B : cA D) * iso D A B) : Id ((B : cA D) * iso D A B) (G (F C)) C
+-- -- = <i> (C.1, C.2.1, C.2.2.1
+-- -- , <j> ((C.2.2.2.1 @ j).1
+-- -- ,lemIdPSet (sH X S A.1 A.1 A.2 A.2 (cC X A.1 C.1.1 A.1 C.2.1.1 C.2.2.1.1))
+-- -- (sH X S A.1 A.1 A.2 A.2 (cId X A.1))
+-- -- (propSet (sH X S A.1 A.1 A.2 A.2 (cC X A.1 C.1.1 A.1 C.2.1.1 C.2.2.1.1))
+-- -- (sHProp X S A.1 A.1 A.2 A.2 (cC X A.1 C.1.1 A.1 C.2.1.1 C.2.2.1.1)))
+-- -- (<j>sH X S A.1 A.1 A.2 A.2 (C.2.2.2.1 @ j).1)
+-- -- (sHComp X S A.1 C.1.1 A.1 A.2 C.1.2 A.2 C.2.1.1 C.2.2.1.1 C.2.1.2 C.2.2.1.2)
+-- -- (sHId X S A.1 A.2)
+-- -- (<j>((G (F C)).2.2.2.1 @ j).2)
+-- -- (<j>(C.2.2.2.1 @ j).2) @i@j)
+-- -- , <j> ((C.2.2.2.2 @ j).1
+-- -- ,lemIdPSet (sH X S C.1.1 C.1.1 C.1.2 C.1.2 (cC X C.1.1 A.1 C.1.1 C.2.2.1.1 C.2.1.1))
+-- -- (sH X S C.1.1 C.1.1 C.1.2 C.1.2 (cId X C.1.1))
+-- -- (propSet (sH X S C.1.1 C.1.1 C.1.2 C.1.2 (cC X C.1.1 A.1 C.1.1 C.2.2.1.1 C.2.1.1))
+-- -- (sHProp X S C.1.1 C.1.1 C.1.2 C.1.2 (cC X C.1.1 A.1 C.1.1 C.2.2.1.1 C.2.1.1)))
+-- -- (<j>sH X S C.1.1 C.1.1 C.1.2 C.1.2 (C.2.2.2.2 @ j).1)
+-- -- (sHComp X S C.1.1 A.1 C.1.1 C.1.2 A.2 C.1.2 C.2.2.1.1 C.2.1.1 C.2.2.1.2 C.2.1.2)
+-- -- (sHId X S C.1.1 C.1.2)
+-- -- (<j>((G (F C)).2.2.2.2 @ j).2)
+-- -- (<j>(C.2.2.2.2 @ j).2) @i@j))
+-- -- hole0 (A : cA D)
+-- -- : isContr ((C : (B1 : cA X) * ( iso X A.1 B1))
+-- -- * (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1)
+-- -- = isContrSig ((B1 : cA X) * ( iso X A.1 B1))
+-- -- (\(C : (B1 : cA X) * ( iso X A.1 B1)) ->
+-- -- (B2 : sP X S C.1) * (_ : sH X S A.1 C.1 A.2 B2 C.2.1) * sH X S C.1 A.1 B2 A.2 C.2.2.1)
+-- -- (isC A.1)
+-- -- (\(C : (B1 : cA X) * ( iso X A.1 B1)) ->
+-- -- let p : Id ((B1 : cA X) * ( iso X A.1 B1)) (A.1, idIso X A.1) C
+-- -- = lemIsCategory X isC A.1 C.1 C.2
+-- -- in transport
+-- -- (<i> isContr ((B2 : sP X S (p@i).1) * (_ : sH X S A.1 (p@i).1 A.2 B2 (p@i).2.1) * sH X S (p@i).1 A.1 B2 A.2 (p@i).2.2.1))
+-- -- ((A.2,sHId X S A.1 A.2,sHId X S A.1 A.2)
+-- -- ,\(Y : (B2 : sP X S A.1) * (_ : sH X S A.1 A.1 A.2 B2 (cId X A.1)) * sH X S A.1 A.1 B2 A.2 (cId X A.1)) ->
+-- -- <i> (isS A.1 A.2 Y.1 Y.2.1 Y.2.2 @ i
+-- -- ,lemIdPProp (sH X S A.1 A.1 A.2 A.2 (cId X A.1))
+-- -- (sH X S A.1 A.1 A.2 Y.1 (cId X A.1))
+-- -- (sHProp X S A.1 A.1 A.2 A.2 (cId X A.1))
+-- -- (<i>sH X S A.1 A.1 A.2 (isS A.1 A.2 Y.1 Y.2.1 Y.2.2 @ i) (cId X A.1))
+-- -- (sHId X S A.1 A.2) Y.2.1 @ i
+-- -- ,lemIdPProp (sH X S A.1 A.1 A.2 A.2 (cId X A.1))
+-- -- (sH X S A.1 A.1 Y.1 A.2 (cId X A.1))
+-- -- (sHProp X S A.1 A.1 A.2 A.2 (cId X A.1))
+-- -- (<i>sH X S A.1 A.1 (isS A.1 A.2 Y.1 Y.2.1 Y.2.2 @ i) A.2 (cId X A.1))
+-- -- (sHId X S A.1 A.2) Y.2.2 @ i)))
+-- -- hole (A : cA D) : isContr ((B : cA D) * iso D A B) = transport (<i>isContr(eq1 A@-i)) (hole0 A)
+
+--
+
+functor (A B : precategory) : U
+ = (Fob : cA A -> cA B)
+ * (Fmor : (x y : cA A) -> cH A x y -> cH B (Fob x) (Fob y))
+ * (Fid : (x : cA A) -> Id (cH B (Fob x) (Fob x)) (Fmor x x (cId A x)) (cId B (Fob x)))
+ * ((x y z : cA A) -> (f : cH A x y) -> (g : cH A y z) -> Id (cH B (Fob x) (Fob z)) (Fmor x z (cC A x y z f g)) (cC B (Fob x) (Fob y) (Fob z) (Fmor x y f) (Fmor y z g)))
+
+idFunctor (A : precategory) : functor A A
+ = (\(x : cA A) -> x
+ ,\(x y : cA A) (h : cH A x y) -> h
+ ,\(x : cA A) -> <_> cId A x
+ ,\(x y z : cA A) (f : cH A x y) (g : cH A y z) -> <_> cC A x y z f g)
+
+compFunctor (A B C : precategory) (F : functor A B) (G : functor B C) : functor A C
+ = (\(x : cA A) -> G.1 (F.1 x)
+ ,\(x y : cA A) (h : cH A x y) -> G.2.1 (F.1 x) (F.1 y) (F.2.1 x y h)
+ ,\(x : cA A) -> compId (cH C (G.1 (F.1 x)) (G.1 (F.1 x)))
+ (G.2.1 (F.1 x) (F.1 x) (F.2.1 x x (cId A x)))
+ (G.2.1 (F.1 x) (F.1 x) (cId B (F.1 x)))
+ (cId C (G.1 (F.1 x)))
+ (<i>G.2.1 (F.1 x) (F.1 x) (F.2.2.1 x @ i))
+ (G.2.2.1 (F.1 x))
+ ,\(x y z : cA A) (f : cH A x y) (g : cH A y z) ->
+ compId (cH C (G.1 (F.1 x)) (G.1 (F.1 z)))
+ (G.2.1 (F.1 x) (F.1 z) (F.2.1 x z (cC A x y z f g)))
+ (G.2.1 (F.1 x) (F.1 z) (cC B (F.1 x) (F.1 y) (F.1 z) (F.2.1 x y f) (F.2.1 y z g)))
+ (cC C (G.1 (F.1 x)) (G.1 (F.1 y)) (G.1 (F.1 z)) (G.2.1 (F.1 x) (F.1 y) (F.2.1 x y f)) (G.2.1 (F.1 y) (F.1 z) (F.2.1 y z g)))
+ (<i> G.2.1 (F.1 x) (F.1 z) (F.2.2.2 x y z f g @ i))
+ (G.2.2.2 (F.1 x) (F.1 y) (F.1 z) (F.2.1 x y f) (F.2.1 y z g))
+ )
+
+ffFunctor (A B : precategory) (F : functor A B) : U
+ = (a b : cA A) -> isEquiv (cH A a b) (cH B (F.1 a) (F.1 b)) (F.2.1 a b)
+ffEq (A B : precategory) (F : functor A B) (ff : ffFunctor A B F) (a b : cA A)
+ : Id U (cH A a b) (cH B (F.1 a) (F.1 b))
+ = equivId (cH A a b) (cH B (F.1 a) (F.1 b)) (F.2.1 a b) (ff a b)
+propFFFunctor (A B : precategory) (F : functor A B) : prop (ffFunctor A B F)
+ = propPi (cA A) (\(a : cA A) -> (b : cA A) -> isEquiv (cH A a b) (cH B (F.1 a) (F.1 b)) (F.2.1 a b))
+ (\(a : cA A) -> propPi (cA A) (\(b : cA A) -> isEquiv (cH A a b) (cH B (F.1 a) (F.1 b)) (F.2.1 a b))
+ (\(b : cA A) -> propIsEquiv (cH A a b) (cH B (F.1 a) (F.1 b)) (F.2.1 a b)))
+
+lem10 (A B : U) (e : equiv A B) (x y : B) (p : Id A (e.2 x).1.1 (e.2 y).1.1) : Id B x y
+ = transport
+ (compId U (Id B (e.1 (e.2 x).1.1) (e.1 (e.2 y).1.1)) (Id B x (e.1 (e.2 y).1.1)) (Id B x y)
+ (<i> Id B (retEq A B e x @ i) (e.1 (e.2 y).1.1)) (<i> Id B x (retEq A B e y @ i)))
+ (mapOnPath A B e.1 (e.2 x).1.1 (e.2 y).1.1 p)
+opaque lem10
+
+lem10' (A B : U) (e : equiv A B) (x y : A) (p : Id B (e.1 x) (e.1 y)) : Id A x y
+ = transport
+ (compId U (Id A (e.2 (e.1 x)).1.1 (e.2 (e.1 y)).1.1) (Id A x (e.2 (e.1 y)).1.1) (Id A x y)
+ (<i> Id A (secEq A B e x @ i) (e.2 (e.1 y)).1.1) (<i> Id A x (secEq A B e y @ i))
+ )
+ (mapOnPath B A (invEq A B e) (e.1 x) (e.1 y) p)
+opaque lem10'
+
+lemFF (A B : precategory) (F : functor A B) (ff : ffFunctor A B F) (x y : cA A)
+ : Id U (iso A x y) (iso B (F.1 x) (F.1 y))
+ = hole
+ where
+ F0 (f : iso A x y) : iso B (F.1 x) (F.1 y)
+ = (F.2.1 x y f.1, F.2.1 y x f.2.1
+ ,compId (cH B (F.1 x) (F.1 x))
+ (cC B (F.1 x) (F.1 y) (F.1 x) (F.2.1 x y f.1) (F.2.1 y x f.2.1))
+ (F.2.1 x x (cC A x y x f.1 f.2.1))
+ (cId B (F.1 x))
+ (<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
+
+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
+
+catIsEquiv (A B : precategory) (F : functor A B) : U
+ = (_ : ffFunctor A B F)
+ * ((b : cA B) -> (a : cA A) * iso B (F.1 a) b)
+catEquiv (A B : precategory) : U = (F : functor A B) * catIsEquiv A B F
+catPropIsEquiv (A B : precategory) (isC : isCategory A) (F : functor A B) : prop (catIsEquiv A B F)
+ = propSig (ffFunctor A B F) (\(_ : ffFunctor A B F) -> (b : cA B) -> (a : cA A) * iso B (F.1 a) b)
+ (propFFFunctor A B F)
+ (\(ff : ffFunctor A B F) -> propPi (cA B) (\(b : cA B) -> (a : cA A) * iso B (F.1 a) b)
+ (\(b : cA B) -> F23 A B F (F12 A B isC F ff) b))
+
+catIsIso (A B : precategory) (F : functor A B) : U
+ = (_ : ffFunctor A B F) * isEquiv (cA A) (cA B) F.1
+catPropIsIso (A B : precategory) (F : functor A B) : prop (catIsIso A B F)
+ = propSig (ffFunctor A B F) (\(_ : ffFunctor A B F) -> isEquiv (cA A) (cA B) F.1)
+ (propFFFunctor A B F)
+ (\(_ : ffFunctor A B F) -> propIsEquiv (cA A) (cA B) F.1)
+catIso (A B : precategory) : U = (F : functor A B) * catIsIso A B F
+
+catIso2 (A B : precategory) : U = (e1 : equiv (cA A) (cA B))
+ * (e2 : (x y : cA A) -> equiv (cH A x y) (cH B (e1.1 x) (e1.1 y)))
+ * (_ : (x : cA A) -> Id (cH B (e1.1 x) (e1.1 x)) ((e2 x x).1 (cId A x)) (cId B (e1.1 x)))
+ * ((x y z : cA A) -> (f : cH A x y) -> (g : cH A y z) ->
+ Id (cH B (e1.1 x) (e1.1 z))
+ ((e2 x z).1 (cC A x y z f g))
+ (cC B (e1.1 x) (e1.1 y) (e1.1 z) ((e2 x y).1 f) ((e2 y z).1 g)))
+
+catIsoIsEquiv (A B : precategory) (F : functor A B) (e : catIsIso A B F) : catIsEquiv A B F
+ = (e.1,\(b:cA B)->((e.2 b).1.1, eqToIso B (F.1 (e.2 b).1.1) b (<i>(e.2 b).1.2@-i)))
+
+invEquiv (A:U) (a b:A) : Id U (Id A a b) (Id A b a)
+ = equivId (Id A a b) (Id A b a) (inv A a b) (gradLemma (Id A a b) (Id A b a) (inv A a b) (inv A b a) (\(x:Id A b a) -> <_> x) (\(x:Id A a b) -> <_> x))
+
+catEquivIsIso (A B : precategory) (isCA : isCategory A) (isCB : isCategory B) (F : functor A B) (e : catIsEquiv A B F)
+ : catIsIso A B F
+ = (e.1, \(b:cA B)->
+ let p : isContr ((a:cA A)*iso B (F.1 a) b)
+ = (e.2 b, F23 A B F (F12 A B isCA F e.1) b (e.2 b))
+ in transport (<i>isContr ((a:cA A)*invEquiv (cA B) (F.1 a) b @ i))
+ (transport (<i> isContr ((a:cA A)*lemIsCategory3 B isCB (F.1 a) b@-i)) p))
+
+equivProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A) : equiv A B =
+ (F, gradLemma A B F G (\(y : B) -> BProp (F (G y)) y) (\(x : A) -> AProp (G (F x)) x))
+
+catIsEquivEqIso (A B : precategory) (isCA : isCategory A) (isCB : isCategory B) (F : functor A B)
+ : equiv (catIsEquiv A B F) (catIsIso A B F)
+ = equivProp (catIsEquiv A B F) (catIsIso A B F) (catPropIsEquiv A B isCA F) (catPropIsIso A B F)
+ (catEquivIsIso A B isCA isCB F) (catIsoIsEquiv A B F)
+
+catEquivEqIso (A B : precategory) (isCA : isCategory A) (isCB : isCategory B) : Id U (catEquiv A B) (catIso A B)
+ = <i> (F : functor A B) * (transEquivToId (catIsEquiv A B F) (catIsIso A B F) (catIsEquivEqIso A B isCA isCB F) @ i)
+
+catIsoEqId (A B : precategory) : Id U (catIso A B) (Id precategory A B)
+ = ?
+
+-- lemIdSig (A:U) (B : A -> U) (t u : Sigma A B) :
+-- Id U (Id (Sigma A B) t u) ((p : Id A t.1 u.1) * IdP (<i> B (p @ i)) t.2 u.2) =
+
+stop : Unit = U
-- f'
-- W -----> Z
-- Y -----> X
-- f
-homTo (C : precategory) (X : cA C) : U = (Y : cA C) * cH C Y X
-cospan (C : precategory) : U
- = (X : cA C) * (_ : homTo C X) * homTo C X
-cospanCone (C : precategory) (D : cospan C) : U
- = (W : cA C) * (f : cH C W D.2.1.1) * (g : cH C W D.2.2.1)
- * Id (cH C W D.1)
- (cC C W D.2.1.1 D.1 f D.2.1.2)
- (cC C W D.2.2.1 D.1 g D.2.2.2)
-cospanConeHom (C : precategory) (D : cospan C) (E1 E2 : cospanCone C D) : U
- = (h : cH C E1.1 E2.1)
- * (_ : Id (cH C E1.1 D.2.1.1) (cC C E1.1 E2.1 D.2.1.1 h E2.2.1) E1.2.1)
- * (Id (cH C E1.1 D.2.2.1) (cC C E1.1 E2.1 D.2.2.1 h E2.2.2.1) E1.2.2.1)
-cospanConeId (C : precategory) (D : cospan C) (E : cospanCone C D) : cospanConeHom C D E E
- = (cId C E.1, cIdL C E.1 D.2.1.1 E.2.1, cIdL C E.1 D.2.2.1 E.2.2.1)
-cospanConeComp (C : precategory) (D : cospan C) (X Y Z : cospanCone C D)
- (F : cospanConeHom C D X Y) (G : cospanConeHom C D Y Z) : cospanConeHom C D X Z
- = (cC C X.1 Y.1 Z.1 F.1 G.1
- ,compId (cH C X.1 D.2.1.1)
- (cC C X.1 Z.1 D.2.1.1 (cC C X.1 Y.1 Z.1 F.1 G.1) Z.2.1)
- (cC C X.1 Y.1 D.2.1.1 F.1 (cC C Y.1 Z.1 D.2.1.1 G.1 Z.2.1))
- X.2.1
- (cIdC C X.1 Y.1 Z.1 D.2.1.1 F.1 G.1 Z.2.1)
- (compId (cH C X.1 D.2.1.1)
- (cC C X.1 Y.1 D.2.1.1 F.1 (cC C Y.1 Z.1 D.2.1.1 G.1 Z.2.1))
- (cC C X.1 Y.1 D.2.1.1 F.1 Y.2.1)
- X.2.1
- (<i> cC C X.1 Y.1 D.2.1.1 F.1 (G.2.1 @ i))
- F.2.1)
- ,compId (cH C X.1 D.2.2.1)
- (cC C X.1 Z.1 D.2.2.1 (cC C X.1 Y.1 Z.1 F.1 G.1) Z.2.2.1)
- (cC C X.1 Y.1 D.2.2.1 F.1 (cC C Y.1 Z.1 D.2.2.1 G.1 Z.2.2.1))
- X.2.2.1
- (cIdC C X.1 Y.1 Z.1 D.2.2.1 F.1 G.1 Z.2.2.1)
- (compId (cH C X.1 D.2.2.1)
- (cC C X.1 Y.1 D.2.2.1 F.1 (cC C Y.1 Z.1 D.2.2.1 G.1 Z.2.2.1))
- (cC C X.1 Y.1 D.2.2.1 F.1 Y.2.2.1)
- X.2.2.1
- (<i> cC C X.1 Y.1 D.2.2.1 F.1 (G.2.2 @ i))
- F.2.2))
-
-isPullback (C : precategory) (D : cospan C) (E : cospanCone C D) : U
- = (h : cospanCone C D) -> isContr (cospanConeHom C D h E)
-isPullbackProp (C : precategory) (D : cospan C) (E : cospanCone C D) : prop (isPullback C D E)
- = propPi (cospanCone C D) (\(h : cospanCone C D) -> isContr (cospanConeHom C D h E))
- (\(h : cospanCone C D) -> propIsContr (cospanConeHom C D h E))
-hasPullback (C : precategory) (D : cospan C) : U = (E : cospanCone C D) * isPullback C D E
-
-cospanConePrecategory (C : precategory) (D : cospan C) : precategory
- = ((cospanCone C D, cospanConeHom C D)
- ,(\(X Y : cospanCone C D) -> setSig (cH C X.1 Y.1)
- (\(h : cH C X.1 Y.1) ->
- (_ : Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1)
- * (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 h Y.2.2.1) X.2.2.1))
- (cHSet C X.1 Y.1)
- (\(h : cH C X.1 Y.1) -> setSig (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1)
- (\(_ : Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1) ->
- (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 h Y.2.2.1) X.2.2.1))
- (propSet (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1)
- (cHSet C X.1 D.2.1.1 (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1))
- (\(_ : Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 h Y.2.1) X.2.1) ->
- (propSet (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 h Y.2.2.1) X.2.2.1)
- (cHSet C X.1 D.2.2.1 (cC C X.1 Y.1 D.2.2.1 h Y.2.2.1) X.2.2.1)))))
- ,cospanConeId C D
- ,cospanConeComp C D
- ,\(X Y : cospanCone C D) (F : cospanConeHom C D X Y) ->
- <i> (cIdL C X.1 Y.1 F.1 @ i
- ,lemIdPProp (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdL C X.1 Y.1 F.1 @ 0) Y.2.1) X.2.1)
- (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdL C X.1 Y.1 F.1 @ 1) Y.2.1) X.2.1)
- (cHSet C X.1 D.2.1.1 (cC C X.1 Y.1 D.2.1.1 (cIdL C X.1 Y.1 F.1 @ 0) Y.2.1) X.2.1)
- (<i>Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdL C X.1 Y.1 F.1 @ i) Y.2.1) X.2.1)
- (cospanConeComp C D X X Y (cospanConeId C D X) F).2.1
- F.2.1 @ i
- ,lemIdPProp (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdL C X.1 Y.1 F.1 @ 0) Y.2.2.1) X.2.2.1)
- (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdL C X.1 Y.1 F.1 @ 1) Y.2.2.1) X.2.2.1)
- (cHSet C X.1 D.2.2.1 (cC C X.1 Y.1 D.2.2.1 (cIdL C X.1 Y.1 F.1 @ 0) Y.2.2.1) X.2.2.1)
- (<i>Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdL C X.1 Y.1 F.1 @ i) Y.2.2.1) X.2.2.1)
- (cospanConeComp C D X X Y (cospanConeId C D X) F).2.2
- F.2.2 @ i)
- ,\(X Y : cospanCone C D) (F : cospanConeHom C D X Y) ->
- <i> (cIdR C X.1 Y.1 F.1 @ i
- ,lemIdPProp (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdR C X.1 Y.1 F.1 @ 0) Y.2.1) X.2.1)
- (Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdR C X.1 Y.1 F.1 @ 1) Y.2.1) X.2.1)
- (cHSet C X.1 D.2.1.1 (cC C X.1 Y.1 D.2.1.1 (cIdR C X.1 Y.1 F.1 @ 0) Y.2.1) X.2.1)
- (<i>Id (cH C X.1 D.2.1.1) (cC C X.1 Y.1 D.2.1.1 (cIdR C X.1 Y.1 F.1 @ i) Y.2.1) X.2.1)
- (cospanConeComp C D X Y Y F (cospanConeId C D Y)).2.1
- F.2.1 @ i
- ,lemIdPProp (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdR C X.1 Y.1 F.1 @ 0) Y.2.2.1) X.2.2.1)
- (Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdR C X.1 Y.1 F.1 @ 1) Y.2.2.1) X.2.2.1)
- (cHSet C X.1 D.2.2.1 (cC C X.1 Y.1 D.2.2.1 (cIdR C X.1 Y.1 F.1 @ 0) Y.2.2.1) X.2.2.1)
- (<i>Id (cH C X.1 D.2.2.1) (cC C X.1 Y.1 D.2.2.1 (cIdR C X.1 Y.1 F.1 @ i) Y.2.2.1) X.2.2.1)
- (cospanConeComp C D X Y Y F (cospanConeId C D Y)).2.2
- F.2.2 @ i)
- ,\(X Y Z W : cospanCone C D) (F : cospanConeHom C D X Y) (G : cospanConeHom C D Y Z) (H : cospanConeHom C D Z W) ->
- <i> (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ i
- ,lemIdPProp (Id (cH C X.1 D.2.1.1) (cC C X.1 W.1 D.2.1.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 0) W.2.1) X.2.1)
- (Id (cH C X.1 D.2.1.1) (cC C X.1 W.1 D.2.1.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 1) W.2.1) X.2.1)
- (cHSet C X.1 D.2.1.1 (cC C X.1 W.1 D.2.1.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 0) W.2.1) X.2.1)
- (<i>Id (cH C X.1 D.2.1.1) (cC C X.1 W.1 D.2.1.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ i) W.2.1) X.2.1)
- (cospanConeComp C D X Z W (cospanConeComp C D X Y Z F G) H).2.1
- (cospanConeComp C D X Y W F (cospanConeComp C D Y Z W G H)).2.1 @ i
- ,lemIdPProp (Id (cH C X.1 D.2.2.1) (cC C X.1 W.1 D.2.2.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 0) W.2.2.1) X.2.2.1)
- (Id (cH C X.1 D.2.2.1) (cC C X.1 W.1 D.2.2.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 1) W.2.2.1) X.2.2.1)
- (cHSet C X.1 D.2.2.1 (cC C X.1 W.1 D.2.2.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ 0) W.2.2.1) X.2.2.1)
- (<i>Id (cH C X.1 D.2.2.1) (cC C X.1 W.1 D.2.2.1 (cIdC C X.1 Y.1 Z.1 W.1 F.1 G.1 H.1 @ i) W.2.2.1) X.2.2.1)
- (cospanConeComp C D X Z W (cospanConeComp C D X Y Z F G) H).2.2
- (cospanConeComp C D X Y W F (cospanConeComp C D Y Z W G H)).2.2 @ i))
-
-isCategoryCospanCone (C : precategory) (isC : isCategory C) (D : cospan C)
- : isCategory (cospanConePrecategory C D)
- = undefined
- -- = \(A : cospanCone C D) ->
- -- let p (X : (B : cospanCone C D) * iso (cospanConePrecategory C D) A B)
- -- : Id ((B : cospanCone C D) * iso (cospanConePrecategory C D) A B) (A, isoId (cospanConePrecategory C D) A) X
- -- = <i> ((?, ?, ?, ?)
- -- ,(?, ?, ?, ?))
- -- in ?
-
-isFinal (C : precategory) (A : cA C) : U = (B : cA C) -> isContr (cH C B A)
-isFinalProp (C : precategory) (A : cA C) : prop (isFinal C A)
- = propPi (cA C) (\(B : cA C) -> isContr (cH C B A))
- (\(B : cA C) -> propIsContr (cH C B A))
-
-hasFinal (C : precategory) : U = (A : cA C) * isFinal C A
-
-hasFinalProp (C : precategory) (isC : isCategory C) : prop (hasFinal C)
- = \(x y : hasFinal C) ->
- let p : iso C x.1 y.1
- = ((y.2 x.1).1, (x.2 y.1).1
- , isContrProp (cH C x.1 x.1) (x.2 x.1) (cC C x.1 y.1 x.1 (y.2 x.1).1 (x.2 y.1).1) (cId C x.1)
- , isContrProp (cH C y.1 y.1) (y.2 y.1) (cC C y.1 x.1 y.1 (x.2 y.1).1 (y.2 x.1).1) (cId C y.1))
- in <i> ( lemIsCategory C isC x.1 y.1 p @ i
- , lemIdPProp (isFinal C x.1)
- (isFinal C y.1)
- (isFinalProp C x.1)
- (<i> isFinal C (lemIsCategory C isC x.1 y.1 p @ i))
- x.2 y.2 @ i)
-
-hasPullbackProp (C : precategory) (isC : isCategory C) (D : cospan C) : prop (hasPullback C D)
- = hasFinalProp (cospanConePrecategory C D) (isCategoryCospanCone C isC D)
-
-isCommutative (CA : precategory)
- (A B C D : cA CA)
- (f : cH CA A B) (g : cH CA C D)
- (h : cH CA A C) (i : cH CA B D)
- : U = Id (cH CA A D) (cC CA A C D h g) (cC CA A B D f i)
-
-pullbackPasting
- (CA : precategory)
- (A B C D E F : cA CA)
- (f : cH CA A B) (g : cH CA B C)
- (h : cH CA D E) (i : cH CA E F)
- (j : cH CA A D) (k : cH CA B E) (l : cH CA C F)
- (cc1 : isCommutative CA A B D E f h j k)
- (cc2 : isCommutative CA B C E F g i k l)
- (cc3 : isCommutative CA A C D F (cC CA A B C f g) (cC CA D E F h i) j l)
- (pb2 : isPullback CA (F, (E, i), (C, l)) (B, k, g, cc2))
- (pb3 : isPullback CA (F, (D, cC CA D E F h i), (C, l)) (A, j, cC CA A B C f g, cc3))
- : isPullback CA (E, (D, h), (B, k)) (A, j, f, cc1)
- = \(c : cospanCone CA (E, (D, h), (B, k))) ->
- let hole : Id (cH CA c.1 F)
- (cC CA c.1 D F c.2.1 (cC CA D E F h i))
- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
- = compId (cH CA c.1 F)
- (cC CA c.1 D F c.2.1 (cC CA D E F h i))
- (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i)
- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
- (<n>cIdC CA c.1 D E F c.2.1 h i@-n)
- (compId (cH CA c.1 F)
- (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i)
- (cC CA c.1 E F (cC CA c.1 B E c.2.2.1 k) i)
- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
- (<n>cC CA c.1 E F (c.2.2.2@n) i)
- (compId (cH CA c.1 F)
- (cC CA c.1 E F (cC CA c.1 B E c.2.2.1 k) i)
- (cC CA c.1 B F c.2.2.1 (cC CA B E F k i))
- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
- (cIdC CA c.1 B E F c.2.2.1 k i)
- (compId (cH CA c.1 F)
- (cC CA c.1 B F c.2.2.1 (cC CA B E F k i))
- (cC CA c.1 B F c.2.2.1 (cC CA B C F g l))
- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
- (<n>cC CA c.1 B F c.2.2.1 (cc2@n))
- (<n>cIdC CA c.1 B C F c.2.2.1 g l@-n))))
- c' : cospanCone CA (F, (D, cC CA D E F h i), (C, l))
- = (c.1
- ,c.2.1
- ,cC CA c.1 B C c.2.2.1 g
- ,hole)
-
- hole2 : Id (cH CA c.1 F)
- (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i)
- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
- = compId (cH CA c.1 F)
- (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i)
- (cC CA c.1 D F c.2.1 (cC CA D E F h i))
- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
- (cIdC CA c.1 D E F c.2.1 h i)
- hole
- cc : cospanCone CA (F, (E, i), (C, l))
- = (c.1, cC CA c.1 D E c.2.1 h, c'.2.2.1, hole2)
-
- p0 (h' : cH CA c.1 A) (p : Id (cH CA c.1 D) (cC CA c.1 A D h' j) c.2.1)
- : Id U (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1)
- (Id (cH CA c.1 C) (cC CA c.1 A C h' (cC CA A B C f g)) c'.2.2.1)
- = transport
- (<i> Id U (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1)
- (Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ i) c'.2.2.1))
- (idProp (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1)
- (Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1)
- (cHSet CA c.1 B (cC CA c.1 A B h' f) c.2.2.1)
- (cHSet CA c.1 C (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1)
- (\(p:Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1) ->
- <i> cC CA c.1 B C (p@i) g)
- (\(p1:Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1) ->
- let h1 : cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2)
- = (cC CA c.1 A B h' f
- ,compId (cH CA c.1 E)
- (cC CA c.1 B E (cC CA c.1 A B h' f) k)
- (cC CA c.1 A E h' (cC CA A B E f k))
- (cC CA c.1 D E c.2.1 h)
- (cIdC CA c.1 A B E h' f k)
- (compId (cH CA c.1 E)
- (cC CA c.1 A E h' (cC CA A B E f k))
- (cC CA c.1 A E h' (cC CA A D E j h))
- (cC CA c.1 D E c.2.1 h)
- (<i>cC CA c.1 A E h' (cc1@-i))
- (compId (cH CA c.1 E)
- (cC CA c.1 A E h' (cC CA A D E j h))
- (cC CA c.1 D E (cC CA c.1 A D h' j) h)
- (cC CA c.1 D E c.2.1 h)
- (<i> cIdC CA c.1 A D E h' j h @ -i)
- (<i> cC CA c.1 D E (p@i) h)))
- ,p1)
- h2 : cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2)
- = (c.2.2.1
- ,<i>c.2.2.2@-i
- ,<_>c'.2.2.1)
- in <n> (isContrProp (cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2)) (pb2 cc) h1 h2 @ n).1
- ))
-
- p : Id U (cospanConeHom CA (F, (D, cC CA D E F h i), (C, l)) c' (A, j, cC CA A B C f g, cc3))
- (cospanConeHom CA (E, (D, h), (B, k)) c (A, j, f, cc1))
- = <i> (h : cH CA c.1 A)
- * (p : Id (cH CA c.1 D) (cC CA c.1 A D h j) c.2.1)
- * (p0 h p @ -i)
- in transport (<i> isContr (p@i)) (pb3 c')
+-- homTo (C : precategory) (X : cA C) : U = (Y : cA C) * cH C Y X
+-- cospan (C : precategory) : U
+-- = (X : cA C) * (_ : homTo C X) * homTo C X
+-- hasCospanCone (C : precategory) (D : cospan C) (W : cA C) : U
+-- = (f : cH C W D.2.1.1) * (g : cH C W D.2.2.1)
+-- * Id (cH C W D.1)
+-- (cC C W D.2.1.1 D.1 f D.2.1.2)
+-- (cC C W D.2.2.1 D.1 g D.2.2.2)
+-- cospanCone (C : precategory) (D : cospan C) : U = (W : cA C) * hasCospanCone C D W
+
+-- isCospanConeHom (C : precategory) (D : cospan C) (E1 E2 : cospanCone C D) (h : cH C E1.1 E2.1) : U
+-- = (_ : Id (cH C E1.1 D.2.1.1) (cC C E1.1 E2.1 D.2.1.1 h E2.2.1) E1.2.1)
+-- * (Id (cH C E1.1 D.2.2.1) (cC C E1.1 E2.1 D.2.2.1 h E2.2.2.1) E1.2.2.1)
+-- isCospanConeHomProp (C : precategory) (D : cospan C) (E1 E2 : cospanCone C D) (h : cH C E1.1 E2.1)
+-- : prop (isCospanConeHom C D E1 E2 h)
+-- = propAnd (Id (cH C E1.1 D.2.1.1) (cC C E1.1 E2.1 D.2.1.1 h E2.2.1) E1.2.1)
+-- (Id (cH C E1.1 D.2.2.1) (cC C E1.1 E2.1 D.2.2.1 h E2.2.2.1) E1.2.2.1)
+-- (cHSet C E1.1 D.2.1.1 (cC C E1.1 E2.1 D.2.1.1 h E2.2.1) E1.2.1)
+-- (cHSet C E1.1 D.2.2.1 (cC C E1.1 E2.1 D.2.2.1 h E2.2.2.1) E1.2.2.1)
+
+-- cospanConeHom (C : precategory) (D : cospan C) (E1 E2 : cospanCone C D) : U
+-- = (h : cH C E1.1 E2.1) * isCospanConeHom C D E1 E2 h
+-- cospanConeId (C : precategory) (D : cospan C) (E : cospanCone C D) : cospanConeHom C D E E
+-- = (cId C E.1, cIdL C E.1 D.2.1.1 E.2.1, cIdL C E.1 D.2.2.1 E.2.2.1)
+-- cospanConeComp (C : precategory) (D : cospan C) (X Y Z : cospanCone C D)
+-- (F : cospanConeHom C D X Y) (G : cospanConeHom C D Y Z) : cospanConeHom C D X Z
+-- = (cC C X.1 Y.1 Z.1 F.1 G.1
+-- ,compId (cH C X.1 D.2.1.1)
+-- (cC C X.1 Z.1 D.2.1.1 (cC C X.1 Y.1 Z.1 F.1 G.1) Z.2.1)
+-- (cC C X.1 Y.1 D.2.1.1 F.1 (cC C Y.1 Z.1 D.2.1.1 G.1 Z.2.1))
+-- X.2.1
+-- (cIdC C X.1 Y.1 Z.1 D.2.1.1 F.1 G.1 Z.2.1)
+-- (compId (cH C X.1 D.2.1.1)
+-- (cC C X.1 Y.1 D.2.1.1 F.1 (cC C Y.1 Z.1 D.2.1.1 G.1 Z.2.1))
+-- (cC C X.1 Y.1 D.2.1.1 F.1 Y.2.1)
+-- X.2.1
+-- (<i> cC C X.1 Y.1 D.2.1.1 F.1 (G.2.1 @ i))
+-- F.2.1)
+-- ,compId (cH C X.1 D.2.2.1)
+-- (cC C X.1 Z.1 D.2.2.1 (cC C X.1 Y.1 Z.1 F.1 G.1) Z.2.2.1)
+-- (cC C X.1 Y.1 D.2.2.1 F.1 (cC C Y.1 Z.1 D.2.2.1 G.1 Z.2.2.1))
+-- X.2.2.1
+-- (cIdC C X.1 Y.1 Z.1 D.2.2.1 F.1 G.1 Z.2.2.1)
+-- (compId (cH C X.1 D.2.2.1)
+-- (cC C X.1 Y.1 D.2.2.1 F.1 (cC C Y.1 Z.1 D.2.2.1 G.1 Z.2.2.1))
+-- (cC C X.1 Y.1 D.2.2.1 F.1 Y.2.2.1)
+-- X.2.2.1
+-- (<i> cC C X.1 Y.1 D.2.2.1 F.1 (G.2.2 @ i))
+-- F.2.2))
+
+-- isPullback (C : precategory) (D : cospan C) (E : cospanCone C D) : U
+-- = (h : cospanCone C D) -> isContr (cospanConeHom C D h E)
+-- isPullbackProp (C : precategory) (D : cospan C) (E : cospanCone C D) : prop (isPullback C D E)
+-- = propPi (cospanCone C D) (\(h : cospanCone C D) -> isContr (cospanConeHom C D h E))
+-- (\(h : cospanCone C D) -> propIsContr (cospanConeHom C D h E))
+-- hasPullback (C : precategory) (D : cospan C) : U = (E : cospanCone C D) * isPullback C D E
+
+-- cospanConeStructure (C : precategory) (D : cospan C) : structure C
+-- = (hasCospanCone C D
+-- ,\(x y : cA C) (a : hasCospanCone C D x) (b : hasCospanCone C D y) -> isCospanConeHom C D (x, a) (y, b)
+-- ,\(x y : cA C) (a : hasCospanCone C D x) (b : hasCospanCone C D y) -> isCospanConeHomProp C D (x, a) (y, b)
+-- ,\(x : cA C) (a : hasCospanCone C D x) -> (cospanConeId C D (x, a)).2
+-- ,\(x y z : cA C) (a : hasCospanCone C D x) (b : hasCospanCone C D y) (c : hasCospanCone C D z)
+-- (f : cH C x y) (g : cH C y z)
+-- (Hf : isCospanConeHom C D (x, a) (y, b) f)
+-- (Hg : isCospanConeHom C D (y, b) (z, c) g) -> (cospanConeComp C D (x, a) (y, b) (z, c) (f, Hf) (g, Hg)).2
+-- )
+
+-- cospanConePrecategory (C : precategory) (D : cospan C) : precategory
+-- = sipPrecategory C (cospanConeStructure C D)
+
+-- isCategoryCospanCone (C : precategory) (D : cospan C) (isC : isCategory C) : isCategory (cospanConePrecategory C D)
+-- = sip C isC (cospanConeStructure C D) hole
+-- where
+-- hole : isStandardStructure C (cospanConeStructure C D)
+-- = \(x : cA C) (a b : hasCospanCone C D x)
+-- (c : isCospanConeHom C D (x, a) (x, b) (cId C x))
+-- (d : isCospanConeHom C D (x, b) (x, a) (cId C x)) ->
+-- <i> (compId (cH C x D.2.1.1) a.1 (cC C x x D.2.1.1 (cId C x) a.1) b.1 (<i>cIdL C x D.2.1.1 a.1 @-i) d.1 @ i
+-- ,compId (cH C x D.2.2.1) a.2.1 (cC C x x D.2.2.1 (cId C x) a.2.1) b.2.1 (<i>cIdL C x D.2.2.1 a.2.1 @-i) d.2 @ i
+-- ,lemIdPProp (Id (cH C x D.1) (cC C x D.2.1.1 D.1 a.1 D.2.1.2) (cC C x D.2.2.1 D.1 a.2.1 D.2.2.2))
+-- (Id (cH C x D.1) (cC C x D.2.1.1 D.1 b.1 D.2.1.2) (cC C x D.2.2.1 D.1 b.2.1 D.2.2.2))
+-- (cHSet C x D.1 (cC C x D.2.1.1 D.1 a.1 D.2.1.2) (cC C x D.2.2.1 D.1 a.2.1 D.2.2.2))
+-- (<i>Id (cH C x D.1)
+-- (cC C x D.2.1.1 D.1 (compId (cH C x D.2.1.1) a.1 (cC C x x D.2.1.1 (cId C x) a.1) b.1
+-- (<i>cIdL C x D.2.1.1 a.1 @-i) d.1 @ i) D.2.1.2)
+-- (cC C x D.2.2.1 D.1 (compId (cH C x D.2.2.1) a.2.1 (cC C x x D.2.2.1 (cId C x) a.2.1) b.2.1
+-- (<i>cIdL C x D.2.2.1 a.2.1 @-i) d.2 @ i) D.2.2.2))
+-- a.2.2 b.2.2 @ i)
+
+-- isFinal (C : precategory) (A : cA C) : U = (B : cA C) -> isContr (cH C B A)
+-- isFinalProp (C : precategory) (A : cA C) : prop (isFinal C A)
+-- = propPi (cA C) (\(B : cA C) -> isContr (cH C B A))
+-- (\(B : cA C) -> propIsContr (cH C B A))
+
+-- hasFinal (C : precategory) : U = (A : cA C) * isFinal C A
+
+-- hasFinalProp (C : precategory) (isC : isCategory C) : prop (hasFinal C)
+-- = \(x y : hasFinal C) ->
+-- let p : iso C x.1 y.1
+-- = ((y.2 x.1).1, (x.2 y.1).1
+-- , isContrProp (cH C x.1 x.1) (x.2 x.1) (cC C x.1 y.1 x.1 (y.2 x.1).1 (x.2 y.1).1) (cId C x.1)
+-- , isContrProp (cH C y.1 y.1) (y.2 y.1) (cC C y.1 x.1 y.1 (x.2 y.1).1 (y.2 x.1).1) (cId C y.1))
+-- in <i> ( (lemIsCategory C isC x.1 y.1 p @ i).1
+-- , lemIdPProp (isFinal C x.1)
+-- (isFinal C y.1)
+-- (isFinalProp C x.1)
+-- (<i> isFinal C (lemIsCategory C isC x.1 y.1 p @ i).1)
+-- x.2 y.2 @ i)
+
+-- hasPullbackProp (C : precategory) (isC : isCategory C) (D : cospan C) : prop (hasPullback C D)
+-- = hasFinalProp (cospanConePrecategory C D) (isCategoryCospanCone C D isC)
+
+-- isCommutative (CA : precategory)
+-- (A B C D : cA CA)
+-- (f : cH CA A B) (g : cH CA C D)
+-- (h : cH CA A C) (i : cH CA B D)
+-- : U = Id (cH CA A D) (cC CA A C D h g) (cC CA A B D f i)
+
+-- pullbackPasting
+-- (CA : precategory)
+-- (A B C D E F : cA CA)
+-- (f : cH CA A B) (g : cH CA B C)
+-- (h : cH CA D E) (i : cH CA E F)
+-- (j : cH CA A D) (k : cH CA B E) (l : cH CA C F)
+-- (cc1 : isCommutative CA A B D E f h j k)
+-- (cc2 : isCommutative CA B C E F g i k l)
+-- (cc3 : isCommutative CA A C D F (cC CA A B C f g) (cC CA D E F h i) j l)
+-- (pb2 : isPullback CA (F, (E, i), (C, l)) (B, k, g, cc2))
+-- (pb3 : isPullback CA (F, (D, cC CA D E F h i), (C, l)) (A, j, cC CA A B C f g, cc3))
+-- : isPullback CA (E, (D, h), (B, k)) (A, j, f, cc1)
+-- = \(c : cospanCone CA (E, (D, h), (B, k))) ->
+-- let hole : Id (cH CA c.1 F)
+-- (cC CA c.1 D F c.2.1 (cC CA D E F h i))
+-- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+-- = compId (cH CA c.1 F)
+-- (cC CA c.1 D F c.2.1 (cC CA D E F h i))
+-- (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i)
+-- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+-- (<n>cIdC CA c.1 D E F c.2.1 h i@-n)
+-- (compId (cH CA c.1 F)
+-- (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i)
+-- (cC CA c.1 E F (cC CA c.1 B E c.2.2.1 k) i)
+-- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+-- (<n>cC CA c.1 E F (c.2.2.2@n) i)
+-- (compId (cH CA c.1 F)
+-- (cC CA c.1 E F (cC CA c.1 B E c.2.2.1 k) i)
+-- (cC CA c.1 B F c.2.2.1 (cC CA B E F k i))
+-- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+-- (cIdC CA c.1 B E F c.2.2.1 k i)
+-- (compId (cH CA c.1 F)
+-- (cC CA c.1 B F c.2.2.1 (cC CA B E F k i))
+-- (cC CA c.1 B F c.2.2.1 (cC CA B C F g l))
+-- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+-- (<n>cC CA c.1 B F c.2.2.1 (cc2@n))
+-- (<n>cIdC CA c.1 B C F c.2.2.1 g l@-n))))
+-- c' : cospanCone CA (F, (D, cC CA D E F h i), (C, l))
+-- = (c.1
+-- ,c.2.1
+-- ,cC CA c.1 B C c.2.2.1 g
+-- ,hole)
+
+-- hole2 : Id (cH CA c.1 F)
+-- (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i)
+-- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+-- = compId (cH CA c.1 F)
+-- (cC CA c.1 E F (cC CA c.1 D E c.2.1 h) i)
+-- (cC CA c.1 D F c.2.1 (cC CA D E F h i))
+-- (cC CA c.1 C F (cC CA c.1 B C c.2.2.1 g) l)
+-- (cIdC CA c.1 D E F c.2.1 h i)
+-- hole
+-- cc : cospanCone CA (F, (E, i), (C, l))
+-- = (c.1, cC CA c.1 D E c.2.1 h, c'.2.2.1, hole2)
+
+-- p0 (h' : cH CA c.1 A) (p : Id (cH CA c.1 D) (cC CA c.1 A D h' j) c.2.1)
+-- : Id U (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1)
+-- (Id (cH CA c.1 C) (cC CA c.1 A C h' (cC CA A B C f g)) c'.2.2.1)
+-- = transport
+-- (<i> Id U (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1)
+-- (Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ i) c'.2.2.1))
+-- (idProp (Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1)
+-- (Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1)
+-- (cHSet CA c.1 B (cC CA c.1 A B h' f) c.2.2.1)
+-- (cHSet CA c.1 C (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1)
+-- (\(p:Id (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1) ->
+-- <i> cC CA c.1 B C (p@i) g)
+-- (\(p1:Id (cH CA c.1 C) (cIdC CA c.1 A B C h' f g @ 0) c'.2.2.1) ->
+-- let h1 : cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2)
+-- = (cC CA c.1 A B h' f
+-- ,compId (cH CA c.1 E)
+-- (cC CA c.1 B E (cC CA c.1 A B h' f) k)
+-- (cC CA c.1 A E h' (cC CA A B E f k))
+-- (cC CA c.1 D E c.2.1 h)
+-- (cIdC CA c.1 A B E h' f k)
+-- (compId (cH CA c.1 E)
+-- (cC CA c.1 A E h' (cC CA A B E f k))
+-- (cC CA c.1 A E h' (cC CA A D E j h))
+-- (cC CA c.1 D E c.2.1 h)
+-- (<i>cC CA c.1 A E h' (cc1@-i))
+-- (compId (cH CA c.1 E)
+-- (cC CA c.1 A E h' (cC CA A D E j h))
+-- (cC CA c.1 D E (cC CA c.1 A D h' j) h)
+-- (cC CA c.1 D E c.2.1 h)
+-- (<i> cIdC CA c.1 A D E h' j h @ -i)
+-- (<i> cC CA c.1 D E (p@i) h)))
+-- ,p1)
+-- h2 : cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2)
+-- = (c.2.2.1
+-- ,<i>c.2.2.2@-i
+-- ,<_>c'.2.2.1)
+-- in <n> (isContrProp (cospanConeHom CA (F, (E, i), (C, l)) cc (B, k, g, cc2)) (pb2 cc) h1 h2 @ n).1
+-- ))
+
+-- p : Id U (cospanConeHom CA (F, (D, cC CA D E F h i), (C, l)) c' (A, j, cC CA A B C f g, cc3))
+-- (cospanConeHom CA (E, (D, h), (B, k)) c (A, j, f, cc1))
+-- = <i> (h : cH CA c.1 A)
+-- * (p : Id (cH CA c.1 D) (cC CA c.1 A D h j) c.2.1)
+-- * (p0 h p @ -i)
+-- in transport (<i> isContr (p@i)) (pb3 c')
projects / cubicaltt.git / commitdiff