open import Cat.Functor.Adjoint
open import Cat.Prelude

import Cat.Functor.Reasoning
import Cat.Reasoning

module Cat.Functor.Adjoint.Mate where

Mates🔗

Let $F⊣U:A\to B\text{,}$ $F^{\prime }⊣U^{\prime }:A^{\prime }\to B^{\prime }$ be a pair of adjunctions, and let $X:A\to A^{\prime }$ and $Y:B\to B^{\prime }$ be a pair of functors, fitting together into a diagram

which needn’t necessarily commute. By pasting with the adjunction units and counits, there is an equivalence between the sets of natural transformations $XU\to U^{\prime }Y$ and $F^{\prime }X\to YF\text{,}$ which in one direction sends

to

We call natural transformations $\alpha :XU\to U^{\prime }Y$ and $\beta :F^{\prime }X\to YF$ mates, with respect to the adjunctions $F⊣U$ and $F^{\prime }⊣U^{\prime }\text{,}$ if they correspond under this equivalence.

open Functor

module _
  {oa ℓa ob ℓb oc ℓc od ℓd}
  {A : Precategory oa ℓa}
  {A' : Precategory ob ℓb}
  {B : Precategory oc ℓc}
  {B' : Precategory od ℓd}
  {F : Functor A B}
  {U : Functor B A}
  {F' : Functor A' B'}
  {U' : Functor B' A'}
  (F⊣U : F ⊣ U)
  (F'⊣U' : F' ⊣ U')
  (X : Functor A A')
  (Y : Functor B B')
  where
  private
    module F⊣U = _⊣_ F⊣U
    module F'⊣U' = _⊣_ F'⊣U'
    module U = Cat.Functor.Reasoning U
    module U' = Cat.Functor.Reasoning U'
    module F = Cat.Functor.Reasoning F
    module F' = Cat.Functor.Reasoning F'
    module X = Cat.Functor.Reasoning X
    module Y = Cat.Functor.Reasoning Y
    module A = Cat.Reasoning A
    module B = Cat.Reasoning B
    module A' = Cat.Reasoning A'
    module B' = Cat.Reasoning B'

  private
    η : ∀ {x} → A.Hom x (U.₀ (F.₀ x))
    η = F⊣U.unit.η _

    ε : ∀ {x} → B.Hom (F.₀ (U.₀ x)) x
    ε = F⊣U.counit.ε _

    η' : ∀ {x} → A'.Hom x (U'.₀ (F'.₀ x))
    η' = F'⊣U'.unit.η _

    ε' : ∀ {x} → B'.Hom (F'.₀ (U'.₀ x)) x
    ε' = F'⊣U'.counit.ε _

Unfortunately, proof assistants: if we were to define mates by pasting, we would get a natural transformation with much worse definitional behaviour. Therefore, we calculate the mate of a transformation $\alpha :XU\to U^{\prime }Y$ by hand.

  mate : (X F∘ U) => (U' F∘ Y) → (F' F∘ X) => (Y F∘ F)
  mate α = nt module mate where
    module α = _=>_ α

    nt : (F' F∘ X) => (Y F∘ F)
    nt ._=>_.η _ =
      ε' B'.∘ F'.₁ (α.η _) B'.∘ F'.₁ (X.₁ η)
    nt ._=>_.is-natural x y f =
      (ε' B'.∘ F'.₁ (α.η _) B'.∘ F'.₁ (X.₁ η)) B'.∘ F'.₁ (X.₁ f)              ≡⟨ B'.extendr (B'.pullr (F'.weave (X.weave (F⊣U.unit.is-natural _ _ _)))) ⟩≡
      (ε' B'.∘ F'.₁ (α.η _)) B'.∘ F'.₁ (X.₁ (U.₁ (F.₁ f))) B'.∘ F'.₁ (X.₁ η)  ≡⟨ B'.extendl (B'.extendr (F'.weave (α.is-natural _ _ _))) ⟩≡
      (ε' B'.∘ F'.₁ (U'.₁ (Y.₁ (F.₁ f)))) B'.∘ F'.₁ (α.η _) B'.∘ F'.₁ (X.₁ η) ≡⟨ B'.pushl (F'⊣U'.counit.is-natural _ _ _) ⟩≡
      Y.₁ (F.₁ f) B'.∘ (ε' B'.∘ F'.₁ (α.η _) B'.∘ F'.₁ (X.₁ η))               ∎

By a very similar calculation, we can define the mate of $\beta :F^{\prime }X\to YF\text{.}$

  mate-inv : (F' F∘ X) => (Y F∘ F) → (X F∘ U) => (U' F∘ Y)
  mate-inv α = nt module mate-inv where
    module α = _=>_ α

    nt : (X F∘ U) => (U' F∘ Y)
    nt ._=>_.η _ =
      U'.₁ (Y.₁ ε) A'.∘ U'.₁ (α.η _) A'.∘ η'
    nt ._=>_.is-natural x y f =
      (U'.₁ (Y.₁ ε) A'.∘ U'.₁ (α.η _) A'.∘ η') A'.∘ X.₁ (U.₁ f)                     ≡⟨ A'.extendr (A'.pullr (F'⊣U'.unit.is-natural _ _ _)) ⟩≡
      (U'.₁ (Y.₁ ε) A'.∘ U'.₁ (α.η (U.₀ y))) A'.∘ U'.₁ (F'.₁ (X.₁ (U.₁ f))) A'.∘ η' ≡⟨ A'.extendl (A'.extendr (U'.weave (α.is-natural _ _ _))) ⟩≡
      (U'.₁ (Y.₁ ε) A'.∘ U'.₁ (Y.₁ (F.₁ (U.₁ f)))) A'.∘ U'.₁ (α.η _) A'.∘ η'        ≡⟨ A'.pushl (U'.weave (Y.weave (F⊣U.counit.is-natural _ _ f))) ⟩≡
      U'.₁ (Y.₁ f) A'.∘ U'.₁ (Y.₁ ε) A'.∘ U'.₁ (α.η _) A'.∘ η'                      ∎

By some rather tedious applications of the triangle identities, we can calculate that the operations mate and mate-inv are inverse equivalences.

  mate-invl : ∀ (α : (F' F∘ X) => (Y F∘ F)) → mate (mate-inv α) ≡ α
  mate-invl α = ext λ _ →
    ε' B'.∘ ⌜ F'.₁ (U'.₁ (Y.₁ ε) A'.∘ U'.₁ (α.η _) A'.∘ η') ⌝ B'.∘ F'.₁ (X.₁ η)           ≡⟨ ap! (F'.F-∘ _ _ ∙ (ap₂ B'._∘_ refl (F'.F-∘ _ _))) ⟩≡
    ε' B'.∘ (F'.₁ (U'.₁ (Y.₁ ε)) B'.∘ F'.₁ (U'.₁ (α.η _)) B'.∘ F'.₁ η') B'.∘ F'.₁ (X.₁ η) ≡⟨ B'.extendl (B'.pulll (F'⊣U'.counit.is-natural _ _ _)) ⟩≡
    (Y.₁ ε B'.∘ ε') B'.∘ (F'.₁ (U'.₁ (α.η _)) B'.∘ F'.₁ η') B'.∘ F'.₁ (X.₁ η)             ≡⟨ B'.extendl (B'.pulll (B'.pullr (F'⊣U'.counit.is-natural _ _ _))) ⟩≡
    (Y.₁ ε B'.∘ α.η _ B'.∘ ε') B'.∘ F'.₁ η' B'.∘ F'.₁ (X.₁ η)                             ≡⟨ B'.pulll (B'.pullr (B'.cancelr F'⊣U'.zig)) ⟩≡
    (Y.₁ ε B'.∘ α.η _) B'.∘ F'.₁ (X.₁ η)                                                  ≡⟨ B'.pullr (α.is-natural _ _ _) ⟩≡
    Y.₁ ε B'.∘ Y.₁ (F.₁ η) B'.∘ α.η _                                                     ≡⟨ B'.cancell (Y.annihilate F⊣U.zig) ⟩≡
    α.η _                                                                                 ∎
    where module α = _=>_ α

  mate-invr : ∀ (α : (X F∘ U) => (U' F∘ Y)) → mate-inv (mate α) ≡ α
  mate-invr α = ext λ _ →
    U'.₁ (Y.₁ ε) A'.∘ ⌜ U'.₁ (ε' B'.∘ F'.₁ (α.η _) B'.∘ F'.₁ (X.₁ η)) ⌝ A'.∘ η'           ≡⟨ ap! (U'.F-∘ _ _ ∙ (ap₂ A'._∘_ refl (U'.F-∘ _ _))) ⟩≡
    U'.₁ (Y.₁ ε) A'.∘ (U'.₁ ε' A'.∘ U'.₁ (F'.₁ (α.η _)) A'.∘ U'.₁ (F'.₁ (X.₁ η))) A'.∘ η' ≡⟨ ap₂ A'._∘_ refl (A'.extendr (A'.pullr (sym (F'⊣U'.unit.is-natural _ _ _)))) ⟩≡
    U'.₁ (Y.₁ ε) A'.∘ (U'.₁ ε' A'.∘ U'.₁ (F'.₁ (α.η _))) A'.∘ η' A'.∘ X.₁ η               ≡⟨ ap₂ A'._∘_ refl (A'.pullr (A'.extendl (sym (F'⊣U'.unit.is-natural _ _ _)))) ⟩≡
    U'.₁ (Y.₁ ε) A'.∘ U'.₁ ε' A'.∘ η' A'.∘ α.η _ A'.∘ X.₁ η                               ≡⟨ ap₂ A'._∘_ refl (A'.cancell F'⊣U'.zag) ⟩≡
    U'.₁ (Y.₁ ε) A'.∘ α.η _ A'.∘ X.₁ η                                                    ≡⟨ A'.pulll (sym (α.is-natural _ _ _)) ⟩≡
    (α.η _ A'.∘ X.₁ (U.₁ ε)) A'.∘ X.₁ η                                                   ≡⟨ A'.cancelr (X.annihilate F⊣U.zag) ⟩≡
    α.η _                                                                                 ∎
    where module α = _=>_ α

  mate-is-equiv : is-equiv mate
  mate-is-equiv = is-iso→is-equiv (iso mate-inv mate-invl mate-invr)