Full comparison and reflection of split coequalizers (source code)

= Full comparison and reflection of split coequalizers
{title2=$K\text{ full and faithful}\iff G\text{ reflects G-split coequalizers}$}

For an adjunction $F\dashv G$, applying $G$ to its standard counit presentation gives $T^2GD\rightrightarrows TGD\to GD$, split by the monad units. Reflection therefore makes every counit presentation a coequalizer and gives full faithfulness by descent. Conversely, <monad algebra forgetful functor creates split coequalizers> makes an existing G-split quotient a coequalizer in the Eilenberg-Moore category. Fullness and faithfulness of the comparison lift its universal factorization back to the original category.