Split coequalizer (source code)

= Split coequalizer
{title2=$qf=qg,\ qs=1,\ ft=1,\ gt=sq$}

For parallel arrows $f,g:B\rightrightarrows C$, a split coequalizer consists of $q:C\to Q$ and arrows $s:Q\to C$, $t:C\to B$ with $qf=qg$, $qs=1_Q$, $ft=1_C$, and $gt=sq$. These equations prove the <coequalizer> property: if $uf=ug$, then $u=uft=ugt=usq$, so $us$ is the unique factor through $q$. Every <functor> preserves this split coequalizer because it preserves these equations.