Inheritance of effective congruences in coslice categories

Proof. Let $f, g : E \rightrightarrows X$ be a congruence in $\C$. We then construct a congruence on $A+X$ in $A \backslash \C$. On an intuitive level, this will be the congruence generated by $a \sim a$ for $a\in A$ and $x \sim y$ for $(x, y) \in E$. More precisely, we will show the two maps

$$\id_A + f,\, \id_A + g : A+E \rightrightarrows A+X$$

form a congruence. To show the pair of maps is jointly monomorphic, we use extensivity to split the domains of the generalized elements, so without loss of generality we may assume each comes from either $A$ or $E$. Reflexivity and symmetry are straightforward; and for transitivity, we again use extensivity to split the domains of the generalized elements, and provide an argument on each subdomain where the three generalized elements all come from either $A$ or $E$.

Now if this congruence is the kernel pair of $h : A+X \to Z$ in $A \backslash \C$, then $E$ is the kernel pair of $h \circ i_2 : X \to Z$ in $\C$. Namely, if we have two generalized elements $x_1, x_2 : T \rightrightarrows X$ such that $h \circ i_2 \circ x_1 = h \circ i_2 \circ x_2$, then we can construct a pair of maps

$$\id_A + x_1,\, \id_A + x_2 : A+T \rightrightarrows A+X$$

in $A \backslash \C$ with $h \circ (\id_A + x_1) = h \circ (\id_A + x_2)$. Therefore, $\id_A + x_1, \id_A + x_2$ factor through $A+E$ in $A \backslash \C$, so $x_1, x_2$ factor through $A+E$ in $\C$; and using disjoint coproducts, we may conclude that $x_1, x_2$ factor through $E$. $\square$