module Cat.Functor.Compose where
Functoriality of functor compositionπ
When the operation of functor composition, is seen as happening not only to functors but to whole functor categories, then it is itself functorial. This is a bit mind-bending at first, but this module will construct the functor composition functors. Thereβs actually a family of three related functors weβre interested in:
- The functor composition functor itself, having type
- The precomposition functor associated with any
which will be denoted
in TeX and
precompose
in Agda; - The postcomposition functor associated with any
which will be denoted
In the code, thatβs
postcompose
.
Note that the precomposition functor is necessarily βcontravariantβ when compared with in that it points in the opposite direction to
private variable o β : Level A B C C' D E : Precategory o β F G H K : Functor C D Ξ± Ξ² Ξ³ : F => G
We start by defining the action of the composition functor on morphisms: given a pair of natural transformations as in the following diagram, we define their horizontal composition as a natural transformation
Note that there are two ways to do so, but they are equal by naturality of
_β_ : β {F G : Functor D E} {H K : Functor C D} β F => G β H => K β F Fβ H => G Fβ K _β_ {E = E} {F = F} {G} {H} {K} Ξ± Ξ² = nat module horizontal-comp where private module E = Cat.Reasoning E open Fr nat : F Fβ H => G Fβ K nat .Ξ· x = G .Fβ (Ξ² .Ξ· _) E.β Ξ± .Ξ· _ nat .is-natural x y f = E.pullr (Ξ± .is-natural _ _ _) β E.extendl (weave G (Ξ² .is-natural _ _ _))
We can now define the composition functor itself.
Fβ-functor : Functor (Cat[ B , C ] ΓαΆ Cat[ A , B ]) Cat[ A , C ] Fβ-functor {C = C} = go module Fβ-f where private module C = Cat.Reasoning C go : Functor _ _ go .Fβ (F , G) = F Fβ G go .Fβ (Ξ± , Ξ²) = Ξ± β Ξ² go .F-id {x} = ext Ξ» _ β C.idr _ β x .fst .F-id go .F-β {x} {y , _} {z , _} (f , _) (g , _) = ext Ξ» _ β z .Fβ _ C.β f .Ξ· _ C.β g .Ξ· _ β‘β¨ C.pushl (z .F-β _ _) β©β‘ z .Fβ _ C.β z .Fβ _ C.β f .Ξ· _ C.β g .Ξ· _ β‘β¨ C.extend-inner (sym (f .is-natural _ _ _)) β©β‘ z .Fβ _ C.β f .Ξ· _ C.β y .Fβ _ C.β g .Ξ· _ β‘β¨ C.pulll refl β©β‘ (z .Fβ _ C.β f .Ξ· _) C.β (y .Fβ _ C.β g .Ξ· _) β {-# DISPLAY Fβ-f.go = Fβ-functor #-}
Before setting up the pre/post-composition functors, we define their action on morphisms, called whiskerings: these are special cases of horizontal composition where one of the natural transformations is the identity, so defining them directly saves us one application of the unit laws. The mnemonic for triangles is that the base points towards the side that does not change, so in (e.g.) the is unchanging: this expression has type as long as
_β_ : F => G β (H : Functor C D) β F Fβ H => G Fβ H _β_ nt H .Ξ· x = nt .Ξ· _ _β_ nt H .is-natural x y f = nt .is-natural _ _ _ _βΈ_ : (H : Functor E C) β F => G β H Fβ F => H Fβ G _βΈ_ H nt .Ξ· x = H .Fβ (nt .Ξ· x) _βΈ_ H nt .is-natural x y f = sym (H .F-β _ _) β ap (H .Fβ) (nt .is-natural _ _ _) β H .F-β _ _
With the whiskerings already defined, defining and is easy:
module _ (p : Functor C C') where precompose : Functor Cat[ C' , D ] Cat[ C , D ] precompose .Fβ G = G Fβ p precompose .Fβ ΞΈ = ΞΈ β p precompose .F-id = trivial! precompose .F-β f g = trivial! postcompose : Functor Cat[ D , C ] Cat[ D , C' ] postcompose .Fβ G = p Fβ G postcompose .Fβ ΞΈ = p βΈ ΞΈ postcompose .F-id = ext Ξ» _ β p .F-id postcompose .F-β f g = ext Ξ» _ β p .F-β _ _
module _ {F G : Functor C D} where open Cat.Morphism open Fr _βni_ : F β βΏ G β (H : Functor B C) β (F Fβ H) β βΏ (G Fβ H) (Ξ± βni H) = make-iso _ (Ξ± .to β H) (Ξ± .from β H) (ext Ξ» _ β Ξ± .invl Ξ·β _) (ext Ξ» _ β Ξ± .invr Ξ·β _) _βΈni_ : (H : Functor D E) β F β βΏ G β (H Fβ F) β βΏ (H Fβ G) (H βΈni Ξ±) = make-iso _ (H βΈ Ξ± .to) (H βΈ Ξ± .from) (ext Ξ» _ β annihilate H (Ξ± .invl Ξ·β _)) (ext Ξ» _ β annihilate H (Ξ± .invr Ξ·β _))
β-distribl : (Ξ± βnt Ξ²) β H β‘ (Ξ± β H) βnt (Ξ² β H) β-distribl = trivial! βΈ-distribr : F βΈ (Ξ± βnt Ξ²) β‘ (F βΈ Ξ±) βnt (F βΈ Ξ²) βΈ-distribr {F = F} = ext Ξ» _ β F .F-β _ _ module _ where open Cat.Reasoning -- [TODO: Reed M, 14/03/2023] Extend the coherence machinery to handle natural -- isos. ni-assoc : {F : Functor D E} {G : Functor C D} {H : Functor B C} β (F Fβ G Fβ H) β βΏ ((F Fβ G) Fβ H) ni-assoc {E = E} = to-natural-iso Ξ» where .make-natural-iso.eta _ β E .id .make-natural-iso.inv _ β E .id .make-natural-iso.etaβinv _ β E .idl _ .make-natural-iso.invβeta _ β E .idl _ .make-natural-iso.natural _ _ _ β E .idr _ β sym (E .idl _)