open import Cat.Functor.Equivalence
open import Cat.Prelude

open Functor
open _=>_

An adjunction $F \dashv G$ between functors $F : C \to D$ and $G : 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
{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

LβR : Monad C

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

Comparison : Functor D (Eilenberg-Moore C LβR)
Comparison .Fβ x = R.β x , alg where
alg : Algebra-on C LβR (R.β x)
alg .Algebra-on.Ξ½ = R.β (adj.counit.Ξ΅ _)
alg .Algebra-on.Ξ½-unit = adj.zag
alg .Algebra-on.Ξ½-mult =
R.β (adj.counit.Ξ΅ _) C.β Mβ (R.β (adj.counit.Ξ΅ _))        β‘
R.β (adj.counit.Ξ΅ _ D.β L.β (R.β (adj.counit.Ξ΅ _)))
R.β (adj.counit.Ξ΅ x D.β adj.counit.Ξ΅ (L.β (R.β x)))       β‘
R.β (adj.counit.Ξ΅ x) C.β R.β (adj.counit.Ξ΅ (L.β (R.β x))) β
Construction of the functorial action of Comparison
Comparison .Fβ x = hom where
open Algebra-hom
hom : Algebra-hom C _ _ _
hom .morphism = R.β x
hom .commutes =
R.β x C.β R.β (adj.counit.Ξ΅ _)        β‘
R.β (x D.β adj.counit.Ξ΅ _)
R.β (adj.counit.Ξ΅ _ D.β L.β (R.β x))  β‘
R.β (adj.counit.Ξ΅ _) C.β Mβ (R.β x)   β
Comparison .F-id    = Algebra-hom-path _ R.F-id
Comparison .F-β f g = Algebra-hom-path _ (R.F-β _ _)

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

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