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 $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 $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'$ is a subobject of $N$ containing $o$ and closed under $s$, then $N'=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{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\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:hom_N(s y, x)$, $g:hom_N(s y,x)$. If $x=o$ then $f=g$ and is an isomorphism; otherwise $x = s z$; but $s$ is ff, so we have $f':hom_N(y,z)$ and $g':hom_N(y,z)$ which are equal and isomorphisms; hence so are $f= s(f')$ and $g=s(g')$. Thus, $S$ is closed under $s$, so it is all of $N$. Therefore, $N$ is discrete.