NNO in a 2-category

If $K$ is a 2-category with finite limits, a *successor algebra* in $K$ is an object $X$ equipped with morphisms $o:1\to X$ and $s:X\to X$. A morphism of successor algebras is a morphism $f:X\to Y$ with isomorphisms $f{o}_{X}\cong {o}_{Y}$ and $f{s}_{X}\cong {s}_{Y}f$. Likewise a 2-cell of successor algebras is a 2-cell $\alpha :f\to g$ commuting with the above isomorphisms in an obvious way.

Finally, a **natural numbers object** in $K$ is an initial object $N$ in the 2-category $\mathrm{SuccAlg}(K)$ of successor algebras. This means that for any successor algebra $X$ there is a morphism $N\to X$ of successor algebras, unique up to unique isomorphism. Clearly any NNO in $K$ is also an NNO, in the usual sense, in $\mathrm{disc}(K)$.

If $K$ doesn’t have enough exponentials, then perhaps this definition should be augmented with some parametricity, as in the 1-categorical case.

As in a 1-category, we can prove that:

- If $K$ has coproducts, then $[o,s]:1+N\to N$ is an equivalence, since $N$ is an initial algebra for the endofunctor $1+(-)$.
- Therefore, if $K$ is extensive, then $o:1\to N$ and $s:N\to N$ are disjoint subobjects of $N$.
- $N$ satisfies the fifth Peano axiom: if $N\prime $ is a subobject of $N$ containing $o$ and closed under $s$, then $N\prime =N$.

This enables us to show the following, using the internal logic.

If $K$ is a positive Heyting coherent 2-category with an NNO $N$, then $N$ is discrete.

First note that since $N\simeq 1+N$ and coproducts are disjoint, we have

$$\begin{array}{rl}x:N,f:{\mathrm{hom}}_{N}(o,x),g:{\mathrm{hom}}_{N}(x,o)& \u22a2f=g\phantom{\rule{thickmathspace}{0ex}}\text{and is an isomorphism}\\ x:N,f:{\mathrm{hom}}_{N}(x,o),g:{\mathrm{hom}}_{N}(o,x)& \u22a2f=g\phantom{\rule{thickmathspace}{0ex}}\text{and is an isomorphism}\end{array}$$

Now consider the subobject $S\hookrightarrow N$ described in the internal logic as determined by those $y:N$ for which the above sequents remain true when $o$ is replaced by $y$. (This requires universal quantification over $x,f,g$.) The above observation shows that $o\in S$. Suppose that $y\in S$, $x:N$, and $f:{\mathrm{hom}}_{N}(sy,x)$, $g:{\mathrm{hom}}_{N}(sy,x)$. If $x=o$ then $f=g$ and is an isomorphism; otherwise $x=sz$; but $s$ is ff, so we have $f\prime :{\mathrm{hom}}_{N}(y,z)$ and $g\prime :{\mathrm{hom}}_{N}(y,z)$ which are equal and isomorphisms; hence so are $f=s(f\prime )$ and $g=s(g\prime )$. Thus, $S$ is closed under $s$, so it is all of $N$. Therefore, $N$ is discrete.

Revised on February 13, 2009 05:28:19
by Mike Shulman
(75.3.140.11)