module Cat.Functor.Adjoint.Mate where

MatesπŸ”—

Let F⊣U:Aβ†’BF \dashv U : A \to B, Fβ€²βŠ£Uβ€²:Aβ€²β†’Bβ€²F' \dashv U' : A' \to B' be a pair of adjunctions, and let X:Aβ†’Aβ€²X : A \to A' and Y:Bβ†’Bβ€²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β†’Uβ€²YXU \to U'Y and Fβ€²Xβ†’YFF'X \to YF, which in one direction sends

to

We call natural transformations Ξ±:XUβ†’Uβ€²Y\alpha : XU \to U'Y and Ξ²:Fβ€²Xβ†’YF\beta : F'X \to YF mates, with respect to the adjunctions F⊣UF \dashv U and Fβ€²βŠ£Uβ€²F' \dashv U', if they correspond under this equivalence.

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 α:XU→U′Y\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 β:F′X→YF\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)