open import Cat.Functor.Adjoint.Monad
open import Cat.Functor.Equivalence
open import Cat.Displayed.Total
open import Cat.Functor.Adjoint
open import Cat.Diagram.Monad
open import Cat.Prelude

import Cat.Functor.Reasoning
import Cat.Reasoning

open Total-hom
open Functor
open _=>_

Monadic adjunctions🔗

An adjunction $L⊣R$ between functors $L:C\to D$ and $R:D\to C$ is monadic if the induced comparison functor $D\to C^{R\circ L}$ (where the right-hand side is the Eilenberg-Moore category of the monad of the adjunction) is an equivalence of categories.

module
  Cat.Functor.Adjoint.Monadic
  {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 = Cat.Reasoning C
  module D = Cat.Reasoning D
  module L = Cat.Functor.Reasoning L
  module R = Cat.Functor.Reasoning R
  module adj = _⊣_ L⊣R

R∘L : Monad-on _
R∘L = Adjunction→Monad L⊣R

open Monad-on R∘L

_ = Algebra

The composition of R.₁ with the adjunction counit natural transformation gives R an Algebra structure, thus extending R to a functor $D\to C^{R\circ L}\text{.}$

Comparison-EM : Functor D (Eilenberg-Moore R∘L)
Comparison-EM .F₀ x = R.₀ x , alg where
  alg : Algebra-on R∘L (R.₀ x)
  alg .Algebra-on.ν = R.₁ (adj.counit.ε _)
  alg .Algebra-on.ν-unit = adj.zag
  alg .Algebra-on.ν-mult = R.weave (adj.counit.is-natural _ _ _)

Comparison-EM .F₁ x .hom = R.₁ x
Comparison-EM .F₁ x .preserves = R.weave (sym (adj.counit.is-natural _ _ _))
Comparison-EM .F-id    = ext R.F-id
Comparison-EM .F-∘ f g = ext (R.F-∘ _ _)

An adjunction is monadic if Comparison-EM is an equivalence of categories, thus exhibiting $C$ as the category of $R\circ L\text{-algebras:}$

is-monadic : Type _
is-monadic = is-equivalence Comparison-EM