{- Category Theory: - Functor; - Coslice Category; - Universal Arrow; - Equivalence. Copyright (c) Groupoid Infinity, 2014-2018. HoTT 9.2 Functors and transformations HoTT 9.4 Equivalences -} module fun where import cat import iso_sigma -- Definition 9.2.1. Functor on Precategories catfunctor (A B: precategory): U = (ob: carrier A -> carrier B) * (mor: (x y: carrier A) -> hom A x y -> hom B (ob x) (ob y)) * (id: (x: carrier A) -> Path (hom B (ob x) (ob x)) (mor x x (path A x)) (path B (ob x))) * ((x y z: carrier A) -> (f: hom A x y) -> (g: hom A y z) -> Path (hom B (ob x) (ob z)) (mor x z (compose A x y z f g)) (compose B (ob x) (ob y) (ob z) (mor x y f) (mor y z g))) idFunctor (A: precategory): catfunctor A A = (\(x: carrier A) -> x, \(x y: carrier A) (h: hom A x y) -> h, \(x: carrier A) -> <_> path A x, \(x y z: carrier A) (f: hom A x y) (g: hom A y z) -> <_> compose A x y z f g) compFunctor (A B C: precategory) (F: catfunctor A B) (G: catfunctor B C): catfunctor A C = (\(x: carrier A) -> G.1 (F.1 x), \(x y: carrier A) (h: hom A x y) -> G.2.1 (F.1 x) (F.1 y) (F.2.1 x y h), \(x: carrier A) -> composition (hom 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 (path A x))) (G.2.1 (F.1 x) (F.1 x) (path B (F.1 x))) (path C (G.1 (F.1 x))) (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: carrier A) (f: hom A x y) (g: hom A y z) -> composition (hom 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 (compose A x y z f g))) (G.2.1 (F.1 x) (F.1 z) (compose B (F.1 x) (F.1 y) (F.1 z) (F.2.1 x y f) (F.2.1 y z g))) (compose 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))) ( 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))) compFunctor' (A B C: precategory) (F: catfunctor B C) (G: catfunctor A B): catfunctor A C = compFunctor A B C G F functorId (A B : precategory) (f g : catfunctor A B) (p : Path ( (Fob : carrier A -> carrier B) * ((x y : carrier A) -> hom A x y -> hom B (Fob x) (Fob y))) (f.1, f.2.1) (g.1, g.2.1)) : Path (catfunctor A B) f g = let T0 : U = (Fob : carrier A -> carrier B) * ((x y : carrier A) -> hom A x y -> hom B (Fob x) (Fob y)) T1 (t : T0) : U = (Fid : (x : carrier A) -> Path (hom B (t.1 x) (t.1 x)) (t.2 x x (path A x)) (path B (t.1 x))) * ((x y z: carrier A) -> (f : hom A x y) -> (g : hom A y z) -> Path (hom B (t.1 x) (t.1 z)) (t.2 x z (compose A x y z f g)) (compose B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g))) pT1 (t : T0): isProp (T1 t) = let T2: U = (x: carrier A) -> Path (hom B (t.1 x) (t.1 x)) (t.2 x x (path A x)) (path B (t.1 x)) pT2: isProp T2 = propPi (carrier A) (\ (x: carrier A) -> Path (hom B (t.1 x) (t.1 x)) (t.2 x x (path A x)) (path B (t.1 x))) (\ (x: carrier A) -> homSet B (t.1 x) (t.1 x) (t.2 x x (path A x)) (path B (t.1 x))) T3: U = (x y z: carrier A) (f: hom A x y) (g: hom A y z) -> Path (hom B (t.1 x) (t.1 z)) (t.2 x z (compose A x y z f g)) (compose B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g)) pT3: isProp T3 = let p0 (x y z : carrier A) (f : hom A x y) (g : hom A y z) : isProp (Path (hom B (t.1 x) (t.1 z)) (t.2 x z (compose A x y z f g)) (compose B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g))) = homSet B (t.1 x) (t.1 z) (t.2 x z (compose A x y z f g)) (compose B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g)) p1 (x y z : carrier A) (f : hom A x y) : isProp ((g : hom A y z) -> Path (hom B (t.1 x) (t.1 z)) (t.2 x z (compose A x y z f g)) (compose B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g))) = propPi (hom A y z) (\ (g : hom A y z) -> Path (hom B (t.1 x) (t.1 z)) (t.2 x z (compose A x y z f g)) (compose B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g))) (p0 x y z f) p2 (x y z : carrier A) : isProp ((f : hom A x y) (g : hom A y z) -> Path (hom B (t.1 x) (t.1 z)) (t.2 x z (compose A x y z f g)) (compose B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g))) = propPi (hom A x y) (\ (f : hom A x y) -> (g : hom A y z) -> Path (hom B (t.1 x) (t.1 z)) (t.2 x z (compose A x y z f g)) (compose B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g))) (p1 x y z) in propPi3 (carrier A) (\ (x y z : carrier A) -> (f : hom A x y) -> (g : hom A y z) -> Path (hom B (t.1 x) (t.1 z)) (t.2 x z (compose A x y z f g)) (compose B (t.1 x) (t.1 y) (t.1 z) (t.2 x y f) (t.2 y z g))) p2 in propAnd T2 T3 pT2 pT3 p0 : Path ((t : T0) * T1 t) ((f.1, f.2.1), (f.2.2.1, f.2.2.2)) ((g.1, g.2.1), (g.2.2.1, g.2.2.2)) = lemSig T0 T1 pT1 ((f.1, f.2.1), (f.2.2.1, f.2.2.2)) ((g.1, g.2.1), (g.2.2.1, g.2.2.2)) p in ((p0 @ i).1.1, (p0 @ i).1.2, (p0 @ i).2.1, (p0 @ i).2.2) cosliceCat (C D: precategory) (a: carrier C) (F: catfunctor D C): precategory = ((Ob, Hom),id,cmp,HomSet,L,R,Q) where Ob: U = (y: carrier D) * hom C a (F.1 y) Hom (x y: Ob) : U = (h: hom D x.1 y.1) * Path (hom C a (F.1 y.1)) y.2 (compose C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 h)) id (x: Ob) : Hom x x = (path D x.1, comp (<_> (hom C a (F.1 x.1))) (compose C a (F.1 x.1) (F.1 x.1) x.2 (F.2.2.1 x.1 @ -i)) [ (i = 0) -> pathR C a (F.1 x.1) x.2 , (i = 1) -> <_> compose C a (F.1 x.1) (F.1 x.1) x.2 (F.2.1 x.1 x.1 (path D x.1)) ]) cmp (x y z: Ob) (f: Hom x y) (g: Hom y z): Hom x z = let h: hom D x.1 z.1 = compose D x.1 y.1 z.1 f.1 g.1 p : Path (hom C a (F.1 z.1)) z.2 (compose C a (F.1 x.1) (F.1 z.1) x.2 (F.2.1 x.1 z.1 h)) = let p2: Path (hom C a (F.1 z.1)) z.2 (compose C a (F.1 y.1) (F.1 z.1) (compose C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 f.1)) (F.2.1 y.1 z.1 g.1)) = comp (<_> hom C a (F.1 z.1)) (g.2 @ i) [ (i = 0) -> <_> z.2 , (i = 1) -> compose C a (F.1 y.1) (F.1 z.1) (f.2 @ j) (F.2.1 y.1 z.1 g.1) ] p3 : Path (hom C a (F.1 z.1)) (compose C a (F.1 y.1) (F.1 z.1) (compose C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 f.1)) (F.2.1 y.1 z.1 g.1)) (compose C a (F.1 x.1) (F.1 z.1) x.2 (F.2.1 x.1 z.1 (compose D x.1 y.1 z.1 f.1 g.1))) = comp (<_> hom C a (F.1 z.1)) (pathC C a (F.1 x.1) (F.1 y.1) (F.1 z.1) x.2 (F.2.1 x.1 y.1 f.1) (F.2.1 y.1 z.1 g.1) @ i) [ (i = 0) -> <_> compose C a (F.1 y.1) (F.1 z.1) (compose C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 f.1)) (F.2.1 y.1 z.1 g.1) , (i = 1) -> compose C a (F.1 x.1) (F.1 z.1) x.2 (F.2.2.2 x.1 y.1 z.1 f.1 g.1 @ -j) ] in comp (<_> hom C a (F.1 z.1)) (p2 @ i) [ (i = 0) -> <_> z.2 , (i = 1) -> p3 ] in (h, p) HomSet (x y : Ob): isSet (Hom x y) = let p0: isSet (hom D x.1 y.1) = homSet D x.1 y.1 p1 (h: hom D x.1 y.1) : isSet (Path (hom C a (F.1 y.1)) y.2 (compose C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 h))) = propSet ((Path (hom C a (F.1 y.1)) y.2 (compose C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 h)))) (homSet C a (F.1 y.1) y.2 (compose C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 h))) in setSig (hom D x.1 y.1) (\ (h: hom D x.1 y.1) -> Path (hom C a (F.1 y.1)) y.2 (compose C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 h))) p0 p1 homId (x y: Ob) (h0 h1: Hom x y) (p: Path (hom D x.1 y.1) h0.1 h1.1): Path (Hom x y) h0 h1 = let A : U = hom D x.1 y.1 P (h : A) : U = Path (hom C a (F.1 y.1)) y.2 (compose C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 h)) pP (h : A) : isProp (P h) = homSet C a (F.1 y.1) y.2 (compose C a (F.1 x.1) (F.1 y.1) x.2 (F.2.1 x.1 y.1 h)) in lemSig A P pP h0 h1 p L (x y: Ob) (f : Hom x y) : Path (Hom x y) (cmp x x y (id x) f) f = homId x y (cmp x x y (id x) f) f (pathL D x.1 y.1 f.1) R (x y: Ob) (f : Hom x y) : Path (Hom x y) (cmp x y y f (id y)) f = homId x y (cmp x y y f (id y)) f (pathR D x.1 y.1 f.1) Q (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)) = homId x w (cmp x z w (cmp x y z f g) h) (cmp x y w f (cmp y z w g h)) (pathC D x.1 y.1 z.1 w.1 f.1 g.1 h.1) sliceCat (C D: precategory) (a: carrier (opCat C)) (F: catfunctor D (opCat C)) : precategory = cosliceCat (opCat C) D a F ffFunctor (A B: precategory) (F: catfunctor A B) : U = (a b: carrier A) -> isEquiv (hom A a b) (hom B (F.1 a) (F.1 b)) (F.2.1 a b) propFFFunctor (A B: precategory) (F: catfunctor A B): isProp (ffFunctor A B F) = propPi (carrier A) (\(a: carrier A) -> (b: carrier A) -> isEquiv (hom A a b) (hom B (F.1 a) (F.1 b)) (F.2.1 a b)) (\(a: carrier A) -> propPi (carrier A) (\(b: carrier A) -> isEquiv (hom A a b) (hom B (F.1 a) (F.1 b)) (F.2.1 a b)) (\(b: carrier A) -> propIsEquiv (hom A a b) (hom B (F.1 a) (F.1 b)) (F.2.1 a b))) catIsEquiv (A B: precategory) (F: catfunctor A B): U = (_: ffFunctor A B F) * ((b: carrier B) -> (a : carrier A) * iso B (F.1 a) b) catEquiv (A B: precategory) : U = (F: catfunctor A B) * catIsEquiv A B F catPathIsEquiv (A: precategory): catIsEquiv A A (idFunctor A) = (\(a b: carrier A) -> idIsEquiv (hom A a b),\(b:carrier A) -> (b, idIso A b)) catPathEquiv (A: precategory): catEquiv A A = (idFunctor A, catPathIsEquiv A) catIsIso (A B: precategory) (F: catfunctor A B) : U = (_: ffFunctor A B F) * isEquiv (carrier A) (carrier B) F.1 catPropIsIso (A B: precategory) (F: catfunctor A B) : isProp (catIsIso A B F) = propSig (ffFunctor A B F) (\(_: ffFunctor A B F) -> isEquiv (carrier A) (carrier B) F.1) (propFFFunctor A B F) (\(_: ffFunctor A B F) -> propIsEquiv (carrier A) (carrier B) F.1) catIso (A B: precategory): U = (F: catfunctor A B) * catIsIso A B F F12 (A B : precategory) (isC : isCategory A) (F : catfunctor A B) (p1 : ffFunctor A B F) (x : carrier A) : isContr ((y : carrier A) * iso B (F.1 y) (F.1 x)) = undefined F23 (A B : precategory) (F : catfunctor A B) (p2 : (x : carrier A) -> isContr ((y : carrier A) * iso B (F.1 y) (F.1 x))) (x : carrier B) (a b : (y : carrier A) * iso B (F.1 y) x) : Path ((y : carrier A) * iso B (F.1 y) x) a b = undefined catPropIsEquiv (A B: precategory) (isC: isCategory A) (F: catfunctor A B): isProp (catIsEquiv A B F) = propSig (ffFunctor A B F) (\(_: ffFunctor A B F) -> (b: carrier B) -> (a: carrier A) * iso B (F.1 a) b) (propFFFunctor A B F) (\ (ff: ffFunctor A B F) -> propPi (carrier B) (\(b: carrier B) -> (a: carrier A) * iso B (F.1 a) b) (\(b: carrier B) -> F23 A B F (F12 A B isC F ff) b)) 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)) eqToIso (C : precategory) (A B : carrier C) (p : Path (carrier C) A B) : iso C A B = J (carrier C) A (\(B : carrier C) -> \(p : Path (carrier C) A B) -> iso C A B) (idIso C A) B p lemIsCategory (C : precategory) (isC : isCategory C) (A B : carrier C) (e : iso C A B) : Path ((B : carrier C) * iso C A B) (A, idIso C A) (B, e) = (isContrProp ((B : carrier C) * iso C A B) (isC A) (A, idIso C A) (B, e) @ i) lemIsCategory2 (C : precategory) (isC : isCategory C) (A B : carrier C) : isEquiv (Path (carrier C) A B) (iso C A B) (eqToIso C A B) = equivFunFib (carrier C) (Path (carrier C) A) (iso C A) (eqToIso C A) (isContrSingl (carrier C) A) (isC A) B lemIsCategory3 (C : precategory) (isC : isCategory C) (A B : carrier C) : Path U (Path (carrier C) A B) (iso C A B) = equivPath (Path (carrier C) A B) (iso C A B) (eqToIso C A B) (lemIsCategory2 C isC A B) catEquivIsIso (A B: precategory) (isCA: isCategory A) (isCB: isCategory B) (F: catfunctor A B) (e: catIsEquiv A B F) : catIsIso A B F = (e.1, \(b:carrier B) -> let p : isContr ((a:carrier 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 (isContr ((a:carrier A) * invEquiv (carrier B) (F.1 a) b @ i)) (transport ( isContr ((a:carrier A) * lemIsCategory3 B isCB (F.1 a) b@-i)) p)) catIsoIsEquiv (A B: precategory) (F: catfunctor A B) (e: catIsIso A B F): catIsEquiv A B F = (e.1,\(b:carrier B)->((e.2 b).1.1, eqToIso B (F.1 (e.2 b).1.1) b ((e.2 b).1.2@-i))) catIsEquivEqIso (A B: precategory) (isCA: isCategory A) (isCB: isCategory B) (F: catfunctor 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) catIsoEqPath (A B: precategory) : Path U (catIso A B) (Path precategory A B) = undefined catEquivEqPath' (A: category) : isContr ((B : category) * catEquiv A.1 B.1) = undefined catEquivEqIso (A B: precategory) (isCA: isCategory A) (isCB: isCategory B) : Path U (catEquiv A B) (catIso A B) = (F: catfunctor A B) * (equivToPath (catIsEquiv A B F) (catIsIso A B F) (catIsEquivEqIso A B isCA isCB F) @ i) catEquivEqPath (A B: precategory) (isCA: isCategory A) (isCB: isCategory B) : Path U (catEquiv A B) (Path precategory A B) = composition U (catEquiv A B) (catIso A B) (Path precategory A B) (catEquivEqIso A B isCA isCB) (catIsoEqPath A B)