= Monadic tower for nested partial unary operations
{title2=$\ell=m-n$}
For the <nested partial unary operation category> tower, each one-step forgetful <functor> is a <monadic adjunction> right adjoint: it reflects <isomorphisms> and creates its split <coequalizers>. The <Beck monadicity theorem> identifies the first <Eilenberg-Moore category> with the next category in the tower. A long composite has that same first <monad> because <free extension of nested partial unary operations> leaves no new top fixed points. Repeating the comparison forgets one fewer operation at each step. The remaining forgetful functor is not full until no operation remains to forget, giving <monadic length> $m-n$.
Back to article page
