Monadic length

When each comparison functor has a left adjoint, iterating the Eilenberg-Moore comparison functor produces the monadic tower. Its monadic length is the least number of comparison steps needed to reach an equivalence; an equivalence has length zero and a non-equivalence that is already monadic has length one.

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$.