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

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-∘ _ _