module Cat.Functor.Adjoint.Hom where

module _ {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                               ∎
module _ {o β„“ oβ€²} {C : Precategory o β„“} {D : Precategory oβ€² β„“}
         {L : Functor D C} {R : Functor C D}
         where
  private
    module C = Cat C
    module D = Cat D
    module L = Func L
    module R = Func R


  hom-natural-iso→adjoints
    : natural-iso (Hom[-,-] C F∘ (Functor.op L FΓ— Id)) (Hom[-,-] D F∘ (Id FΓ— R))
    β†’ L ⊣ R
  hom-natural-iso→adjoints eta =
    hom-iso→adjoints (to .η _) (natural-iso-to-is-equiv eta (_ , _)) λ g h x →
      happly (to .is-natural _ _ (h , g)) x
    where
      open natural-iso eta
      open _=>_

module _ {o β„“ oβ€²} {C : Precategory o β„“} {D : Precategory oβ€² β„“}
         {L : Functor D C} {R : Functor C D}
         (adj : L ⊣ R)
         where
  private
    module C = Cat C
    module D = Cat D
    module L = Func L
    module R = Func R

  adjunct-hom-iso-from
    : βˆ€ a β†’ natural-iso (Hom-from C (L.β‚€ a)) (Hom-from D a F∘ R)
  adjunct-hom-iso-from a = to-natural-iso mi where
    open make-natural-iso

    mi : make-natural-iso (Hom-from C (L.β‚€ a)) (Hom-from D a F∘ R)
    mi .eta x = L-adjunct adj
    mi .inv x = R-adjunct adj
    mi .eta∘inv _ = funext Ξ» _ β†’ L-R-adjunct adj _
    mi .inv∘eta _ = funext Ξ» _ β†’ R-L-adjunct adj _
    mi .natural _ _ f = funext Ξ» g β†’ sym (L-adjunct-naturalr adj f g)

  adjunct-hom-iso-into
    : βˆ€ b β†’ natural-iso (Hom-into C b F∘ Functor.op L) (Hom-into D (R.β‚€ b))
  adjunct-hom-iso-into b = to-natural-iso mi where
    open make-natural-iso

    mi : make-natural-iso (Hom-into C b F∘ Functor.op L) (Hom-into D (R.β‚€ b))
    mi .eta x = L-adjunct adj
    mi .inv x = R-adjunct adj
    mi .eta∘inv _ = funext Ξ» _ β†’ L-R-adjunct adj _
    mi .inv∘eta _ = funext Ξ» _ β†’ R-L-adjunct adj _
    mi .natural _ _ f = funext Ξ» g β†’ sym $ L-adjunct-naturall adj g f

  adjunct-hom-iso
    : natural-iso (Hom[-,-] C F∘ (Functor.op L FΓ— Id)) (Hom[-,-] D F∘ (Id FΓ— R))
  adjunct-hom-iso = to-natural-iso mi where
    open make-natural-iso

    mi : make-natural-iso (Hom[-,-] C F∘ (Functor.op L FΓ— Id)) (Hom[-,-] D F∘ (Id FΓ— R))
    mi .eta x = L-adjunct adj
    mi .inv x = R-adjunct adj
    mi .eta∘inv _ = funext Ξ» _ β†’ L-R-adjunct adj _
    mi .inv∘eta _ = funext Ξ» _ β†’ R-L-adjunct adj _
    mi .natural _ _ (f , h) = funext Ξ» g β†’ sym $ L-adjunct-naturalβ‚‚ adj h f g