Hi all,

Let $\mathcal{E}$ be an elementary topos with natural number object $N$, and let $+: N \times N \to N$ be the the addition arrow; I expect that the nature of $N$ and $+$ will turn out to be irrelevant to my question, but if so they should at least make its motivation clear. Let $E$ be the pullback of $+$ along itself, with projections $p, q: E \to N \times N$; for example if $\mathcal{E}$ is the topos of sets then $E$ may simply be taken to be the set of quadruples $(n, m, n', m') \in N^4$ such that $n + m' = n' + m$, with $a(n, m, n', m') = (n, m')$, $b(n, m, n', m') = (n', m)$. Let $f_1, f_2: E \to N \times N$ be given by

$f_1 \equiv \left< p_1 a, p_2 b \right>$

$f_2 \equiv \left< p_1 b, p_2 a \right>$

(here $p_1, p_2: N \times N \to N$ are the projections and $\left< f, g \right>$ denotes the product arrow $X \to N \times N$ of arrows $f, g: X \to N$). For example in the topos of sets again, $f_1 (n, m, n', m') = (n, m)$ etc.. Let $c: N \times N \to Z$ be the coequaliser of $f_1$ and $f_2$, so $Z$ is the integer object in $\mathcal{E}$.

My question is: if $g, h, g', h': X \to N$ are such that $c \left< g, h \right> = c \left< g', h' \right>$, is it always the case that $+ \left< g, h' \right> = + \left< g', h \right>$? Equivalently, is $E$ with the arrows $f_1$, $f_2$ the pullback of $c$ along itself?

I've spent a while trying to prove it is but I just keep going round in circles, so any hints will be much appreciated.