Power objects turn coreflexive equalizers into coequalizers (source code)

= Power objects turn coreflexive equalizers into coequalizers
{title2=$PA\rightrightarrows PB\xrightarrow{Pe}PE$}

For a <coreflexive pair> $f,g:B\rightrightarrows A$ with equalizer $e:E\hookrightarrow B$, direct image along the mono $f$ satisfies $Pf\,\exists_f=1$ and $Pg\,\exists_f=\exists_e Pe$. Thus any map $h:PB\to Z$ equalizing $Pf,Pg$ obeys $h=h\exists_e Pe$. Since $Pe\exists_e=1$, the map $Pe$ is their <coequalizer>. These identities hold for parameterized subobjects in any <elementary topos>.