A Universe of Sorts

A fuctor $U: D \to C$ is monadic iff it has a left adjoint $F: C \to D$ and the adjunction is monadic.
An adjunction $C : F \vdash U: D$ is monadic if the induced "comparison functor" from $D$ to the category of algebras (eilenberg-moore category) $C^T$ is an equivalence of categories .
That is, the functor $\phi: D \to C^T$ is an equivalence of categories.
Some notes: We have $D \to C^T$ and not the other way around since the full order is $C_T \to D \to C^T$ : Kleisli, to $D$ , to Eilenberg moore. We go from "more semantics" to "less semantics" --- such induced functors cannot "add structure" (by increasing the amount of semantics), but they can "embed" more semantics into less semantics. Thus, there is a comparison functor from $D$ to $C^T$ .
Eilenberg-moore is written $C^T$ since the category consists of $T$ -algebras, where $T$ is the induced monad $T: C \to D \to C$ . It's $C^T$ because a $T$ algebra consists of arrows $\{ Tc \to c : c \in C \}$ with some laws. If one wished to be cute, the could think of this as " $T \to C$ ".
The monad $T$ is $C \to C$ and not $D \to D$ because, well, let's pick a concrete example: Mon. The monad on the set side takes a set $S$ to the set of words on $S$ , written $S^\star$ . The other alleged "monad" takes a monoid $M$ to the free monoid on the element of $M$ . We've lost structure.

§ Monadic Functor