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⊣R$ gives rise to a monad, where the underlying functor is $R\circ L\text{.}$

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.ε (L.₀ x))) λ x y f →
  R.₁ (adj.ε (L.₀ y)) C.∘ R.₁ (L.₁ (R.₁ (L.₁ f))) ≡⟨ sym (R.F-∘ _ _) ⟩≡
  R.₁ (adj.ε (L.₀ y) D.∘ L.₁ (R.₁ (L.₁ f)))       ≡⟨ ap R.₁ (adj.counit.is-natural _ _ _) ⟩≡
  R.₁ (L.₁ f D.∘ adj.ε (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.ε (L.F₀ x)) C.∘ R.₁ (L.₁ (adj.η x)) ≡ C.id
  path =
    R.₁ (adj.ε _) C.∘ R.₁ (L.₁ (adj.η _)) ≡⟨ sym (R.F-∘ _ _) ⟩≡
    R.₁ (adj.ε _ D.∘ L.₁ (adj.η _))       ≡⟨ ap R.₁ adj.zig ⟩≡
    R.₁ D.id                              ≡⟨ R.F-id ⟩≡
    C.id                                  ∎

Adjunction→Monad .mult-assoc {x} = path where abstract
  path : R.₁ (adj.ε _) C.∘ R.₁ (L.₁ (R.₁ (adj.ε (L.F₀ x))))
       ≡ R.₁ (adj.ε _) C.∘ R.₁ (adj.ε (L .F₀ (R.F₀ (L.F₀ x))))
  path =
    R.₁ (adj.ε _) C.∘ R.₁ (L.₁ (R.₁ (adj.ε _)))   ≡⟨ sym (R.F-∘ _ _) ⟩≡
    R.₁ (adj.ε _ D.∘ L.₁ (R.₁ (adj.ε _)))         ≡⟨ ap R.₁ (adj.counit.is-natural _ _ _) ⟩≡
    R.₁ (adj.ε _ D.∘ adj.ε _)                     ≡⟨ R.F-∘ _ _ ⟩≡
    R.₁ (adj.ε _) C.∘ R.₁ (adj.ε _)               ∎