Split equalizers associated with a monad (source code)

= Split equalizers associated with a monad
{title2=$\eta_{TA},\ T\eta_A$}

For a <monad> $(T,\eta,\mu)$, the map $\eta_{TA}:TA\to TTA$ is a <split equalizer> of $\eta_{TTA},T\eta_{TA}$ with retraction $\mu_A$ and splitting $T\mu_A$. The map $T\eta_A:TA\to TTA$ is a split equalizer of $TT\eta_A,T\eta_{TA}$ with retraction $\mu_A$ and splitting $\mu_{TA}$. Each assertion follows from the two unit laws and <naturality> of the unit or multiplication. No assumption that $T$ preserves arbitrary equalizers is needed.