Monadic length
= 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.