Natural numbers objects in topoi: Recursion in a parameter I am currently trying to prove an exercise from Sheaves in Geometry and Logic: A First Introduction to Topos Theory by Mac Lane and Moerdijk about natural numbers objects.
First, we have the following definition:

Definition. A natural numbers object in a topos $\mathcal E$ is an object $N$ with arrows
  $$
1\overset 0 \longrightarrow N \overset s \longrightarrow N
$$
  such that for any object $X$ of $\mathcal E$ with arrows $x$ and $f$, as below, there is a unique arrow $h$ which makes the following diagram commute:
  $$
\begin{array}{cclcl}
1 & \overset 0 \longrightarrow & N & \overset s \longrightarrow & N \\
|| & & \downarrow h & & \downarrow h \\
1 & \underset x \longrightarrow & X & \underset f \longrightarrow & X.
\end{array}
$$

Next, the exercise in question is as follows:

Exercise. Let $N$, with arrows $0:1\to N$ and $s:N\to N$, be a natural numbers object in a topos $\mathcal E$.
  Prove that the following form of recursion "in a parameter":
  for objects $X$ and $Y$ of $\mathcal E$ and maps $g:X\to Y$ and $h:Y\times X\to Y$, there is a unique $f:N\times X\to Y$ such that the following diagrams commute:
  $$
\begin{array}{ccccclcc}
\phantom{\cong}1\times X & \overset{0\times\mathrm{id}}\longrightarrow & N\times X\phantom{f}
& &
\phantom{(f,\pi_2)}N\times X & \overset{s\times\mathrm{id}}\longrightarrow & N\times X
\\
\cong\downarrow & & \downarrow f && (f,\pi_2)\downarrow && \downarrow f
\\
\phantom{\cong}X & \underset g \longrightarrow & Y \phantom{f!}
&& \phantom{(f,\pi_2)}Y\times X & \underset h \longrightarrow & Y. \phantom{f}
\end{array}
$$
  [In $\mathbf{Sets}$, this would mean that $f$ is the function defined by $f(0,x)=g(x)$, $f(n+1,x)=h(f(n,x),x)$.]

Now, the proof is very straightforward in $\mathbf{Sets}$, but I can't figure it out for a general topos. It seems like there should be some sort of exponential/adjunction argument, but I'm not getting it. I hope I'm not missing anything obvious!
I'm looking forward to peoples' responses. Thanks in advance!

Edit (2013-03-24): For completeness, I decided to include my proof of the exercise that works in $\mathbf{Sets}$.
Proof.
Let $N$ be a natural numbers object in $\mathbf{Sets}$ (with the necessary functions $0:1\to N$ and $s:N\to N$), let $X$ and $Y$ be sets, and let
$$
g: X \to Y
\qquad\text{and}\qquad
h : Y \times X \to Y
$$
be functions.
We wish to show that there exists a unique function $f:N\times X\to Y$ such that
$$
f(0,x) = g(x)
\qquad\text{and}\qquad
f(n+1,x) = h(f(n,x),x)
$$
for all $n\in N$ and $x\in X$.
Given $x\in X$, define $h_x:Y\to Y$ by $h_x(y)=h(y,x)$ (this implicitly uses the
$$
\mathrm{Hom}_{\mathbf{Sets}}(Y\times X,Y)
\cong
\mathrm{Hom}_{\mathbf{Sets}}(X, Y^Y)
$$
adjunction). 
Then for each $x\in X$ we have a diagram
$$
1 \overset{g(x)} \longrightarrow Y \overset{h_x} \longrightarrow Y
$$
which induces a unique arrow $f_x:N\to Y$ such that the following diagram commutes:
$$
\begin{array}{cclcl}
1 & \overset 0 \longrightarrow & N & \overset s \longrightarrow & N \\
|| & & \downarrow f_x & & \downarrow f_x \\
1 & \underset{g(x)} \longrightarrow & Y & \underset {h_x} \longrightarrow & Y.
\end{array}
$$
Then we define $f:N\times X\to Y$ by $f(n,x)=f_x(n)$, and it is easy to see that this $f$ satisfies the desired properties and is unique.
This is the proof that I am struggling to generalize.
Maybe this is the wrong approach altogether for a general proof, although I feel like it should generalize.
Any help would be greatly appreciated.
 A: Here is an elementary proof of the existence part.
