Strict Beck monadicity theorem

For the forward direction, if $K$ is an isomorphism then $U=U^{T}K$ on the nose. Transport through the inverse functor of $K$ preserves the exact apex, legs, and uniqueness in [L2], so $U$ has the strict-creation property in [L3].

For the reverse direction, [L4] makes each lifted canonical pair $U$-split. Strict creation [L3] gives a unique object $H(A,a)$ of $\mathcal{D}$ on the prescribed underlying apex $A$ and a coequalizer whose underlying map is $a:TA\to A$. Uniqueness and the coequalizer universal property define $H$ on algebra homomorphisms.

The functor $K(H(A,a))$ and the given algebra $(A,a)$ are lifts of the same split base fork; [L2] and the canonical coequalizer [L5] make the lift unique, so $KH=1_{{\mathcal{C}}^T}$ on objects and morphisms. For $d\in \mathcal{D}$, its counit fork is the existing lift of the canonical split fork of $K(d)$, so strict uniqueness gives $HK(d)=d$ and the same equality on morphisms. Hence $H$ is a two-sided inverse of $K$, and $U$ is strictly monadic by [L1].

Step 1.1 proves the forward implication and steps 1.2 and 2.1 prove the reverse implication, establishing the biconditional.