If is a 2-category with finite limits, a successor algebra in is an object equipped with morphisms and . A morphism of successor algebras is a morphism with isomorphisms and . Likewise a 2-cell of successor algebras is a 2-cell commuting with the above isomorphisms in an obvious way.
Finally, a natural numbers object in is an initial object in the 2-category of successor algebras. This means that for any successor algebra there is a morphism of successor algebras, unique up to unique isomorphism. Clearly any NNO in is also an NNO, in the usual sense, in .
If 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:
This enables us to show the following, using the internal logic.
First note that since and coproducts are disjoint, we have
Now consider the subobject described in the internal logic as determined by those for which the above sequents remain true when is replaced by . (This requires universal quantification over .) The above observation shows that . Suppose that , , and , . If then and is an isomorphism; otherwise ; but is ff, so we have and which are equal and isomorphisms; hence so are and . Thus, is closed under , so it is all of . Therefore, is discrete.