Supplied created canonical presentations give a quasi-inverse to the comparison functor

For a $T$-algebra $(A,a)$, the pair $F(TA)\rightrightarrows F(A)$ with arrows $F(a)$ and ${\epsilon }_{FA}$ has under $U$ the canonical pair $T(a),{\mu }_A:T^{2}A\rightrightarrows TA$. By [L2] and [L3] it is $U$-split.

Let $q_A:F(A)\to H(A,a)$ be the created coequalizer supplied for $(A,a)$. Its image is isomorphic to the canonical base coequalizer from step 1.1, and the universal property fixes the resulting comparisons.

An algebra homomorphism $r:(A,a)\to (B,b)$ carries the canonical pair for $A$ to that for $B$. The two coequalizer universal properties therefore define a unique morphism $H(r):H(A,a)\to H(B,b)$, and uniqueness proves preservation of identities and composition.

For $d\in \mathcal{D}$, the counit fork $F(TUd)\rightrightarrows F(Ud)\stackrel{{\epsilon }_d}{\to }d$ maps under $U$ to the canonical split presentation of $K(d)$. Creation reflects the lifted coequalizer, so comparison with $q_{K(d)}$ yields an isomorphism $HK(d)\cong d$.

The underlying fork of $K(q_A)$ is a split coequalizer, transported from the canonical split fork along the isomorphism supplied by ordinary creation. Since $K(q_A)$ is a lift of that fork, [L4] makes it a coequalizer in ${\mathcal{C}}^T$. The map $a:TA\to A$ is the other canonical algebra coequalizer by [L5], so their universal properties produce a unique isomorphism $KH(A,a)\cong (A,a)$.

The defining equations for the comparisons in steps 3.3 and 3.2 commute with every algebra homomorphism and every morphism of $\mathcal{D}$. Uniqueness of maps out of the coequalizers therefore makes both families natural, proving the two displayed natural isomorphisms.