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.



Question about equivalence relation defining integers in an elementary topos
I think what you want first is a lemma that $\mathbb{N}$ is a cancellative monoid (which is the case in any topos). Just think about how you would prove your statement in the category of sets using ordinary elements, and I think it will become clear. 


The usual construction of the left adjoint to the forgetful functor from abelian groups to abelian monoids involves the observation that, for $m, n, m', n'$ in an abelian monoid $M$, the relation 


$$\exists\_{j \in M} m' + n + j = m + n' + j$$ 


defines an equivalence relation $\langle m, n \rangle \sim \langle m', n' \rangle$ on $M \times M$. (Only transitivity need be checked.) Cancellation means that from this we can infer 


$$m' + n = m + n'$$ 


which is what you want. 


We thus need to show 


$$\forall\_{j \in \mathbb{N}} ((x + j = y + j) \Rightarrow (x = y))$$ 


in the natural numbers object. This is done by induction on $j$ (the subobject of such $j$ contains 0 and ... and therefore is all of $\mathbb{N}$). 


