Natural numbers objects in topoi: Recursion in a parameter

Solution 1:

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.

Solution 2:

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\}$.