category_theory.reflective

A functor is reflective, or a reflective inclusion, if it is fully faithful and right adjoint.

category_theory.monadic_right_adjoint

A right adjoint functor R : D тед C is monadic if the comparison function monad.comparison R from D to the category of Eilenberg-Moore algebras for the adjunction is an equivalence.

category_theory.monadic_of_reflective

Any reflective inclusion has a monadic right adjoint. cf Prop 5.3.3 of [Riehl][riehl2017]