Creo que la respuesta es no, porque ser un objeto numérico natural es una propiedad universal y ser un modelo de la aritmética de Nelson no lo es.
Mientras una categoría sea de Heyting (es una categoría regular en la que los mapas de imagen inversa entre los entramados de subobjetos tienen adyacentes correctos) es posible hablar de modelos de cualquier teoría de primer orden dentro de la categoría. Sin embargo, hay un problema: a menudo los modelos de una teoría de primer orden no son únicos hasta el isomorfismo (único) en las categorías de Heyting. Así que ser el modelo de una teoría de primer orden en una categoría de Heyting no suele ser una propiedad universal.
Un objeto numérico natural es no esencialmente un modelo de la aritmética de Peano, ya que la aritmética de Peano tiene muchos modelos no estándar. Yo diría que es esencialmente un modelo de la aritmética de segundo orden, aunque esto no tiene sentido directamente en otras categorías que no sean topos.
La aritmética de Nelson es más débil que la aritmética de Peano, y por tanto tiene los mismos modelos no estándar, si no muchos más. Se podría decir que normalmente hay muchos objetos de números naturales de Nelson no isomórficos. Pero no creo que esto sea lo que quieres decir.
Después del comentario de François, puede que tenga una mejor idea de lo que está buscando. Supongo que quieres algo como un objeto de número natural, que pasa a forzar la aritmética de Nelson en el lenguaje interno.
La definición de objeto de número natural tiene sentido en categorías monoidales arbitrarias, si se formula correctamente. Sin embargo, en estos contextos seguimos teniendo todas las funciones recursivas primitivas, que no tienen las restricciones de complejidad que menciona el artículo de la encuesta sobre la aritmética de Nelson. Así que eliminar la estructura de la categoría ambiental es insuficiente.
Lógica lineal son capaces de controlar la complejidad, y yo buscaría una respuesta allí. La idea es que la categoría ambiental tiene un endofunctor $!$ y que la recursión no da morfismos del objeto número natural $N$ pero de $!N$ en su lugar. Ahora puede controlar la deuda de la recursión en las funciones $N\to N$ controlando qué morfismos $!N\to N$ mediante un morfismo canónico $!N\to N$ . He tratado de encontrar una propiedad universal relacionada hace un par de meses, pero no he tenido éxito.
