# Michael Shulman 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}\left(K\right)$ 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}\left(K\right)$.

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 $\left[o,s\right]:1+N\to N$ is an equivalence, since $N$ is an initial algebra for the endofunctor $1+\left(-\right)$.
• 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.

###### Theorem

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

###### Proof

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

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

Now consider the subobject $S↪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}\left(sy,x\right)$, $g:{\mathrm{hom}}_{N}\left(sy,x\right)$. 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}\left(y,z\right)$ and $g\prime :{\mathrm{hom}}_{N}\left(y,z\right)$ which are equal and isomorphisms; hence so are $f=s\left(f\prime \right)$ and $g=s\left(g\prime \right)$. 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)