open import Cat.Functor.Naturality
open import Cat.Instances.Product
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Functor.Reasoning as Fr
import Cat.Reasoning
import Cat.Morphism

open Functor
open _=>_

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

{-# DISPLAY horizontal-comp.nat f g = f β g #-}


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