Unit law for a monad algebra (source code)

= Unit law for a monad algebra
{title2=$a\eta_X=1_X$}

For an <algebra for a monad> $(X,a)$, its action $a:TX\to X$ satisfies $a\eta_X=1_X$.