Data-supplied crude monadicity theorem for reflexive coequalizers

For a $T$-algebra $(A,a)$, the pair $F(TA)\rightrightarrows F(A)$ used in canonical reconstruction has common section $F({\eta }_A)$: one composite is the algebra unit law and the other is the adjunction triangle identity. Hence it is reflexive by [L1].

Use the supplied coequalizer $q_A:F(A)\to H(A,a)$ of this reflexive pair. By hypothesis, applying $U$ preserves it.

The preserved coequalizer $U{q}_A$ and the split canonical base coequalizer in [L3] coequalize the same pair, so transport of the splitting makes the underlying fork of $K(q_A)$ split. By [L5], $K(q_A)$ is a coequalizer in ${\mathcal{C}}^T$; by [L4], so is the canonical fork ending at $(A,a)$. Their universal properties therefore give an isomorphism $KH(A,a)\cong (A,a)$.

For $d\in \mathcal{D}$, compare the coequalizer of the reflexive counit pair with the counit fork ending at $d$. Their images under $U$ are isomorphic canonical coequalizers, so the comparison morphism becomes an isomorphism under $U$ and is itself an isomorphism by [L2].

The supplied object assignment and coequalizer universality define $H$ on algebra homomorphisms, and uniqueness makes the comparisons in steps 3.1 and 4.1 natural. Thus $H$ is a quasi-inverse to $K$, so $K$ is an equivalence and $U$ is monadic.