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

import Cat.Functor.Reasoning as Func
import Cat.Reasoning as Cat

module Cat.Functor.Adjoint.Hom
  {o β„“ oβ€² β„“β€²} {C : Precategory o β„“} {D : Precategory oβ€² β„“β€²}
  {L : Functor D C} {R : Functor C D}
  where

Adjoints as hom-isomorphismsπŸ”—

Recall from the page on adjoint functors that an adjoint pair L⊣RL \dashv R induces an isomorphism

HomC(L(x),y)β‰…HomD(x,R(y)) {\mathbf{Hom}}_\mathcal{C}(L(x), y) \cong {\mathbf{Hom}}_\mathcal{D}(x, R(y))

of Hom{\mathbf{Hom}}-sets, sending each morphism to its left and right adjuncts, respectively. What that page does not mention is that any functors L,RL, R with such a correspondence β€” as long as the isomorphism is natural β€” actually generates an adjunction L⊣RL \dashv R, with the unit and counit given by the adjuncts of each identity morphism.

More precisely, the data we require is an equivalence (of sets) f:HomC(Lx,y)β†’HomD(x,Ry)f : {\mathbf{Hom}}_\mathcal{C}(Lx,y) \to {\mathbf{Hom}}_\mathcal{D}(x,Ry) such that the equation

f(g∘x∘Lh)=Rg∘fx∘h f(g \circ x \circ Lh) = Rg \circ fx \circ h

holds. While this may seem un-motivated, it’s really a naturality square for a transformation between the functors HomC(Lβˆ’,βˆ’){\mathbf{Hom}}_\mathcal{C}(L-,-) and HomD(βˆ’,Rβˆ’){\mathbf{Hom}}_\mathcal{D}(-,R-) whose data has been β€œunfolded” into elementary terms.

hom-iso-natural
  : (βˆ€ {x y} β†’ C.Hom (L.β‚€ x) y β†’ D.Hom x (R.β‚€ y))
  β†’ Type _
hom-iso-natural f =
  βˆ€ {a b c d} (g : C.Hom a b) (h : D.Hom c d) x
  β†’ f (g C.∘ x C.∘ L.₁ h) ≑ R.₁ g D.∘ f x D.∘ h

hom-iso→adjoints
  : (f : βˆ€ {x y} β†’ C.Hom (L.β‚€ x) y β†’ D.Hom x (R.β‚€ y))
  β†’ (eqv : βˆ€ {x y} β†’ is-equiv (f {x} {y}))
  β†’ hom-iso-natural f
  β†’ L ⊣ R
hom-iso→adjoints f f-equiv natural = adj′ where
  f⁻¹ : βˆ€ {x y} β†’ D.Hom x (R.β‚€ y) β†’ C.Hom (L.β‚€ x) y
  f⁻¹ = equivβ†’inverse f-equiv

  inv-natural : βˆ€ {a b c d} (g : C.Hom a b) (h : D.Hom c d) x
              β†’ f⁻¹ (R.₁ g D.∘ x D.∘ h) ≑ g C.∘ f⁻¹ x C.∘ L.₁ h
  inv-natural g h x = ap fst $ is-contr→is-prop (f-equiv .is-eqv _)
    (f⁻¹ (R.₁ g D.∘ x D.∘ h) , refl)
    ( g C.∘ f⁻¹ x C.∘ L.₁ h
    , natural _ _ _
    βˆ™ sym (equivβ†’counit f-equiv _)
    βˆ™ ap (f βŠ™ f⁻¹)
         (D.extendl (ap (R.₁ g D.∘_) (equivβ†’counit f-equiv _))))

