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

import Cat.Functor.Reasoning
import Cat.Reasoning
import Cat.Morphism

open Functor
open _=>_

module Cat.Functor.Compose where

Functoriality of functor composition🔗

When the operation of functor composition, $(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] \times [A, B] \to [A, C];$
The precomposition functor associated with any $p : C \to C^{'},$ which will be denoted $- \circ p : [C^{'}, D] \to [C, D]$ in TeX and precompose in Agda;
The postcomposition functor associated with any $p : C \to C^{'},$ which will be denoted $p \circ - : [A, C] \to [A, C^{'}];$ In the code, that’s postcompose.

Note that the precomposition functor $- \circ p$ is necessarily “contravariant” when compared with $p,$ in that it points in the opposite direction to $p .$

private variable
  o ℓ : Level
  A B C C' D E : Precategory o ℓ
  F G H K L M : 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 $F \circ H \Rightarrow G \circ K .$

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 Cat.Functor.Reasoning
  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.) $F ▶ θ,$ the $F$ is unchanging: this expression has type $FG \to F H,$ as long as $θ : 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 $- \circ p$ and $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    = 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-∘ _ _

We also remark that horizontal composition obeys a very handy interchange law.

◆-interchange
  : {F H L : Functor B C} {G K M : Functor A B}
  → (α : F => H) (β : G => K)
  → (γ : H => L) (δ : K => M)
  → (γ ◆ δ) ∘nt (α ◆ β) ≡ (γ ∘nt α) ◆ (δ ∘nt β)
◆-interchange {B = B} {C = C} {A = A} {H = H} {L = L}  α β γ δ = ext λ j →
  (L.₁ (δ .η _) C.∘ γ .η _) C.∘ H.₁ (β .η _) C.∘ α .η _ ≡⟨ C.extendl (sym (L.shuffler (sym (γ .is-natural _ _ _)))) ⟩≡
  L.₁ (δ .η _ B.∘ β .η _) C.∘ γ .η _ C.∘ α .η _         ∎
  where
    module A = Cat.Reasoning A
    module B = Cat.Reasoning B
    module C = Cat.Reasoning C
    module L = Cat.Functor.Reasoning L
    module H = Cat.Functor.Reasoning H
    open Functor

module _ {F G : Functor C D} where
  open Cat.Morphism
  open Cat.Functor.Reasoning

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