Is the coproduct $N=1+N$ universal? Let $\mathcal{C}$ be a category with finite limits and a (parameterized) natural numbers object $(N,0,s)$. Let $1$ denote the terminal object of the category. It's easy to show that the following is a coproduct diagram.
$$ 1 \xrightarrow{0} N \xleftarrow{s} N $$
My question is: is this coproduct diagram necessarily universal?

Background
A coproduct $A+B$ is said to be universal if pulling it back along any morphism into $A+B$ gives a coproduct diagram. (See Introduction to extensive and distributive categories by Carboni and Walters, definition 2.10.)
Often, natural numbers objects are considered in the context of extensive categories, in which all coproducts are universal (see lemma 2.11 of the same paper). However, I'm curious whether this coproduct is universal even if the ambient category is not assumed to be extensive. I suspect it is not true, since I can't find a simple proof, but I'm not well versed enough to come up with a counter-example.
One reason to ask whether the coproduct is universal is because it allows the definition of certain functions "by cases". If we have an arrow $u : X \rightarrow N$, then we might want to define an arrow $f : X \rightarrow Y$ in a way that $f(x)$ is defined by cases, depending on whether $u(x) = 0$ or not. Doing this requires that we can write $X$ as the coproduct of $X_0$ and $X_{>0}$, where $X_0$ is the equalizer of $u$ and $0$, and $X_{>0}$ is the equalizer of $1{\dot -}u$ and $0$. It's not too hard to show that this is possible for any $u$ iff the coproduct $N=1+N$ is universal.
 A: The answer is no in general - but this is a fairly subtle issue. First, let's go over why this is "almost true".
Given $e:X \to N$ I denote by $X_0$ and $X_{>0}$ the pullback of $\{0\}$ and $N_{>0}$ along $e$.
So, given $N$ a parametrized NNO, and $f,g :X \to Y$ two functions, what you can easily do using the NNO property, is construct a function $h:X \times N \to Y$ such that $h(x,0)= f(x)$ and $h(x,Sn)=g(x)$.
And if on top of this you have a map $e:X \to N$ then you can define $h'(x)=h(x,e(x))$ which morally is defined $h'(x) = f(x)$ if $e(x)=0$ and $h'(x)=g(x)$ if $e(x)>0$. More precisely, its restriction to $X_0$ and $X_{>0}$ will coincide respectively with the restriction of $f$ and $g$.
But that doesn't quite give you a pushout because the maps $f$ and $g$ are defined on the whole of $X$ and not on $X_0$ and $X_{>0}$. If you have a way to somehow extend a map only defined on $X_0$ and $X_{>0}$ to a map defined on the whole of $X$, then this construction would show the result (at least the existence part). For example, I claim that this method shows:
Proposition: Let $e:X \to N$. Assume there are two maps $u_0:X \to X_0$ and $u_{>0} :X \to X_{>0}$. Then $X = X_0 \coprod X_{>0}$
For example, if both $X_0$ and $X_{>0}$ have global sections (map from $1$) then the proposition can be applied with $u_0$ and $u_{>0}$ two constant maps.
The general idea of the proof is that using the discussion above you can modify $u_0$ and $u_{>0}$ into maps $\tilde{u_0}$ and $\tilde{u_{>0}}$ so that they restrict to the identity on $X_0$ and this provide you with a canonical way of extending functions on $X_0$ and $X_{>0}$ to the whole of $X$ to apply the discussion above. This only proves the existence part of the coproduct property, not the uniqueness - but there is a neat trick to deduce uniqueness:
Lemma : Let $i:A \to C$ and $j:B \to C$ and assume that the induced natural transformation $Hom(C,Y) \to Hom(A,Y) \times Hom(B,Y)$ admit a section, which is natural in $Y$ and sends the pair $(i,j)$ to the identity of $C$. Then $C$ is the coproduct of $A$ and $B$ (with the maps $i$ and $j$).
Indeed, under the assumption of the lemma, the functor $Hom(A,Y) \times Hom(B,Y)$ is a retract of $C$, by a certain map $P: Hom(C,Y) \to Hom(C,Y)$, which by the Yoneda lemma corresponds to a map $P:C \to C$, but the second assumption give you that $P$ is the identity.
To deduce the proposition, just observe that the way we build a map $X \to Y$ out of two maps $X_0 \to X $ and $X_{>0} \to X$ is natural in $Y$, and gives the identity of $X$ if one start form the two inclusion map (for this we need to use the precise way the function $\tilde{u_0}$ and $\tilde{u_{>0}}$ were defined using the NNO).
Now, a counterexample.
So the general idea is we want to start from a situation where one of the two fiber has no map from 1 - that's not quite sufficient but this is necessary. I'm starting from the following assumption. Let $C$ be a category such that:

*

*$C$ has all finite limits and is extensive (all coproducts are universal and disjoint). I don't really need extensivity, I think I only need a (maybe strict) initial object - but most categories with NNO are extensive anyway.


*$C$ has a parametrized NNO.


*There exists a function $f: N \to N$ such that $f$ is not the constant equal to zero function but for all map $p: 1 \to N$ the composite $fp$ is equal to $0$.
I would recommend just assuming these exist. But a typical example of this situation (and to be honest the only ones I know) is to take $C$ to be the free topos (with NNO) or the free (extensive) cartesian closed category with NNO, or the free extensive category with NNO. In each case you can take $f$ to be a primitive recursive function which sends an integer $n$ to $1$ if $n$ is a code of a proof in the theory of elementary topos with NNO there exists a map $  * \to \emptyset$ - of course replacing elementary topos with NNO, by extensive (cartesian closed) with NNO in the other two cases.
In these categories, the only maps $1 \to N$ are the standard integer, so as such a proof of course does not exist, all global section are sent to $0$. But the point is that because of Gödel's theorem (applied to the recursively enumerable theory of say elementary topos with NNO), that function $f$ isn't the function equal to $0$.
Ok, so of course $C$ is extensive, so it isn't our counterexample on the nose.
Take $P$ to be the full subcategory of $C$ of objects $X$ that are either the initial object or admit at least one function $1 \to X$.
I claim that $P$ is a coreflective subcategory of $C$. Indeed, for any object $Y$ of $C$, then either it has no map $1 \to Y$ - in which case there is only one map $X \to Y$ with $X \in P$ given by the unique map from the initial object - Or there are some maps $1 \to Y$ in which case $Y \in P$. So in both case, there is a universal map $X \to Y$ with $X \in P$.
In particular, the category $P$ has all finite limits (by computing them in $C$ and applying the reflection). It is closed under product and coproduct in $C$ and contains the NNO of $C$, so it has a parametrized NNO.
Now consider our function $f:N \to N$, we assumed above. The fiber of $f$ over $N_{>0}$ has no map from $1$, so in $P$ it becomes the initial object. The fiber of $f$ over $0$ cannot be isomorphic (by the canonical mao) to $N$ because otherwise, we would have $f=0$. So the coproduct of the two is simply the fiver over $0$ - which is not isomorphic to $N$ (well - in fact, it will likelt be isomorphic to $N$ - but I mean not isomorphic by the canonical map).
