CatDat

Quotients of effective congruences are strict quotients

Proof. Suppose we have $h : X \to Z$ so that we have a cartesian square $$\begin{CD} E @> f >> X \\ @V g VV @VV h V \\ X @>> h > Z. \end{CD}$$ Then by the universal property of the coequalizer, there is a unique morphism $$\bar h : X/E \to Z$$ such that $h = \bar h \circ p$. Now suppose we have generalized elements $x_1, x_2 : T \rightrightarrows X$ such that $p \circ x_1 = p \circ x_2$. Then $$h \circ x_1 = \bar h \circ p \circ x_1 = \bar h \circ p \circ x_2 = h \circ x_2,$$ so the pair $x_1, x_2$ factors through $f, g : E \rightrightarrows X$. The uniqueness of the factorization follows from the assumption that $E$ is a congruence, so $f, g$ are jointly monomorphic. $\square$