module Cat.Instances.Functor where private variable o h oβ hβ oβ hβ : Level B C D E : Precategory o h F G : Functor C D
Functor (pre)categoriesπ
open import Cat.Functor.Base public
Functor categoriesπ
When the codomain category is univalent, then so is the category of functors . Essentially, this can be read as saying that βnaturally isomorphic functors are identifiedβ. We begin by proving that the components of a natural isomorphism (a natural transformation with natural inverse) are themselves isomorphisms in .
open import Cat.Functor.Univalence public
Curryingπ
There is an equivalence between the spaces of bifunctors and the space of functors . We refer to the image of a functor under this equivalence as its exponential transpose, and we refer to the map in the βforwardsβ direction (as in the text above) as currying:
Curry : Functor (C ΓαΆ D) E β Functor C Cat[ D , E ] Curry {C = C} {D = D} {E = E} F = curried where open import Cat.Functor.Bifunctor {C = C} {D = D} {E = E} F curried : Functor C Cat[ D , E ] curried .Fβ = Right curried .Fβ xβy = NT (Ξ» f β first xβy) Ξ» x y f β sym (F-β F _ _) Β·Β· ap (Fβ F) (Ξ£-pathp (C .idr _ β sym (C .idl _)) (D .idl _ β sym (D .idr _))) Β·Β· F-β F _ _ curried .F-id = Nat-path Ξ» x β F-id F curried .F-β f g = Nat-path Ξ» x β ap (Ξ» x β Fβ F (_ , x)) (sym (D .idl _)) β F-β F _ _ Uncurry : Functor C Cat[ D , E ] β Functor (C ΓαΆ D) E Uncurry {C = C} {D = D} {E = E} F = uncurried where import Cat.Reasoning C as C import Cat.Reasoning D as D import Cat.Reasoning E as E module F = Functor F uncurried : Functor (C ΓαΆ D) E uncurried .Fβ (c , d) = Fβ (F.β c) d uncurried .Fβ (f , g) = F.β f .Ξ· _ E.β Fβ (F.β _) g uncurried .F-id {x = x , y} = path where abstract path : E ._β_ (F.β (C .id) .Ξ· y) (Fβ (F.β x) (D .id)) β‘ E .id path = F.β C.id .Ξ· y E.β Fβ (F.β x) D.id β‘β¨ E.elimr (F-id (F.β x)) β©β‘ F.β C.id .Ξ· y β‘β¨ (Ξ» i β F.F-id i .Ξ· y) β©β‘ E.id β uncurried .F-β (f , g) (f' , g') = path where abstract path : uncurried .Fβ (f C.β f' , g D.β g') β‘ uncurried .Fβ (f , g) E.β uncurried .Fβ (f' , g') path = F.β (f C.β f') .Ξ· _ E.β Fβ (F.β _) (g D.β g') β‘Λβ¨ E.pulll (Ξ» i β F.F-β f f' (~ i) .Ξ· _) β©β‘Λ F.β f .Ξ· _ E.β F.β f' .Ξ· _ E.β β Fβ (F.β _) (g D.β g') β β‘β¨ ap! (F-β (F.β _) _ _) β©β‘ F.β f .Ξ· _ E.β F.β f' .Ξ· _ E.β Fβ (F.β _) g E.β Fβ (F.β _) g' β‘β¨ cat! E β©β‘ F.β f .Ξ· _ E.β β F.β f' .Ξ· _ E.β Fβ (F.β _) g β E.β Fβ (F.β _) g' β‘β¨ ap! (F.β f' .is-natural _ _ _) β©β‘ F.β f .Ξ· _ E.β (Fβ (F.β _) g E.β F.β f' .Ξ· _) E.β Fβ (F.β _) g' β‘β¨ cat! E β©β‘ ((F.β f .Ξ· _ E.β Fβ (F.β _) g) E.β (F.β f' .Ξ· _ E.β Fβ (F.β _) g')) β
Constant diagramsπ
There is a functor from to that takes an object to the constant functor .
module _ {o β o' β'} {C : Precategory o β} {J : Precategory o' β'} where private module C = Precategory C private module J = Precategory J
ConstD : Functor C Cat[ J , C ] ConstD .Fβ x = Const x ConstD .Fβ f = const-nt f ConstD .F-id = Nat-path (Ξ» _ β refl) ConstD .F-β f g = Nat-path (Ξ» _ β refl)
Fβ-assoc : β {o β o' β' o'' β'' oβ ββ} {C : Precategory o β} {D : Precategory o' β'} {E : Precategory o'' β''} {F : Precategory oβ ββ} {F : Functor E F} {G : Functor D E} {H : Functor C D} β F Fβ (G Fβ H) β‘ (F Fβ G) Fβ H Fβ-assoc = Functor-path (Ξ» x β refl) Ξ» x β refl Fβ-idl : β {o'' β'' oβ ββ} {E : Precategory o'' β''} {E' : Precategory oβ ββ} {F : Functor E E'} β Id Fβ F β‘ F Fβ-idl = Functor-path (Ξ» x β refl) Ξ» x β refl Fβ-idr : β {o'' β'' oβ ββ} {E : Precategory o'' β''} {E' : Precategory oβ ββ} {F : Functor E E'} β F Fβ Id β‘ F Fβ-idr = Functor-path (Ξ» x β refl) Ξ» x β refl module _ {o β o' β' o'' β''} {C : Precategory o β} {D : Precategory o' β'} {E : Precategory o'' β''} where private module CD = Cat.Reasoning Cat[ C , D ] module DE = Cat.Reasoning Cat[ D , E ] module CE = Cat.Reasoning Cat[ C , E ] Fβ-iso-l : {F F' : Functor D E} {G : Functor C D} β F DE.β F' β (F Fβ G) CE.β (F' Fβ G) Fβ-iso-l {F} {F'} {G} isom = CE.make-iso (isom.to β G) (isom.from β G) (Nat-path Ξ» x β isom.invl Ξ·β _) (Nat-path Ξ» x β isom.invr Ξ·β _) where module isom = DE._β _ isom Fβ-iso-r : {F : Functor D E} {G G' : Functor C D} β G CD.β G' β (F Fβ G) CE.β (F Fβ G') Fβ-iso-r {F} {G} {G'} isom = CE.make-iso (F βΈ isom.to) (F βΈ isom.from) (Nat-path Ξ» x β F.annihilate (isom.invl Ξ·β _)) (Nat-path Ξ» x β F.annihilate (isom.invr Ξ·β _)) where module isom = CD._β _ isom module F = Cat.Functor.Reasoning F open import Cat.Functor.Naturality public module _ {o β o' β'} {C : Precategory o β} {D : Precategory o' β'} where private module DD = Cat.Reasoning Cat[ D , D ] module CD = Cat.Reasoning Cat[ C , D ] module D = Cat.Reasoning D module C = Cat.Reasoning C Fβ-iso-id-l : {F : Functor D D} {G : Functor C D} β F β βΏ Id β (F Fβ G) β βΏ G Fβ-iso-id-l {F} {G} isom = subst ((F Fβ G) CD.β _) Fβ-idl (Fβ-iso-l isom) open _=>_ _ni^op : F β βΏ G β Functor.op F β βΏ Functor.op G _ni^op Ξ± = Cat.Reasoning.make-iso _ (_=>_.op (IsoβΏ.from Ξ±)) (_=>_.op (IsoβΏ.to Ξ±)) (Nat-path Ξ» j β IsoβΏ.invl Ξ± Ξ·β _) (Nat-path Ξ» j β IsoβΏ.invr Ξ± Ξ·β _) module _ {o β ΞΊ} {C : Precategory o β} where open Functor open _=>_ natural-iso-to-is-equiv : {F G : Functor C (Sets ΞΊ)} β (eta : F β βΏ G) β β x β is-equiv (IsoβΏ.to eta .Ξ· x) natural-iso-to-is-equiv eta x = is-isoβis-equiv $ iso (IsoβΏ.from eta .Ξ· x) (Ξ» x i β IsoβΏ.invl eta i .Ξ· _ x) (Ξ» x i β IsoβΏ.invr eta i .Ξ· _ x) natural-iso-from-is-equiv : {F G : Functor C (Sets ΞΊ)} β (eta : F β βΏ G) β β x β is-equiv (IsoβΏ.from eta .Ξ· x) natural-iso-from-is-equiv eta x = is-isoβis-equiv $ iso (IsoβΏ.to eta .Ξ· x) (Ξ» x i β IsoβΏ.invr eta i .Ξ· _ x) (Ξ» x i β IsoβΏ.invl eta i .Ξ· _ x) natural-isoβequiv : {F G : Functor C (Sets ΞΊ)} β (eta : F β βΏ G) β β x β β£ F .Fβ x β£ β β£ G .Fβ x β£ natural-isoβequiv eta x = IsoβΏ.to eta .Ξ· x , natural-iso-to-is-equiv eta x