CatDat

Implication Details

Assumptions: full, monadic

Conclusions: equivalence

Reason: Assume that $T$ is a monad on $\mathcal{C}$ such that the forgetful functor $U : \mathbf{Alg}(T) \to \mathcal{C}$ is full. Then by general facts about adjunctions (see MSE/1994963) the unit $\eta : \mathrm{id}_{\mathcal{C}} \to T$ is an isomorphism of functors. Then it is an isomorphism of monads, so that $U$ is an equivalence.