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

import Cat.Functor.Reasoning
import Cat.Reasoning

module Cat.Functor.Adjoint.Mate where


# Matesπ

Let be a pair of adjunctions, and let and 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 and which in one direction sends

to

We call natural transformations and mates, with respect to the adjunctions and 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 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

  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)