Let $\varepsilon$ denote the evaluation morphism and $\Lambda(x)$ the exponential transpose of $x$.
Given your $g$ and $h$ let $i$ be the canonical isomorphism from $1\times X \to X$ and define two morphisms $u = \Lambda(i ; g) : 1 \to Y^X$ and $v = \Lambda\left(\langle\varepsilon, \pi_2\rangle ; h\right) : Y^X \to Y^X$. Then there exists a unique $\hat{f} : N \to Y^X$ such that $0 ; \hat{f} = u$ and $s ; \hat{f} = \hat{f} ; v$. Define $f = \hat{f} \times id ; \varepsilon : N\times X \to Y$. Computing a bit we get
\begin{align*}
s\times id ; f &= (s ; \hat{f}) \times id ; \varepsilon = (\hat{f} ; v) \times id ; \varepsilon\\
&= (\hat{f}\times id) ; \left(\Lambda\left(\langle\varepsilon, \pi_2\rangle ; h\right)\times id\right) ; \varepsilon\\
&=(\hat{f}\times id) ; \langle \varepsilon, \pi_2\rangle ; h\\
&= \langle f, \pi_2\rangle ; h
\end{align*}
and 
\begin{align*}
0\times id ; f = (0 ; \hat{f}) \times id ; \varepsilon = \Lambda(i ; g) \times id ; \varepsilon = i ; g
\end{align*}
This shows the existence of $f$. Uniqueness is straightforward as any such $f$ induces an $\hat{f}$ satisfying the required two equations by setting $\hat{f} = \Lambda(f)$. This assignment is easily seen, using the universal property of exponentials, to be a bijection.
Notice that you don't really need a topos, you only need a cartesian closed category to carry out the argument.
In Set, this reduces to defining $u$ and $v$ point-wise as
\begin{align*}
  u(\star)(x) &= g(x)\\
  v(\phi)(x) &= h(\phi(x), x)
\end{align*}
where $1 = \{\star\}$.
A: Your struggles, I think, are that the definition of a NNO is given externally; but a direct translation of your proof requires an internal version in the form of a map $r:Y \times Y^Y \to Y^N$ that takes a "generalized element" of $Y$ and a "generalized map" from $Y$ to $Y$ and produces a "generalized map" $N \to Y$.
Set theoretically, this map would be given by
$$ r(y,h)(n) = k^{(n)}(y) $$
where $k^{(n)}$ is the $n$-fold iterate of $k$.
If we have this map $r$, then your argument is constructing the map $X \to Y \times Y^Y \to Y^N$, which you transpose to get $f$. (phrase things in terms of generalized elements if you like)
In the interest of preserving the specific argument you wish to make, let's see if we can construct $r$.
There are lots of ways we can rewrite things with natural isomorphisms. This one seems most promising to me:
$$ \hom(Y \times Y^Y, Y^N)
\cong \hom(N \times Y \times Y^Y, Y)
\cong \hom(N, Y^{Y \times Y^Y}) $$
Set theoretically, $r$ would correspond to the map
$$ n \mapsto \left( (y,k) \mapsto k^{(n)}(y) \right) $$
This one is promising, because it looks like I can define this one by recursion! If I attach $k$ to the output so that I can "remember" it, I can recursively define a function $s_n$ by:


*

*$s_0(y,k) = (y,k)$

*$s_{n+1}(y,k) = (k(y), k)$


So we set up the corresponding diagram
$$1 \to (Y \times Y^Y)^{Y \times Y^Y} \to (Y \times Y^Y)^{Y \times Y^Y}$$
Obtain
$$N \to (Y \times Y^Y)^{Y \times Y^Y} $$
Then convert to
$$ N \times Y \times Y^Y \to Y \times Y^Y \to Y $$
(the last map is projection, not evaluation).
If there's any justice in the world, the transpose of this is $r : Y \times Y^Y \to Y^N$. I'm too exhausted (and rusty) by this point to verify it all works out.

With that said, attacking the problem from scratch I probably would have curried differently: try to define a function $N \to Y^X$. Although it's plausible I would have wound up making a similar argument as to the one above.
