Equalizer presentation by powers of a coseparator (source code)

= Equalizer presentation by powers of a coseparator
{title2=$B\longrightarrow S^I\rightrightarrows S^J$}

In a <complete category> that is a <locally small category> with a <coseparator> $S$, suppose every <monomorphism> is a <regular monomorphism>. The evaluation embedding $B\to S^I$, $I=\mathcal C(B,S)$, is an <equalizer> of some pair into $Q$. Composing that pair with the evaluation embedding $Q\to S^J$ leaves the <equalizer> unchanged. Here powers mean <products in a category> indexed by sets, without assuming an <exponential object> exists.