module Cat.Functor.Compose where

Functoriality of functor compositionπŸ”—

When the operation of functor composition, (F,G)↦F∘G(F, G) \mapsto F \circ G, 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 [B,C]Γ—[A,B]β†’[A,C][B, C] \times [A, B] \to [A,C];
  • The precomposition functor associated with any p:Cβ†’Cβ€²p : C \to C', which will be denoted βˆ’βˆ˜p:[Cβ€²,D]β†’[C,D]- \circ p : [C', D] \to [C,D] in TeX and precompose in Agda;
  • The postcomposition functor associated with any p:Cβ†’Cβ€²p : C \to C', which will be denoted pβˆ˜βˆ’:[A,C]β†’[A,Cβ€²]p \circ - : [A,C] \to [A,C']; In the code, that’s postcompose.

Note that the precomposition functor βˆ’βˆ˜p- \circ p is necessarily β€œcontravariant” when compared with pp, in that it points in the opposite direction to pp.

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₁ {y = y , _} (n1 , n2) .Ξ· x = y .F₁ (n2 .Ξ· _) C.∘ n1 .Ξ· _

  go .F₁ {x = F , G} {y = W , X} (n1 , n2) .is-natural _ _ f =
    (W .F₁ (n2 .Ξ· _) C.∘ n1 .Ξ· _) C.∘ F .F₁ (G .F₁ f) β‰‘βŸ¨ C.pullr (n1 .is-natural _ _ _) βŸ©β‰‘
    W .F₁ (n2 .Ξ· _) C.∘ W .F₁ (G .F₁ f) C.∘ n1 .Ξ· _   β‰‘βŸ¨ C.extendl (W.weave (n2 .is-natural _ _ _)) βŸ©β‰‘
    W .F₁ (X .F₁ f) C.∘ W .F₁ (n2 .Ξ· _) C.∘ n1 .Ξ· _   ∎
    where module W = Fr W

  go .F-id {x} = Nat-path Ξ» _ β†’ C.idr _ βˆ™ x .fst .F-id
  go .F-∘ {x} {y , _} {z , _} (f , _) (g , _) = Nat-path Ξ» _ β†’
    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 (natural transformations) first, called whiskerings, first. The mnemonic for triangles is that the base points towards the side that does not change, so in (e.g.) f▢θf \blacktriangleright \theta, the ff is unchanging: this expression has type fg→fhfg \to fh, as long as θ:g→h\theta : g \to h.

_β—‚_ : 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 βˆ’βˆ˜p- \circ p and pβˆ˜βˆ’p \circ - 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    = Nat-path Ξ» _ β†’ refl
  precompose .F-∘ f g = Nat-path Ξ» _ β†’ refl

  postcompose : Functor Cat[ D , C ] Cat[ D , Cβ€² ]
  postcompose .Fβ‚€ G    = p F∘ G
  postcompose .F₁ ΞΈ    = p β–Έ ΞΈ
  postcompose .F-id    = Nat-path Ξ» _ β†’ p .F-id
  postcompose .F-∘ f g = Nat-path Ξ» _ β†’ p .F-∘ _ _

Whiskerings are instances of a more general form of composition for natural transformations, known as horizontal composition.

_β—†_ : βˆ€ {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 _ _ _))