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 \dashv U : A \to B$, $F' \dashv U' : A' \to B'$ be a pair of adjunctions, and let $X : A \to A'$ and $Y : B \to B'$ 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'Y$ and $F'X \to YF$, which in one direction sends  to  We call natural transformations $\alpha : XU \to U'Y$ and $\beta : F'X \to YF$ mates, with respect to the adjunctions $F \dashv U$ and $F' \dashv U'$, 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'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'X \to YF$.

  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 α =
Nat-path λ _ →
ε' 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 α =
Nat-path λ _ →
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)