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

import Cat.Functor.Reasoning
import Cat.Reasoning

open Total-hom
open Functor
open _=>_


An adjunction between functors and is monadic if the induced comparison functor (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 = Cat.Reasoning C
module D = Cat.Reasoning D
module L = Cat.Functor.Reasoning L
module R = Cat.Functor.Reasoning R
module adj = _β£_ Lβ£R

LβR : Monad C

private
module Kleisli = Cat.Reasoning (Kleisli LβR)
module EM = Cat.Reasoning (Eilenberg-Moore LβR)


The composition of R.β with the adjunction counit natural transformation gives R an Algebra structure, thus extending R to a functor

Comparison-EM : Functor D (Eilenberg-Moore LβR)
Comparison-EM .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.weave (adj.counit.is-natural _ _ _)

Construction of the functorial action of Comparison-EM
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 as the category of

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