Permalink
Fetching contributors…
Cannot retrieve contributors at this time
1240 lines (1136 sloc) 71 KB
-- Categories with structure identity principle
module category where
import sigma
import univalence
lemReflComp (A : U) (a b : A) (p : Path A a b) : Path (Path A a b) (compPath 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 ]
opaque lemReflComp
lemReflComp' (A : U) (a b : A) (p : Path A a b) : Path (Path A a b) (compPath A a b b p (<_> b)) p =
<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 : Path ((x : A) -> B x) f0 f1)
: Path (Path ((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
lemPathPProp (A B : U) (AProp : prop A) (p : Path U A B) : (x : A) -> (y : B) -> PathP p x y
= J U A (\(B : U) -> \(p : Path U A B) -> (x : A) -> (y : B) -> PathP p x y) AProp B p
opaque lemPathPProp
lemPathPSet (A B : U) (ASet : set A) (p : Path U A B) : (x : A) (y : B) (s t : PathP p x y) -> Path (PathP p x y) s t
= J U A (\(B : U) -> \(p : Path U A B) -> (x : A) (y : B) (s t : PathP p x y) -> Path (PathP p x y) s t) ASet B p
opaque lemPathPSet
lemPathPSet2 (A B : U) (ASet : set A) (p1 : Path U A B)
: (p2 : Path U A B) -> (p : Path (Path U A B) p1 p2) ->
(x : A) -> (y : B) -> (s : PathP p1 x y) -> (t : PathP p2 x y) -> PathP (<i> (PathP (p @ i) x y)) s t
= J (Path U A B) p1 (\(p2 : Path U A B) -> \(p : Path (Path U A B) p1 p2) -> (x : A) -> (y : B) -> (s : PathP p1 x y) -> (t : PathP p2 x y) -> PathP (<i> (PathP (p @ i) x y)) s t)
(lemPathPSet A B ASet p1)
opaque lemPathPSet2
substPathP (A B : U) (p : Path U A B) (x : A) (y : B) (q : Path B (transport p x) y) : PathP p x y
= transport (<i> PathP p x (q@i)) hole
where
hole : PathP p x (transport p x) = <i> comp (<j> p @ (i /\ j)) x [(i=0) -> <_> x]
opaque substPathP
transRefl (A : U) (a : A) : Path A (transport (<_> A) a) a = <i> comp (<_> A) a [(i=1) -> <_>a]
opaque transRefl
isContrProp (A : U) (p : isContr A) (x y : A) : Path A x y = compPath A x p.1 y (<i> p.2 x @ -i) (p.2 y)
opaque isContrProp
equivProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A) : equiv A B =
(F, isoToEquiv A B F G (\(y : B) -> BProp (F (G y)) y) (\(x : A) -> AProp (G (F x)) x))
opaque equivProp
idProp (A B : U) (AProp : prop A) (BProp : prop B) (F : A -> B) (G : B -> A) : Path U A B
= equivPath A B (equivProp A B AProp BProp F G).1 (equivProp A B AProp BProp F G).2
opaque idProp
lemTransEquiv (A B:U) (e:Path U A B) (x:A) : Path B (transport e x) ((transport (<i> equiv (e@-i) B) (idEquiv B)).1 x)
= <i> transRefl B (transport e x)@-i
opaque lemTransEquiv
--
categoryData : U = (A : U) * (A -> A -> U)
-- Propositional data of a precategory
isPrecategory2 (C : categoryData) (id : (x : C.1) -> C.2 x x) (c : (x y z : C.1) -> C.2 x y -> C.2 y z -> C.2 x z) : U
= let A : U = C.1
hom : A -> A -> U = C.2
in (homSet : (x y : A) -> set (hom x y))
* (cPathL : (x y : A) -> (f : hom x y) -> Path (hom x y) (c x x y (id x) f) f)
* (cPathR : (x y : A) -> (f : hom x y) -> Path (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) -> Path (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)))
propIsPrecategory2 (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)
: prop (isPrecategory2 C id c)
= let A : U = C.1; hom : A->A->U = C.2 in
propSig
((x y : A) -> set (hom x y))
(\(_:(x y : A) -> set (hom x y))->
((cPathL : (x y : A) -> (f : hom x y) -> Path (hom x y) (c x x y (id x) f) f)
* (cPathR : (x y : A) -> (f : hom x y) -> Path (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) -> Path (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)))))
(propPi A (\(x:A)->(y : A) -> set (hom x y))
(\(x:A)->propPi A (\(y : A) -> set (hom x y)) (\(y:A)->setIsProp (hom x y))))
(\(hset:(x y : A) -> set (hom x y))->
(propAnd
((x y : A) -> (f : hom x y) -> Path (hom x y) (c x x y (id x) f) f)
((cPathR : (x y : A) -> (f : hom x y) -> Path (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) -> Path (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))))
(propPi A (\(x:A)->(y : A) -> (f : hom x y) -> Path (hom x y) (c x x y (id x) f) f)
(\(x:A)->propPi A (\(y : A) -> (f : hom x y) -> Path (hom x y) (c x x y (id x) f) f)
(\(y:A)->propPi (hom x y) (\(f : hom x y) -> Path (hom x y) (c x x y (id x) f) f)
(\(f:hom x y)->hset x y (c x x y (id x) f) f))))
(propAnd
((x y : A) -> (f : hom x y) -> Path (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) -> Path (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)))
(propPi A (\(x:A)->(y : A) -> (f : hom x y) -> Path (hom x y) (c x y y f (id y)) f)
(\(x:A)->propPi A (\(y : A) -> (f : hom x y) -> Path (hom x y) (c x y y f (id y)) f)
(\(y:A)->propPi (hom x y) (\(f : hom x y) -> Path (hom x y) (c x y y f (id y)) f)
(\(f:hom x y)->hset x y (c x y y f (id y)) f))))
(propPi A (\(x:A)->(y z w : A) -> (f : hom x y) -> (g : hom y z) -> (h : hom z w) -> Path (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)))
(\(x:A)->propPi A (\(y:A)->(z w : A) -> (f : hom x y) -> (g : hom y z) -> (h : hom z w) -> Path (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)))
(\(y:A)->propPi A (\(z:A)->(w : A) -> (f : hom x y) -> (g : hom y z) -> (h : hom z w) -> Path (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)))
(\(z:A)->propPi A (\(w:A)-> (f : hom x y) -> (g : hom y z) -> (h : hom z w) -> Path (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)))
(\(w:A)->propPi (hom x y) (\(f : hom x y) -> (g : hom y z) -> (h : hom z w) -> Path (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)))
(\(f:hom x y)->propPi (hom y z) (\(g : hom y z) -> (h : hom z w) -> Path (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)))
(\(g:hom y z)->propPi (hom z w) (\(h : hom z w) -> Path (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)))
(\(h:hom z w)->hset x w (c x z w (c x y z f g) h) (c x y w f (c y z w g h)))))))))))))
isPrecategory (C : categoryData) : U =
let A : U = C.1
hom : A -> A -> U = C.2
in (id : (x : A) -> hom x x) * (c : (x y z : A) -> hom x y -> hom y z -> hom x z) * isPrecategory2 C id c
precategory : U = (C : categoryData) * isPrecategory C
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.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
cPath (C : precategory) (x : cA C) : cH C x x = C.2.1 x
cPathL (C : precategory) (x y : cA C) (f : cH C x y)
: Path (cH C x y) (cC C x x y (cPath C x) f) f = C.2.2.2.2.1 x y f
cPathR (C : precategory) (x y : cA C) (f : cH C x y)
: Path (cH C x y) (cC C x y y f (cPath C y)) f = C.2.2.2.2.2.1 x y f
cPathC (C : precategory) (x y z w : cA C) (f : cH C x y) (g : cH C y z) (h : cH C z w)
: Path (cH C x w) (cC C x z w (cC C x y z f g) h) (cC C x y w f (cC C y z w g h)) = C.2.2.2.2.2.2 x y z w f g h
--
-- Isomorphisms
--
iso (C : precategory) (A B : cA C) : U
= (f : cH C A B) * (g : cH C B A)
* (_ : Path (cH C A A) (cC C A B A f g) (cPath C A))
* (Path (cH C B B) (cC C B A B g f) (cPath C B))
isoEq (C : precategory) (A B : cA C) (f g : iso C A B) (p1 : Path (cH C A B) f.1 g.1) (p2 : Path (cH C B A) f.2.1 g.2.1)
: Path (iso C A B) f g
= <i> (p1@i,p2@i
,lemPathPProp (Path (cH C A A) (cC C A B A (p1@0) (p2@0)) (cPath C A))
(Path (cH C A A) (cC C A B A (p1@1) (p2@1)) (cPath C A))
(cHSet C A A (cC C A B A (p1@0) (p2@0)) (cPath C A))
(<i>Path (cH C A A) (cC C A B A (p1@i) (p2@i)) (cPath C A))
f.2.2.1 g.2.2.1 @ i
,lemPathPProp (Path (cH C B B) (cC C B A B (p2@0) (p1@0)) (cPath C B))
(Path (cH C B B) (cC C B A B (p2@1) (p1@1)) (cPath C B))
(cHSet C B B (cC C B A B (p2@0) (p1@0)) (cPath C B))
(<i>Path (cH C B B) (cC C B A B (p2@i) (p1@i)) (cPath C B))
f.2.2.2 g.2.2.2 @ i)
opaque isoEq
invIso (C : precategory) (A B : cA C) (f : iso C A B) : iso C B A = (f.2.1, f.1, f.2.2.2, f.2.2.1)
idIso (C : precategory) (A : cA C) : iso C A A = (cPath C A, cPath C A, cPathL C A A (cPath C A), cPathL C A A (cPath C A))
invIsoEquiv (C : precategory) (A B : cA C) : isEquiv (iso C A B) (iso C B A) (invIso C A B)
= isoToEquiv (iso C A B) (iso C B A) (invIso C A B) (invIso C B A) (\(x : iso C B A) -> <_> x) (\(x : iso C A B) -> <_> x)
invIsoEq (C : precategory) (A B : cA C) : Path U (iso C A B) (iso C B A)
= equivPath (iso C A B) (iso C B A) (invIso C A B) (invIsoEquiv C A B)
compIsoHelper (X : precategory) (A B C : cA X) (f : iso X A B) (g : iso X B C)
: Path (cH X A A) (cC X A C A (cC X A B C f.1 g.1) (cC X C B A g.2.1 f.2.1)) (cPath X A)
= compPath (cH X A A)
(cC X A C A (cC X A B C f.1 g.1) (cC X C B A g.2.1 f.2.1))
(cC X A B A f.1 (cC X B C A g.1 (cC X C B A g.2.1 f.2.1)))
(cPath X A)
(cPathC X A B C A f.1 g.1 (cC X C B A g.2.1 f.2.1))
(compPath (cH X A A)
(cC X A B A f.1 (cC X B C A g.1 (cC X C B A g.2.1 f.2.1)))
(cC X A B A f.1 (cC X B B A (cC X B C B g.1 g.2.1) f.2.1))
(cPath X A)
(<i>cC X A B A f.1 (cPathC X B C B A g.1 g.2.1 f.2.1 @ -i))
(compPath (cH X A A)
(cC X A B A f.1 (cC X B B A (cC X B C B g.1 g.2.1) f.2.1))
(cC X A B A f.1 (cC X B B A (cPath X B) f.2.1))
(cPath X A)
(<i>cC X A B A f.1 (cC X B B A (g.2.2.1 @ i) f.2.1))
(compPath (cH X A A)
(cC X A B A f.1 (cC X B B A (cPath X B) f.2.1))
(cC X A B A f.1 f.2.1)
(cPath X A)
(<i>cC X A B A f.1 (cPathL X B A f.2.1 @ i))
f.2.2.1)))
opaque compIsoHelper
compIso (X : precategory) (A B C : cA X) (f : iso X A B) (g : iso X B C) : iso X A C
= (cC X A B C f.1 g.1, cC X C B A g.2.1 f.2.1
,compIsoHelper X A B C f g
,compIsoHelper X C B A (invIso X B C g) (invIso X A B f))
PathLIso (C : precategory) (A B : cA C) (f : iso C A B) : Path (iso C A B) (compIso C A A B (idIso C A) f) f
= isoEq C A B (compIso C A A B (idIso C A) f) f (cPathL C A B f.1) (cPathR C B A f.2.1)
opaque PathLIso
PathRIso (C : precategory) (A B : cA C) (f : iso C A B) : Path (iso C A B) (compIso C A B B f (idIso C B)) f
= isoEq C A B (compIso C A B B f (idIso C B)) f (cPathR C A B f.1) (cPathL C B A f.2.1)
opaque PathRIso
PathCIso (X : precategory) (A B C D : cA X) (f : iso X A B) (g : iso X B C) (h : iso X C D)
: Path (iso X A D) (compIso X A C D (compIso X A B C f g) h) (compIso X A B D f (compIso X B C D g h))
= isoEq X A D (compIso X A C D (compIso X A B C f g) h) (compIso X A B D f (compIso X B C D g h))
(cPathC X A B C D f.1 g.1 h.1) (<i>cPathC X D C B A h.2.1 g.2.1 f.2.1@-i)
opaque PathCIso
PathInvLIso (X : precategory) (A B : cA X) (f : iso X A B) : Path (iso X B B) (compIso X B A B (invIso X A B f) f) (idIso X B)
= isoEq X B B (compIso X B A B (invIso X A B f) f) (idIso X B) f.2.2.2 f.2.2.2
opaque PathInvLIso
opaque compIso
--
-- Categories
--
eqToIso (C : precategory) (A B : cA C) (p : Path (cA C) A B) : iso C A B
= J (cA C) A (\(B : cA C) -> \(p : Path (cA C) A B) -> iso C A B) (idIso C A) B p
isCategory (C : precategory) : U = (A : cA C) -> isContr ((B : cA C) * iso C A B)
propIsCategory (C : precategory) : prop (isCategory C)
= propPi (cA C) (\(A : cA C) -> isContr ((B : cA C) * iso C A B))
(\(A : cA C) -> propIsContr ((B : cA C) * iso C A B))
category : U = (C:precategory)*isCategory C
lemIsCategory (C : precategory) (isC : isCategory C) (A B : cA C) (e : iso C A B) : Path ((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 (Path (cA C) A B) (iso C A B) (eqToIso C A B)
= equivFunFib (cA C) (Path (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) : Path U (Path (cA C) A B) (iso C A B)
= equivPath (Path (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
--
-- the structure identity principle
--
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 (cPath 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
sHPath (X : precategory) (S : structure X) : (x : cA X) -> (a : sP X S x) -> sH X S x x a a (cPath 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 (cPath X x) -> sH X S x x b a (cPath X x) ->
Path (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 = (cPath C X.1, sHPath 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) : Path (hom x y) (cmp x x y (id x) f) f
= <i> (cPathL C x.1 y.1 f.1 @ i
,lemPathPProp (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 (cPathL 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) : Path (hom x y) (cmp x y y f (id y)) f
= <i> (cPathR C x.1 y.1 f.1 @ i
,lemPathPProp (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 (cPathR 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) : Path (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> (cPathC C x.1 y.1 z.1 w.1 f.1 g.1 h.1 @ i
,lemPathPProp (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 (cPathC 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) : Path A x y = compPath 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)
-- The structure identity principle for categories
sip (X : precategory) (isC : isCategory X) (S : structure X) (isS : isStandardStructure X S) : isCategory (sipPrecategory X S)
= hole
where
D : precategory = sipPrecategory X S
eq1 (A : cA D)
: Path 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)
= isoPath
((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
,lemPathPProp (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 (cPath 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)
(sHPath X S A.1 A.2) @ i)
, <i> (C.1.2.2.2.2 @ i
,lemPathPProp (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 (cPath 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)
(sHPath 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))
: Path ((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) : Path ((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
,lemPathPSet (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 (cPath 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)
(sHPath 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
,lemPathPSet (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 (cPath 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)
(sHPath 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 : Path ((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,sHPath X S A.1 A.2,sHPath X S A.1 A.2)
,\(Y : (B2 : sP X S A.1) * (_ : sH X S A.1 A.1 A.2 B2 (cPath X A.1)) * sH X S A.1 A.1 B2 A.2 (cPath X A.1)) ->
<i> (isS A.1 A.2 Y.1 Y.2.1 Y.2.2 @ i
,lemPathPProp (sH X S A.1 A.1 A.2 A.2 (cPath X A.1))
(sH X S A.1 A.1 A.2 Y.1 (cPath X A.1))
(sHProp X S A.1 A.1 A.2 A.2 (cPath 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) (cPath X A.1))
(sHPath X S A.1 A.2) Y.2.1 @ i
,lemPathPProp (sH X S A.1 A.1 A.2 A.2 (cPath X A.1))
(sH X S A.1 A.1 Y.1 A.2 (cPath X A.1))
(sHProp X S A.1 A.1 A.2 A.2 (cPath 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 (cPath X A.1))
(sHPath 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)
opaque sip
--
-- Functors
--
-- TODO: define as functor_data and isFunctor
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) -> Path (cH B (Fob x) (Fob x)) (Fmor x x (cPath A x)) (cPath B (Fob x)))
* ((x y z : cA A) -> (f : cH A x y) -> (g : cH A y z) -> Path (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) -> <_> cPath 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) -> compPath (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 (cPath A x)))
(G.2.1 (F.1 x) (F.1 x) (cPath B (F.1 x)))
(cPath 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) ->
compPath (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)
: Path U (cH A a b) (cH B (F.1 a) (F.1 b))
= equivPath (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 : Path A (e.2 x).1.1 (e.2 y).1.1) : Path B x y
= transport
(compPath U (Path B (e.1 (e.2 x).1.1) (e.1 (e.2 y).1.1)) (Path B x (e.1 (e.2 y).1.1)) (Path B x y)
(<i> Path B (retEq A B e x @ i) (e.1 (e.2 y).1.1)) (<i> Path 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 : Path B (e.1 x) (e.1 y)) : Path A x y
= transport
(compPath U (Path A (e.2 (e.1 x)).1.1 (e.2 (e.1 y)).1.1) (Path A x (e.2 (e.1 y)).1.1) (Path A x y)
(<i> Path A (secEq A B e x @ i) (e.2 (e.1 y)).1.1) (<i> Path 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)
: Path U (iso A x y) (iso B (F.1 x) (F.1 y))
= hole
where
F0 (f : iso A x y) : iso B (F.1 x) (F.1 y)
= (F.2.1 x y f.1, F.2.1 y x f.2.1
,compPath (cH B (F.1 x) (F.1 x))
(cC B (F.1 x) (F.1 y) (F.1 x) (F.2.1 x y f.1) (F.2.1 y x f.2.1))
(F.2.1 x x (cC A x y x f.1 f.2.1))
(cPath B (F.1 x))
(<i>F.2.2.2 x y x f.1 f.2.1 @-i)
(compPath (cH B (F.1 x) (F.1 x))
(F.2.1 x x (cC A x y x f.1 f.2.1))
(F.2.1 x x (cPath A x))
(cPath B (F.1 x))
(<i>F.2.1 x x (f.2.2.1@i))
(F.2.2.1 x))
,compPath (cH B (F.1 y) (F.1 y))
(cC B (F.1 y) (F.1 x) (F.1 y) (F.2.1 y x f.2.1) (F.2.1 x y f.1))
(F.2.1 y y (cC A y x y f.2.1 f.1))
(cPath B (F.1 y))
(<i>F.2.2.2 y x y f.2.1 f.1 @-i)
(compPath (cH B (F.1 y) (F.1 y))
(F.2.1 y y (cC A y x y f.2.1 f.1))
(F.2.1 y y (cPath A y))
(cPath B (F.1 y))
(<i>F.2.1 y y (f.2.2.2@i))
(F.2.2.1 y)))
G0 (g : iso B (F.1 x) (F.1 y)) : iso A x y
= ((ff x y g.1).1.1
,(ff y x g.2.1).1.1
,lem10' (cH A x x) (cH B (F.1 x) (F.1 x)) (F.2.1 x x, ff x x) (cC A x y x (ff x y g.1).1.1 (ff y x g.2.1).1.1) (cPath A x)
(compPath (cH B (F.1 x) (F.1 x))
(F.2.1 x x (cC A x y x (ff x y g.1).1.1 (ff y x g.2.1).1.1))
(cC B (F.1 x) (F.1 y) (F.1 x) (F.2.1 x y (ff x y g.1).1.1) (F.2.1 y x (ff y x g.2.1).1.1))
(F.2.1 x x (cPath A x))
(F.2.2.2 x y x (ff x y g.1).1.1 (ff y x g.2.1).1.1)
(compPath (cH B (F.1 x) (F.1 x))
(cC B (F.1 x) (F.1 y) (F.1 x) (F.2.1 x y (ff x y g.1).1.1) (F.2.1 y x (ff y x g.2.1).1.1))
(cC B (F.1 x) (F.1 y) (F.1 x) g.1 g.2.1)
(F.2.1 x x (cPath A x))
(<i>cC B (F.1 x) (F.1 y) (F.1 x) ((ff x y g.1).1.2@-i) ((ff y x g.2.1).1.2@-i))
(compPath (cH B (F.1 x) (F.1 x))
(cC B (F.1 x) (F.1 y) (F.1 x) g.1 g.2.1)
(cPath B (F.1 x))
(F.2.1 x x (cPath A x))
g.2.2.1
(<i>F.2.2.1 x @ -i))))
,lem10' (cH A y y) (cH B (F.1 y) (F.1 y)) (F.2.1 y y, ff y y) (cC A y x y (ff y x g.2.1).1.1 (ff x y g.1).1.1) (cPath A y)
(compPath (cH B (F.1 y) (F.1 y))
(F.2.1 y y (cC A y x y (ff y x g.2.1).1.1 (ff x y g.1).1.1))
(cC B (F.1 y) (F.1 x) (F.1 y) (F.2.1 y x (ff y x g.2.1).1.1) (F.2.1 x y (ff x y g.1).1.1))
(F.2.1 y y (cPath A y))
(F.2.2.2 y x y (ff y x g.2.1).1.1 (ff x y g.1).1.1)
(compPath (cH B (F.1 y) (F.1 y))
(cC B (F.1 y) (F.1 x) (F.1 y) (F.2.1 y x (ff y x g.2.1).1.1) (F.2.1 x y (ff x y g.1).1.1))
(cC B (F.1 y) (F.1 x) (F.1 y) g.2.1 g.1)
(F.2.1 y y (cPath A y))
(<i>cC B (F.1 y) (F.1 x) (F.1 y) ((ff y x g.2.1).1.2@-i) ((ff x y g.1).1.2@-i))
(compPath (cH B (F.1 y) (F.1 y))
(cC B (F.1 y) (F.1 x) (F.1 y) g.2.1 g.1)
(cPath B (F.1 y))
(F.2.1 y y (cPath A y))
g.2.2.2
(<i>F.2.2.1 y @ -i))))
)
FG (g : iso B (F.1 x) (F.1 y)) : Path (iso B (F.1 x) (F.1 y)) (F0 (G0 g)) g
= isoEq B (F.1 x) (F.1 y) (F0 (G0 g)) g
(<i>(ff x y g.1).1.2@-i) (<i>(ff y x g.2.1).1.2@-i)
GF (f : iso A x y) : Path (iso A x y) (G0 (F0 f)) f
= isoEq A x y (G0 (F0 f)) f
(<i> ((ff x y (F.2.1 x y f.1)).2 (f.1,<j>F.2.1 x y f.1)@i).1)
(<i> ((ff y x (F.2.1 y x f.2.1)).2 (f.2.1,<j>F.2.1 y x f.2.1)@i).1)
hole : Path U (iso A x y) (iso B (F.1 x) (F.1 y)) = isoPath (iso A x y) (iso B (F.1 x) (F.1 y)) F0 G0 FG GF
opaque lemFF
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) : Path U (iso A x y) (iso B (F.1 x) (F.1 y))
= lemFF A B F p1 x y
hole : isContr ((y : cA A) * iso B (F.1 x) (F.1 y))
= transport (<i> isContr ((y : cA A) * (hole2 y @ i))) (isC x)
opaque F12
F23 (A B : precategory) (F : functor A B) (p2 : (x : cA A) -> isContr ((y : cA A) * iso B (F.1 y) (F.1 x)))
(x : cA B)
(a b : (y : cA A) * iso B (F.1 y) x) : Path ((y : cA A) * iso B (F.1 y) x) a b
= transport p hole3
where
hole2 : Path ((y : cA A) * iso B (F.1 y) (F.1 a.1))
(a.1, idIso B (F.1 a.1)) (b.1, compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2))
= isContrProp ((y : cA A) * iso B (F.1 y) (F.1 a.1)) (p2 a.1)
(a.1, idIso B (F.1 a.1)) (b.1, compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2))
opaque hole2
hole3 : Path ((y : cA A) * iso B (F.1 y) x)
(a.1, compIso B (F.1 a.1) (F.1 a.1) x (idIso B (F.1 a.1)) a.2)
(b.1, compIso B (F.1 b.1) (F.1 a.1) x (compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2)) a.2)
= <i> ((hole2@i).1, compIso B (F.1 (hole2@i).1) (F.1 a.1) x (hole2@i).2 a.2)
opaque hole3
p : Path U (Path ((y : cA A) * iso B (F.1 y) x)
(a.1, compIso B (F.1 a.1) (F.1 a.1) x (idIso B (F.1 a.1)) a.2)
(b.1, compIso B (F.1 b.1) (F.1 a.1) x (compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2)) a.2))
(Path ((y : cA A) * iso B (F.1 y) x) a b)
= (<i>Path ((y : cA A) * iso B (F.1 y) x)
(a.1, PathLIso B (F.1 a.1) x a.2 @ i)
(b.1, compPath (iso B (F.1 b.1) x)
(compIso B (F.1 b.1) (F.1 a.1) x (compIso B (F.1 b.1) x (F.1 a.1) b.2 (invIso B (F.1 a.1) x a.2)) a.2)
(compIso B (F.1 b.1) x x b.2 (compIso B x (F.1 a.1) x (invIso B (F.1 a.1) x a.2) a.2))
b.2
(PathCIso B (F.1 b.1) x (F.1 a.1) x b.2 (invIso B (F.1 a.1) x a.2) a.2)
(compPath (iso B (F.1 b.1) x)
(compIso B (F.1 b.1) x x b.2 (compIso B x (F.1 a.1) x (invIso B (F.1 a.1) x a.2) a.2))
(compIso B (F.1 b.1) x x b.2 (idIso B x))
b.2
(<i>compIso B (F.1 b.1) x x b.2 (PathInvLIso B (F.1 a.1) x a.2 @ i))
(PathRIso B (F.1 b.1) x b.2))
@ i))
opaque F23
--
-- 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))
catPathIsEquiv (A : precategory) : catIsEquiv A A (idFunctor A)
= (\(a b : cA A) -> idIsEquiv (cH A a b)
,\(b:cA A) -> (b, idIso A b))
catPathEquiv (A : precategory) : catEquiv A A = (idFunctor A, catPathIsEquiv A)
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 : Path U (cA A) (cA B))
* (e2 : PathP (<i>(x y : e1@i)->U) (cH A) (cH B))
* (_ : PathP (<i> (x:e1@i)->(e2@i) x x) (cPath A) (cPath B))
* (PathP (<i> (x y z:e1@i)->(e2@i) x y->(e2@i) y z->(e2@i) x z) (cC A) (cC B))
eCatIso3 (A B : precategory) : Path U (Path precategory A B) (catIso3 A B)
= isoPath (Path precategory A B) (catIso3 A B)
F G FG GF
where
F (e:Path precategory A B):catIso3 A B = (<i>(e@i).1.1, <i>(e@i).1.2, <i>(e@i).2.1, <i>(e@i).2.2.1)
G (e:catIso3 A B):Path precategory A B = <i> ((e.1@i, e.2.1@i), e.2.2.1@i, e.2.2.2@i
,lemPathPProp (isPrecategory2 A.1 A.2.1 A.2.2.1)
(isPrecategory2 B.1 B.2.1 B.2.2.1)
(propIsPrecategory2 A.1 A.2.1 A.2.2.1)
(<i>isPrecategory2 (e.1@i, e.2.1@i) (e.2.2.1@i) (e.2.2.2@i))
A.2.2.2 B.2.2.2 @ i)
FG(e:catIso3 A B):Path (catIso3 A B) (F (G e)) e=<_>e
GF(e:Path precategory A B):Path (Path precategory A B) (G (F e)) e
=<i j>((e@j).1, (e@j).2.1, (e@j).2.2.1
,lemPathPSet (isPrecategory2 A.1 A.2.1 A.2.2.1)
(isPrecategory2 B.1 B.2.1 B.2.2.1)
(propSet (isPrecategory2 A.1 A.2.1 A.2.2.1) (propIsPrecategory2 A.1 A.2.1 A.2.2.1))
(<i>isPrecategory2 (e@i).1 (e@i).2.1 (e@i).2.2.1)
A.2.2.2 B.2.2.2
(<j> (G (F e)@j).2.2.2) (<j>(e@j).2.2.2)
@ i @ j)
catIso30 (A B : precategory) : U = (e1 : Path U (cA A) (cA B))
* (e2 : Path ((x y : cA A)->U) (cH A) (\(x y:cA A)->cH B (transport e1 x) (transport e1 y)))
* (_ : Path ((x:cA A)->cH A x x)
(cPath A)
(\(x : cA A) -> transport (<j>(e2@-j) x x) (cPath B (transport e1 x))))
* (Path ((x y z:cA A)->cH A x y->cH A y z->cH A x z)
(\(x y z:cA A)(f:cH A x y)(g:cH A y z)->cC A x y z f g)
(\(x y z:cA A)(f:cH A x y)(g:cH A y z)->
transport (<i>(e2@-i) x z)
(cC B (transport e1 x) (transport e1 y) (transport e1 z)
(transport (<i>(e2@i) x y) f)
(transport (<i>(e2@i) y z) g))))
eCatIso30 (A B : precategory) : Path U (catIso3 A B) (catIso30 A B)
= <i> (e1 : Path U (cA A) (cA B))
* (let e21 : (x y : e1@-i) -> U
= comp (<_> (x y : e1@-i) -> U)
(\(x y : e1@-i) -> cH B (transport (<j>e1@-i\/j) x) (transport (<j>e1@-i\/j) y))
[(i=1)-><_>\(x y:cA A) -> cH B (transport e1 x) (transport e1 y)
,(i=0)-><j>\(x y:cA B) -> cH B (transRefl (cA B) x @ j) (transRefl (cA B) y @ j)
]
f21 : Path ((x y : e1@-i) -> U)
(\(x y : e1@-i) -> cH B (transport (<j>e1@-i\/j) x) (transport (<j>e1@-i\/j) y))
e21
= fill (<_> (x y : e1@-i) -> U)
(\(x y : e1@-i) -> cH B (transport (<j>e1@-i\/j) x) (transport (<j>e1@-i\/j) y))
[(i=1)-><_>\(x y:cA A) -> cH B (transport e1 x) (transport e1 y)
,(i=0)-><j>\(x y:cA B) -> cH B (transRefl (cA B) x @ j) (transRefl (cA B) y @ j)
]
in
(e2 : PathP (<j> (x y : e1@j/\-i) -> U) (cH A) e21)
* (_ : PathP (<j> (x : e1@j/\-i) -> (e2@j/\-i) x x)
(cPath A)
(comp (<_> (x:e1@-i)->(e2@-i) x x)
(\(x : e1@-i) -> transport (<j>(e2@-i\/-j) x x) (transport (<j>(f21@j) x x) (cPath B (transport (<j>e1@-i\/j) x))))
[(i=1)-><j>\(x:cA A) -> transport (<j>(e2@-j) x x) (transRefl ((f21@0) x x) (cPath B (transport e1 x)) @ j)
,(i=0)-><j>\(x:cA B) ->
transRefl ((e2@1) x x)
(compPath (cH B x x)
(transport (<k>cH B (transRefl (cA B) x@k) (transRefl (cA B) x@k))
(cPath B (transport (<_> cA B) x)))
(transport (<_>cH B x x) (cPath B x))
(cPath B x)
(<j>transport (<k>cH B (transRefl (cA B) x@j\/k) (transRefl (cA B) x@j\/k))
(cPath B (transRefl (cA B) x @ j)))
(transRefl (cH B x x) (cPath B x))
@ j) @ j
]))
* (PathP (<j> (x y z : e1@j/\-i) (f : (e2@j/\-i) x y) (g : (e2@j/\-i) y z) -> (e2@j/\-i) x z)
(cC A)
(comp (<_> (x y z : e1@-i) (f : (e2@-i) x y) (g : (e2@-i) y z) -> (e2@-i) x z)
(\(x y z : e1@-i) (f : (e2@-i) x y) (g : (e2@-i) y z) ->
transport (<j>(e2@-i\/-j) x z) (transport (<j>(f21@j) x z)
(cC B (transport (<j>e1@-i\/j) x) (transport (<j>e1@-i\/j) y) (transport (<j>e1@-i\/j) z)
(transport (<j>(f21@-j) x y) (transport (<j>(e2@-i\/j) x y) f))
(transport (<j>(f21@-j) y z) (transport (<j>(e2@-i\/j) y z) g)))))
[(i=1)-><j>\(x y z : cA A) (f : cH A x y) (g : cH A y z) ->
transport (<j>(e2@-j) x z) (transRefl ((f21@0) x z)
(cC B (transport e1 x) (transport e1 y) (transport e1 z)
(transRefl ((f21@0) x y) (transport (<j>(e2@j) x y) f) @ j)
(transRefl ((f21@0) y z) (transport (<j>(e2@j) y z) g) @ j)) @ j)
,(i=0)-><j>\(x y z : cA B) (f : cH B x y) (g : cH B y z) ->
transRefl ((e2@1) x z)
(compPath (cH B x z)
(transport (<k>cH B (transRefl (cA B) x@k) (transRefl (cA B) z@k))
(cC B (transport (<_>cA B) x) (transport (<_>cA B) y) (transport (<_>cA B) z)
(transport (<k>cH B (transRefl (cA B) x@-k) (transRefl (cA B) y@-k)) (transport (<j>(e2@1) x y) f))
(transport (<k>cH B (transRefl (cA B) y@-k) (transRefl (cA B) z@-k)) (transport (<j>(e2@1) y z) g))))
(transport (<_>cH B x z)
(cC B x y z
(transport (<_>cH B x y) f)
(transport (<_>cH B y z) g)))
(cC B x y z f g)
(<j>transport (<k>cH B (transRefl (cA B) x@j\/k) (transRefl (cA B) z@j\/k))
(cC B (transRefl (cA B) x@j) (transRefl (cA B) y@j) (transRefl (cA B) z@j)
(transport (<k>cH B (transRefl (cA B) x@j\/-k) (transRefl (cA B) y@j\/-k)) (transRefl ((e2@1) x y) f@j))
(transport (<k>cH B (transRefl (cA B) y@j\/-k) (transRefl (cA B) z@j\/-k)) (transRefl ((e2@1) y z) g@j))))
(<j>transRefl (cH B x z) (cC B x y z (transRefl (cH B x y) f @ j) (transRefl (cH B y z) g @ j)) @ j)
@ j) @ j
])))
catIso311 (A B : precategory) (e1:Path U (cA A) (cA B)) : U
= Path ((x y : cA A)->U) (cH A) (\(x y:cA A)->cH B (transport e1 x) (transport e1 y))
catIso312 (A B : precategory) (e1:Path U (cA A) (cA B)) (e2:catIso311 A B e1) : U
= Path ((x:cA A)->cH B (transport e1 x) (transport e1 x))
(\(x:cA A)->transport (<i> (e2@i) x x) (cPath A x))
(\(x : cA A) -> cPath B (transport e1 x))
catIso313 (A B : precategory) (e1:Path U (cA A) (cA B)) (e2:catIso311 A B e1) : U
= Path ((x y z:cA A)->cH A x y->cH A y z->cH B (transport e1 x) (transport e1 z))
(\(x y z:cA A)(f:cH A x y)(g:cH A y z)->transport (<i>(e2@i)x z) (cC A x y z f g))
(\(x y z:cA A)(f:cH A x y)(g:cH A y z)->
cC B (transport e1 x) (transport e1 y) (transport e1 z)
(transport (<i>(e2@i) x y) f)
(transport (<i>(e2@i) y z) g))
catIso31 (A B : precategory) : U = (e1 : Path U (cA A) (cA B))
* (e2 : catIso311 A B e1)
* (_ : catIso312 A B e1 e2)
* ( catIso313 A B e1 e2)
eCatIso31 (A B : precategory) : Path U (catIso30 A B) (catIso31 A B)
= <i> (e1 : Path U (cA A) (cA B))
* (e2 : Path ((x y : cA A)->U) (cH A) (\(x y:cA A)->cH B (transport e1 x) (transport e1 y)))
* (_:comp (<_> U)
(Path ((x:cA A)->(e2@i) x x)
(\(x:cA A)->transport (<j> (e2@i/\j) x x) (cPath A x))
(\(x:cA A)->transport (<j> (e2@i\/-j) x x) (cPath B (transport e1 x))))
[(i=0)-><k>Path ((x:cA A)->cH A x x)
(\(x:cA A)->transRefl (cH A x x) (cPath A x) @ k)
(\(x:cA A)->transport (<j> (e2@-j) x x) (cPath B (transport e1 x)))
,(i=1)-><k>Path ((x:cA A)->(e2@i) x x)
(\(x:cA A)->transport (<j> (e2@j) x x) (cPath A x))
(\(x:cA A)->transRefl ((e2@1) x x) (cPath B (transport e1 x)) @ k)
])
* (comp (<_> U)
(Path ((x y z:cA A)->cH A x y->cH A y z->(e2@i) x z)
(\(x y z:cA A)(f:cH A x y)(g:cH A y z)->
transport (<j> (e2@i/\j) x z) (cC A x y z f g))
(\(x y z:cA A)(f:cH A x y)(g:cH A y z)->
transport (<j>(e2@i\/-j) x z)
(cC B (transport e1 x) (transport e1 y) (transport e1 z)
(transport (<j>(e2@j) x y) f)
(transport (<j>(e2@j) y z) g))))
[(i=0)-><k>Path ((x y z:cA A)->cH A x y->cH A y z->cH A x z)
(\(x y z:cA A)(f:cH A x y)(g:cH A y z)->
transRefl ((e2@0) x z) (cC A x y z f g) @ k)
(\(x y z:cA A)(f:cH A x y)(g:cH A y z)->
transport (<j>(e2@-j) x z)
(cC B (transport e1 x) (transport e1 y) (transport e1 z)
(transport (<j>(e2@j) x y) f)
(transport (<j>(e2@j) y z) g)))
,(i=1)-><k>Path ((x y z:cA A)->cH A x y->cH A y z->(e2@1) x z)
(\(x y z:cA A)(f:cH A x y)(g:cH A y z)->
transport (<j>(e2@j) x z) (cC A x y z f g))
(\(x y z:cA A)(f:cH A x y)(g:cH A y z)->
transRefl ((e2@1) x z)
(cC B (transport e1 x) (transport e1 y) (transport e1 z)
(transport (<j>(e2@j) x y) f)
(transport (<j>(e2@j) y z) g)) @ k)
])
lemEquivCoh (A B:U) (e:equiv A B) (x:A)
: Path (Path B (e.1 x) (e.1 (invEq A B e (e.1 x))))
(<j>e.1(secEq A B e x@-j))
(<j>retEq A B e (e.1 x)@-j)
= <i> comp (<j> Path B (e.1 x) (e.1 (secEq A B e x @ -i /\ -j)))
(((e.2 (e.1 x)).2 (x,<_>e.1 x)@-i).2)
[(i=0)-><j><k>e.1 (secEq A B e x@-k\/-j)
,(i=1)-><j><k>retEq A B e (e.1 x)@-k
]
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, isoToEquiv (Sigma A B) (Sigma A' B') F G FG GF)
where
F (x:Sigma A B):Sigma A' B' = (e.1 x.1, (f x.1).1 x.2)
G (x:Sigma A' B'):Sigma A B = ((e.2 x.1).1.1, ((f (e.2 x.1).1.1).2 (transport (<i> B' ((e.2 x.1).1.2 @ i)) x.2)).1.1)
FG (x:Sigma A' B'):Path (Sigma A' B') (F (G x)) x
= <i> ((e.2 x.1).1.2 @ -i
,comp (<_> B' ((e.2 x.1).1.2 @ -i))
(transport (<j> B' ((e.2 x.1).1.2 @ j/\-i)) x.2)
[(i=0)-><j>((f (e.2 x.1).1.1).2 (transport (<i> B' ((e.2 x.1).1.2 @ i)) x.2)).1.2 @ j
,(i=1)-><j>transRefl (B' ((e.2 x.1).1.2 @ 0)) x.2@j
])
GF (x:Sigma A B):Path (Sigma A B) (G (F x)) x
= <i> (secEq A A' e x.1 @ i
,comp (<_> B (secEq A A' e x.1 @ i))
((f (secEq A A' e x.1 @ i)).2 (transport (<j> B' (e.1 (secEq A A' e x.1 @ i\/-j))) ((f x.1).1 x.2))).1.1
[(i=0)-><k>((f (secEq A A' e x.1 @ 0)).2 (transport (<i> B' (lemEquivCoh A A' e x.1@k@i)) ((f x.1).1 x.2))).1.1
,(i=1)-><k>compPath (B x.1)
((f x.1).2 (transport (<j> B' (e.1 x.1)) ((f x.1).1 x.2))).1.1
((f x.1).2 ((f x.1).1 x.2)).1.1
x.2
(<k>((f x.1).2 (transRefl (B' (e.1 x.1)) ((f x.1).1 x.2)@k)).1.1)
(secEq (B x.1) (B' (e.1 x.1)) (f x.1) x.2) @ k
])
sigEquivLem' (A A':U) (B:A->U) (B':A'->U)
(e:equiv A A')
(f:(x:A)->Path U (B x) (B' (e.1 x)))
: Path U (Sigma A B) (Sigma A' B')
= transEquivToPath (Sigma A B) (Sigma A' B') (sigEquivLem A A' B B' e (\(x:A)->transEquiv' (B' (e.1 x)) (B x) (f x)))
catIso321 (A B : precategory) (e1:Path U (cA A) (cA B)) : U
= (x y:cA A) -> Path U (cH A x y) (cH B (transport e1 x) (transport e1 y))
catIso322 (A B : precategory) (e1:Path U (cA A) (cA B)) (e2:catIso321 A B e1) : U
= (x:cA A) -> Path (cH B (transport e1 x) (transport e1 x))
(transport (e2 x x) (cPath A x))
(cPath B (transport e1 x))
catIso323 (A B : precategory) (e1:Path U (cA A) (cA B)) (e2:catIso321 A B e1) : U
= (x y z:cA A)(f:cH A x y)(g:cH A y z)->
Path (cH B (transport e1 x) (transport e1 z))
(transport (e2 x z) (cC A x y z f g))
(cC B (transport e1 x) (transport e1 y) (transport e1 z)
(transport (e2 x y) f)
(transport (e2 y z) g))
catIso32 (A B : precategory) : U = (e1 : Path U (cA A) (cA B))
* (e2 : catIso321 A B e1)
* (_ : catIso322 A B e1 e2)
* ( catIso323 A B e1 e2)
eCatIso32 (A B : precategory) : Path U (catIso31 A B) (catIso32 A B)
= <i> (e1 : Path U (cA A) (cA B))
* (let F(e2:catIso311 A B e1):catIso321 A B e1 = \(x y:cA A)-><i>(e2@i) x y in
transEquivToPath
((e2 : catIso311 A B e1) * (_ : catIso312 A B e1 e2) * ( catIso313 A B e1 e2))
((e2 : catIso321 A B e1) * (_ : catIso322 A B e1 e2) * ( catIso323 A B e1 e2))
(sigEquivLem (catIso311 A B e1) (catIso321 A B e1)
(\(e2 : catIso311 A B e1) -> (_ : catIso312 A B e1 e2) * ( catIso313 A B e1 e2))
(\(e2 : catIso321 A B e1) -> (_ : catIso322 A B e1 e2) * ( catIso323 A B e1 e2))
(F, isoToEquiv (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, isoToEquiv (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, isoToEquiv (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))
catIso22 (A B : precategory) (e1:equiv (cA A) (cA B)) (e2:catIso21 A B e1) : U
= (x:cA A) -> Path (cH B (e1.1 x) (e1.1 x))
((e2 x x).1 (cPath A x))
(cPath B (e1.1 x))
catIso23 (A B : precategory) (e1:equiv (cA A) (cA B)) (e2:catIso21 A B e1) : U
= (x y z:cA A)(f:cH A x y)(g:cH A y z)->
Path (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))
catIso2 (A B : precategory) : U = (e1 : equiv (cA A) (cA B))
* (e2 : catIso21 A B e1)
* (_ : catIso22 A B e1 e2)
* ( catIso23 A B e1 e2)
eCatIso (A B : precategory) : Path U (catIso A B) (catIso2 A B)
= transEquivToPath (catIso A B) (catIso2 A B)
(F, isoToEquiv (catIso A B) (catIso2 A B) F G (\(e:catIso2 A B)-><_>e) (\(e:catIso A B)-><_>e))
where
F(e:catIso A B):catIso2 A B=((e.1.1, e.2.2),\(x y:cA A)->(e.1.2.1 x y, e.2.1 x y),e.1.2.2.1,e.1.2.2.2)
G(e:catIso2 A B):catIso A B=((e.1.1,\(x y:cA A)->(e.2.1 x y).1,e.2.2.1,e.2.2.2),\(x y:cA A)->(e.2.1 x y).2,e.1.2)
catIso21' (A B : precategory) (e1:Path U (cA A) (cA B)) : U
= (x y:cA A) -> equiv (cH A x y) (cH B (transport e1 x) (transport e1 y))
catIso22' (A B : precategory) (e1:Path U (cA A) (cA B)) (e2:catIso21' A B e1) : U
= (x:cA A) -> Path (cH B (transport e1 x) (transport e1 x))
((e2 x x).1 (cPath A x))
(cPath B (transport e1 x))
catIso23' (A B : precategory) (e1:Path U (cA A) (cA B)) (e2:catIso21' A B e1) : U
= (x y z:cA A)(f:cH A x y)(g:cH A y z)->
Path (cH B (transport e1 x) (transport e1 z))
((e2 x z).1 (cC A x y z f g))
(cC B (transport e1 x) (transport e1 y) (transport e1 z) ((e2 x y).1 f) ((e2 y z).1 g))
equivPi (A:U) (B0 B1:A->U) (e:(a:A)->equiv (B0 a) (B1 a)) : equiv ((a:A)->B0 a) ((a:A)->B1 a)
= (F, isoToEquiv ((a:A)->B0 a) ((a:A)->B1 a)
F (\(g:(a:A)->B1 a)(a:A)->((e a).2 (g a)).1.1)
(\(g:(a:A)->B1 a)-><i>\(a:A)->retEq (B0 a) (B1 a) (e a) (g a)@i)
(\(f:(a:A)->B0 a)-><i>\(a:A)->secEq (B0 a) (B1 a) (e a) (f a)@i)
)
where F(f:(a:A)->B0 a)(a:A):B1 a= (e a).1 (f a)
eCatIso2 (A B:precategory):Path U (catIso32 A B) (catIso2 A B)
= sigEquivLem' (Path U (cA A) (cA B)) (equiv (cA A) (cA B))
(\(e1:Path U (cA A) (cA B)) -> (e2:catIso321 A B e1)*(_:catIso322 A B e1 e2)*(catIso323 A B e1 e2))
(\(e1:equiv (cA A) (cA B)) -> (e2:catIso21 A B e1)*(_:catIso22 A B e1 e2)*(catIso23 A B e1 e2))
(corrUniv' (cA A) (cA B))
(\(e1:Path U (cA A) (cA B)) -> let e1' : equiv (cA A) (cA B) = transEquiv' (cA B) (cA A) e1
p0 (x:cA A):Path (cA B) (transport e1 x) (e1'.1 x)=lemTransEquiv (cA A) (cA B) e1 x
in
transport
(<i> Path U ((e2:catIso321 A B e1)*(_:catIso322 A B e1 e2)*(catIso323 A B e1 e2))
((e2 : (x y:cA A) -> equiv (cH A x y) (cH B (p0 x@i) (p0 y@i)))
* (_ : (x:cA A) -> Path (cH B (p0 x@i) (p0 x@i)) ((e2 x x).1 (cPath A x)) (cPath B (p0 x@i)))
* ((x y z:cA A)(f:cH A x y)(g:cH A y z)->
Path (cH B (p0 x@i) (p0 z@i))
((e2 x z).1 (cC A x y z f g))
(cC B (p0 x@i) (p0 y@i) (p0 z@i) ((e2 x y).1 f) ((e2 y z).1 g))))
)
(sigEquivLem' (catIso321 A B e1) (catIso21' A B e1)
(\(e2:catIso321 A B e1) -> (_:catIso322 A B e1 e2)*(catIso323 A B e1 e2))
(\(e2:catIso21' A B e1) -> (_:catIso22' A B e1 e2)*(catIso23' A B e1 e2))
(equivPi (cA A)
(\(x:cA A) -> (y:cA A) -> Path U (cH A x y) (cH B (transport e1 x) (transport e1 y)))
(\(x:cA A) -> (y:cA A) -> equiv (cH A x y) (cH B (transport e1 x) (transport e1 y)))
(\(x:cA A) -> equivPi (cA A)
(\(y:cA A) -> Path U (cH A x y) (cH B (transport e1 x) (transport e1 y)))
(\(y:cA A) -> equiv (cH A x y) (cH B (transport e1 x) (transport e1 y)))
(\(y:cA A) -> corrUniv' (cH A x y) (cH B (transport e1 x) (transport e1 y)))))
(\(e2:catIso321 A B e1) -> let e2' (x y:cA A) : equiv (cH A x y) (cH B (transport e1 x) (transport e1 y))
= transEquiv' (cH B (transport e1 x) (transport e1 y)) (cH A x y) (e2 x y)
p2 (x y:cA A)(f:cH A x y):Path (cH B (transport e1 x) (transport e1 y)) (transport (e2 x y) f) ((e2' x y).1 f)
= lemTransEquiv (cH A x y) (cH B (transport e1 x) (transport e1 y)) (e2 x y) f
in
<i> (_:(x:cA A) -> Path (cH B (transport e1 x) (transport e1 x)) (p2 x x (cPath A x)@i) (cPath B (transport e1 x)))
* ((x y z:cA A)(f:cH A x y)(g:cH A y z)->
Path (cH B (transport e1 x) (transport e1 z))
(p2 x z (cC A x y z f g)@i)
(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)))
invEquiv (A:U) (a b:A) : Path U (Path A a b) (Path A b a)
= equivPath (Path A a b) (Path A b a) (inv A a b) (isoToEquiv (Path A a b) (Path A b a) (inv A a b) (inv A b a) (\(x:Path A b a) -> <_> x) (\(x:Path 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, isoToEquiv 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) : Path U (catEquiv A B) (catIso A B)
= <i> (F : functor A B) * (transEquivToPath (catIsEquiv A B F) (catIsIso A B F) (catIsEquivEqIso A B isCA isCB F) @ i)
catIsoEqPath (A B : precategory) : Path U (catIso A B) (Path precategory A B)
= compPath U (catIso A B) (catIso2 A B) (Path precategory A B)
(eCatIso A B)
(compPath U (catIso2 A B) (catIso32 A B) (Path precategory A B)
(<i>eCatIso2 A B@-i)
(compPath U (catIso32 A B) (catIso31 A B) (Path precategory A B)
(<i>eCatIso32 A B@-i)
(compPath U (catIso31 A B) (catIso30 A B) (Path precategory A B)
(<i>eCatIso31 A B@-i)
(compPath U (catIso30 A B) (catIso3 A B) (Path precategory A B)
(<i>eCatIso30 A B@-i)
(<i>eCatIso3 A B@-i)))))
catEquivEqPath (A B : precategory) (isCA : isCategory A) (isCB : isCategory B) : Path U (catEquiv A B) (Path precategory A B)
= compPath U (catEquiv A B) (catIso A B) (Path precategory A B) (catEquivEqIso A B isCA isCB) (catIsoEqPath A B)
opaque catEquivEqPath
catEquivEqPath' (A : category) : isContr ((B : category) * catEquiv A.1 B.1)
= transport (<i> isContr ((B : category) * catEquivEqPath A.1 B.1 A.2 B.2@-i))
((A, <_> A.1)
,\(BB:((B : category) * Path precategory A.1 B.1))->
<i>((BB.2@i
,lemPathPProp (isCategory A.1)
(isCategory BB.1.1)
(propIsCategory A.1)
(<i> isCategory (BB.2@i))
A.2 BB.1.2 @ i)
,<j> BB.2@i/\j))
opaque catEquivEqPath'
--
-- Pullbacks
--
-- f'
-- W -----> Z
-- | |
-- g' | | g
-- | |
-- V V
-- 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
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)
* Path (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
= (_ : Path (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)
* (Path (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 (Path (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)
(Path (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
cospanConePath (C : precategory) (D : cospan C) (E : cospanCone C D) : cospanConeHom C D E E
= (cPath C E.1, cPathL C E.1 D.2.1.1 E.2.1, cPathL 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
,compPath (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
(cPathC C X.1 Y.1 Z.1 D.2.1.1 F.1 G.1 Z.2.1)
(compPath (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)
,compPath (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
(cPathC C X.1 Y.1 Z.1 D.2.2.1 F.1 G.1 Z.2.2.1)
(compPath (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) -> (cospanConePath 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) (cPath C x))
(d : isCospanConeHom C D (x, b) (x, a) (cPath C x)) ->
<i> (compPath (cH C x D.2.1.1) a.1 (cC C x x D.2.1.1 (cPath C x) a.1) b.1 (<i>cPathL C x D.2.1.1 a.1 @-i) d.1 @ i
,compPath (cH C x D.2.2.1) a.2.1 (cC C x x D.2.2.1 (cPath C x) a.2.1) b.2.1 (<i>cPathL C x D.2.2.1 a.2.1 @-i) d.2 @ i
,lemPathPProp (Path (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))
(Path (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>Path (cH C x D.1)
(cC C x D.2.1.1 D.1 (compPath (cH C x D.2.1.1) a.1 (cC C x x D.2.1.1 (cPath C x) a.1) b.1
(<i>cPathL 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 (compPath (cH C x D.2.2.1) a.2.1 (cC C x x D.2.2.1 (cPath C x) a.2.1) b.2.1
(<i>cPathL 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) (cPath 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) (cPath C y.1))
in <i> ( (lemIsCategory C isC x.1 y.1 p @ i).1
, lemPathPProp (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)
opaque hasFinalProp
hasPullbackProp (C : precategory) (isC : isCategory C) (D : cospan C) : prop (hasPullback C D)
= hasFinalProp (cospanConePrecategory C D) (isCategoryCospanCone C D isC)
opaque hasPullbackProp
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 = Path (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 : Path (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)
= compPath (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>cPathC CA c.1 D E F c.2.1 h i@-n)
(compPath (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)
(compPath (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)
(cPathC CA c.1 B E F c.2.2.1 k i)
(compPath (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>cPathC 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 : Path (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)
= compPath (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)
(cPathC 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 : Path (cH CA c.1 D) (cC CA c.1 A D h' j) c.2.1)
: Path U (Path (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1)
(Path (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> Path U (Path (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1)
(Path (cH CA c.1 C) (cPathC CA c.1 A B C h' f g @ i) c'.2.2.1))
(idProp (Path (cH CA c.1 B) (cC CA c.1 A B h' f) c.2.2.1)
(Path (cH CA c.1 C) (cPathC 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 (cPathC CA c.1 A B C h' f g @ 0) c'.2.2.1)
(\(p:Path (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:Path (cH CA c.1 C) (cPathC 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
,compPath (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)
(cPathC CA c.1 A B E h' f k)
(compPath (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))
(compPath (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> cPathC 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 : Path 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 : Path (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')