Satisfaction of Peano postulates in topos with natural numbers object Let $\mathcal{T}$ a topos with a natural numbers object, noted $N$. Also assume that $\mathcal{T}$ is not degenerate, meaning that its initial and terminal objects $\emptyset$ and $*$ are not isomorphic. I am trying to prove the satisfaction of the first Peano axiom in $N$: $ \forall n, S n \neq 0 $. If we interpret this axiom as forall morphism $n : * \to N$, $Sn\neq 0$, I managed to prove it as follows. Assume by contradiction that there is an $n : * \to N$ such as $S n = 0 $. Define the predecessor morphism $pred : N \to N$ by recursion in the NNO. By composition with $pred$ we get $n=0$, and then $S0=0$. Again we define by recursion the morphism $h:N\to\Omega$ such as $h0 = \bot$ and $hS = \lnot h$. This finally yields $\bot=\top$ and $\mathcal{T}$ degenerate, which is our contradiction.
My problem is there is another interpretation of the Peano axiom $ \forall n, S n \neq 0 $ in terms of subobjects of $N$. It seems to me that the subobject $A=\{n:N \;|\; S n = 0\}$ is the pullback of $(id,id) : N \to N^2$ and $(0,S): N \to N^2$. Then the satisfaction of the Peano axiom amounts to proving that this pullback is initial, i.e. the smallest subobject of $N$, $\emptyset \to N$. And that I failed to prove. Some of the proof above with an element $n:*\to N$ can be reused, and yields that the 2 morphisms of the pullback are equal $A \to N$ (hence both monic). But that is not enough to conclude that this monomorphism factors through any other subobject of $N$.
Is it possible to finish the second proof ? If not, why is the first interpretation of the Peano axiom better than the second ?
 A: Let's consider the internalisation of this statement. In other words, consider the meaning of the statement $\forall n \in N (Sn \neq 0)$ in the internal logic of the topos. Your version of the internalisation is technically equivalent to the correct version, but there's an even simpler version: that the pullback of $z : 1 \to N$ and $s : N \to N$ is $0$. It's easy to verify that this is equivalent to your version.
Note that in set theory, the statement that the pullback of $z$ and $s$ is $0$ is equivalent to saying that $\{(x, y) \mid x \in 1, y \in N, zx = sy\} = \emptyset$. In other words, there is no $y$ such that $sy = 0$.
Generally, we prove something even stronger; that $(N, z, s)$ is the coproduct of $1$ and $N$.
To do this, we consider the coproduct $1 + N$ of $1$ and $N$ with injections $i_1 : 1 \to N$, $i_N : N \to N$. We then explicitly construct an isomorphism $1 + N \to N$ and its inverse $N \to 1 + N$.
To construct the map $f : 1 + N \to N$, we simply take the $f$ such that $f \circ i_1 = z$, $f \circ i_2 = s$.
To construct the inverse map, first define $s' : 1 + N \to 1 + N$ such that $s' \circ i_1 = i_2 \circ z$ and $s' \circ i_2 = i_2 \circ s$. For convenience, let $z' = i_1$. We then take the unique $g : N \to 1 + N$ such that $g \circ z = z'$ and $g \circ s = s' \circ g$.
We will now show that $g \circ f = 1_{1 + N}$. To do this, it suffices to show that $g \circ f \circ i_j = i_j$ for $j = 1, 2$.
First, I claim that $g \circ f \circ i_2 = i_2$. To do this, we first rewrite $g \circ f \circ i_2 = g \circ s = s' \circ g$. Now note that $s' \circ g \circ z = s' \circ z' = s' \circ i_1 = i_2 \circ z$. And also note that $s' \circ g \circ s = s' \circ s' \circ g$. We also have $i_2 \circ z = i_2 \circ z$ and $i_2 \circ s = s' \circ i_2$, so by the universal property of the NNO, we have $s' \circ g = i_2$ as required.
Now, note that $g \circ f \circ i_1 = g \circ z = z' = i_1$. Therefore, we may indeed conclude that $g \circ f = 1_{1 + N}$.
I conversely claim that $f \circ g = 1_N$. To do this, it suffices to show that $f \circ g \circ z = z$ and that $f \circ g \circ s = s \circ f \circ g$ and then cite the universal property of the NNO.
For the first part of this, we see clearly that $f \circ g \circ z = f \circ z' = f \circ i_1 = z$.
For the second part, we first show that $f \circ s' = s \circ f$. To do this, note that $f \circ s' \circ i_1 = f \circ i_2 \circ z = s \circ z = s \circ f \circ i_1$. And note that $f \circ s' \circ i_2 = f \circ i_2 \circ s = s \circ s = s \circ f \circ i_2$. Apply the universal property of the coproduct to conclude that $f \circ s' = s \circ f$.
Now, we note that $f \circ g \circ s = f \circ s' \circ g = s \circ f \circ g$.
So we indeed see that $f$ and $g$ are inverse isomorphisms $1 + N \cong N$. Furthermore, we see that $f \circ i_1 = z$ and $f \circ i_2 = s$, so therefore $(N, z, s)$ is a coproduct.
To finish the proof, we then cite the fact that in a topos, the injection maps for a coproduct are disjoint (see eg. Sheaves in Geometry and Logic Corollary IV.10.3). This shows us that $0$ is indeed the pullback of $z$ and $s$.
Note that this proof also gives you another Peano axiom for free. For we can conclude from here that since $s$ is a coproduct injection, it must be mono (again citing Corollary IV.10.3 which also states that coproduct injections are mono). And $s$ being mono is exactly the internalisation of the claim that $\forall n, m \in N (sn = sm \to n = m)$.
