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

open Functor
open _=>_


module
{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


Every adjunction $L \dashv R$ gives rise to a monad, where the underlying functor is $R \circ L$.

Adjunction→Monad : Monad C


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 =
R.₁ (adj.counit.ε _) C.∘ R.₁ (L.₁ (adj.unit.η _)) ≡⟨ sym (R.F-∘ _ _) ⟩≡