Proposition 5.4. Assuming that:

$C$ a category
$𝕋$ a monad

Then the forgetful functor

C^{𝕋} \overset{G^{𝕋}}{\to} C

has a left adjoint

F^{𝕋}

, and the adjunction induces the monad

𝕋

.