Definition 5.15 (Monadic tower). Let $C\underset{G}{\overset{F}{\rightleftarrows }}D$ be an adjunction where $D$ has reflexive coequalisers. The monadic tower of $(F⊣G)$ is the diagram

where $𝕋$ is the monad induced by $(F⊣G)$, and $K$ and $L$ are as in Theorem 5.7 and Lemma 5.9, and $𝕊$ is the monad induced by $(L⊣K)$ and so on.

We say $(F⊣G)$ has monadic length $n$ if we reach an equivalence after $n$ steps.