open import Cat.Functor.Adjoint.Monad
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



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.Ξ½-mult =

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.Ξ΅ _)        β‘β¨ sym (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 _

_ = Algebra