We do not require an explicit naturality witness for the inverse of ff, since if a natural transformation is componentwise invertible, then its inverse is natural as well. It remains to use our β€œbinaturality” to compute that f(id)f({{\mathrm{id}}_{}}) and fβˆ’1(id)f^{-1}({{\mathrm{id}}_{}}) do indeed give a system of adjunction units and co-units.

  adjβ€² : L ⊣ R
  adjβ€² .unit .Ξ· x = f C.id
  adjβ€² .unit .is-natural x y h =
    f C.id D.∘ h                    β‰‘βŸ¨ D.introl R.F-id βŸ©β‰‘
    R.₁ C.id D.∘ f C.id D.∘ h       β‰‘Λ˜βŸ¨ natural _ _ _ βŸ©β‰‘Λ˜
    f (C.id C.∘ C.id C.∘ L.₁ h)     β‰‘βŸ¨ ap f (C.cancell (C.idl _) βˆ™ C.intror (C.idl _ βˆ™ L.F-id)) βŸ©β‰‘
    f (L.₁ h C.∘ C.id C.∘ L.₁ D.id) β‰‘βŸ¨ natural _ _ C.id βŸ©β‰‘
    R.₁ (L.₁ h) D.∘ f C.id D.∘ D.id β‰‘βŸ¨ D.refl⟩∘⟨ D.idr _ βŸ©β‰‘
    R.₁ (L.₁ h) D.∘ f C.id          ∎
  adjβ€² .counit .Ξ· x = f⁻¹ D.id
  adjβ€² .counit .is-natural x y f =
    f⁻¹ D.id C.∘ L.₁ (R.₁ f) β‰‘βŸ¨ C.introl refl βŸ©β‰‘
    C.id C.∘ f⁻¹ D.id C.∘ L.₁ (R.₁ f) β‰‘Λ˜βŸ¨ inv-natural _ _ _ βŸ©β‰‘Λ˜
    f⁻¹ (R.₁ C.id D.∘ D.id D.∘ R.₁ f) β‰‘βŸ¨ ap f⁻¹ (D.cancell (D.idr _ βˆ™ R.F-id) βˆ™ D.intror (D.idl _)) βŸ©β‰‘
    f⁻¹ (R.₁ f D.∘ D.id D.∘ D.id)     β‰‘βŸ¨ inv-natural _ _ _ βŸ©β‰‘
    f C.∘ f⁻¹ D.id C.∘ L.₁ D.id       β‰‘βŸ¨ C.refl⟩∘⟨ C.elimr L.F-id βŸ©β‰‘
    f C.∘ f⁻¹ D.id                    ∎
  adjβ€² .zig =
    f⁻¹ D.id C.∘ L.₁ (f C.id)          β‰‘βŸ¨ C.introl refl βŸ©β‰‘
    C.id C.∘ f⁻¹ D.id C.∘ L.₁ (f C.id) β‰‘Λ˜βŸ¨ inv-natural _ _ _ βŸ©β‰‘Λ˜
    f⁻¹ (R.₁ C.id D.∘ D.id D.∘ f C.id) β‰‘βŸ¨ ap f⁻¹ (D.cancell (D.idr _ βˆ™ R.F-id)) βŸ©β‰‘
    f⁻¹ (f C.id)                       β‰‘βŸ¨ equivβ†’unit f-equiv _ βŸ©β‰‘
    C.id                               ∎
  adjβ€² .zag =
    R.₁ (f⁻¹ D.id) D.∘ f C.id          β‰‘βŸ¨ D.refl⟩∘⟨ D.intror refl βŸ©β‰‘
    R.₁ (f⁻¹ D.id) D.∘ f C.id D.∘ D.id β‰‘Λ˜βŸ¨ natural _ _ _ βŸ©β‰‘Λ˜
    f (f⁻¹ D.id C.∘ C.id C.∘ L.₁ D.id) β‰‘βŸ¨ ap f (C.elimr (C.idl _ βˆ™ L.F-id)) βŸ©β‰‘
    f (f⁻¹ D.id)                       β‰‘βŸ¨ equivβ†’counit f-equiv _ βŸ©β‰‘
    D.id                               ∎