open import Cat.Functor.Adjoint
open import Cat.Diagram.Monad
open import Cat.Prelude

open Functor
open Monad
open _=>_

The Monad from an AdjunctionπŸ”—

module
  Cat.Functor.Adjoint.Monad
  {o₁ h₁ oβ‚‚ hβ‚‚ : _}
  {C : Precategory o₁ h₁}
  {D : Precategory oβ‚‚ hβ‚‚}
  {L : Functor C D} {R : Functor D C}
  (L⊣R : L ⊣ R)
  where

private
  module C = Precategory C
  module D = Precategory D
  module L = Functor L
  module R = Functor R
  module adj = _⊣_ L⊣R

Every adjunction L⊣RL \dashv R gives rise to a monad, where the underlying functor is R∘LR \circ L.

Adjunction→Monad : Monad C
Adjunctionβ†’Monad .M = R F∘ L

The unit of the monad is just adjunction monad, and the multiplication comes from the counit.

Adjunction→Monad .unit = adj.unit
Adjunctionβ†’Monad .mult = NT (Ξ» x β†’ R.₁ (Ξ· adj.counit (L.β‚€ x))) Ξ» x y f β†’
  R.₁ (adj.counit.Ξ΅ (L.β‚€ y)) C.∘ R.₁ (L.₁ (R.₁ (L.₁ f))) β‰‘βŸ¨ sym (R.F-∘ _ _) βŸ©β‰‘
  R.₁ (adj.counit.Ξ΅ (L.β‚€ y) D.∘ L.₁ (R.₁ (L.₁ f)))       β‰‘βŸ¨ ap R.₁ (adj.counit.is-natural _ _ _) βŸ©β‰‘
  R.₁ (L.₁ f D.∘ adj.counit.Ξ΅ (L.β‚€ x))                   β‰‘βŸ¨ R.F-∘ _ _ βŸ©β‰‘
  _                                                      ∎

The monad laws follow from the zig-zag identities. In fact, the right-identity law is exactly the zag identity.

Adjunction→Monad .right-ident {x} = adj.zag

The others are slightly more involved.

Adjunction→Monad .left-ident {x} = path where abstract
  path : R.₁ (adj.counit.Ξ΅ (L.Fβ‚€ x)) C.∘ R.₁ (L.₁ (adj.unit.Ξ· x)) ≑ C.id
  path =
    R.₁ (adj.counit.Ξ΅ _) C.∘ R.₁ (L.₁ (adj.unit.Ξ· _)) β‰‘βŸ¨ sym (R.F-∘ _ _) βŸ©β‰‘
    R.₁ (adj.counit.Ξ΅ _ D.∘ L.₁ (adj.unit.Ξ· _))       β‰‘βŸ¨ ap R.₁ adj.zig βŸ©β‰‘
    R.₁ D.id                                          β‰‘βŸ¨ R.F-id βŸ©β‰‘
    C.id                                              ∎

Adjunction→Monad .mult-assoc {x} = path where abstract
  path : R.₁ (adj.counit.Ξ΅ _) C.∘ R.₁ (L.₁ (R.₁ (adj.counit.Ξ΅ (L.Fβ‚€ x))))
       ≑ R.₁ (adj.counit.Ξ΅ _) C.∘ R.₁ (adj.counit.Ξ΅ (L .Fβ‚€ (R.Fβ‚€ (L.Fβ‚€ x))))
  path =
    R.₁ (adj.counit.Ξ΅ _) C.∘ R.₁ (L.₁ (R.₁ (adj.counit.Ξ΅ _)))   β‰‘βŸ¨ sym (R.F-∘ _ _) βŸ©β‰‘
    R.₁ (adj.counit.Ξ΅ _ D.∘ L.₁ (R.₁ (adj.counit.Ξ΅ _)))         β‰‘βŸ¨ ap R.₁ (adj.counit.is-natural _ _ _) βŸ©β‰‘
    R.₁ (adj.counit.Ξ΅ _ D.∘ adj.counit.Ξ΅ _)                     β‰‘βŸ¨ R.F-∘ _ _ βŸ©β‰‘
    R.₁ (adj.counit.Ξ΅ _) C.∘ R.₁ (adj.counit.Ξ΅ _)               ∎