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 {x} = path where abstract
path : R.β (adj.counit.Ξ΅ (L.Fβ x)) C.β R.β (L.β (adj.unit.Ξ· x)) β‘ C.id
path =