1 Introduction

The natural numbers object (NNO) is among the most basic universal constructions of categorical logic. Lawvere’s 1964 axiomatisation of the elementary theory of the category of sets (ETCS) treats the NNO as an irreducible primitive on equal footing with the terminal object, the subobject classifier, and exponentials. In any cartesian closed category $C$ with a terminal object $1$ , an NNO is a triple $(N, 0 : 1 \to N, s : N \to N)$ such that for every $(X, x_{0} : 1 \to X, f : X \to X)$ there exists a unique morphism $h : N \to X$ with $h \circ 0 = x_{0}$ and $h \circ s = f \circ h$ . Two NNOs are related by a unique isomorphism; the automorphism group of an NNO is trivial. In $Set$ the NNO is the von Neumann set $ω = {0, 1, 2, \dots}$ with successor; up to canonical isomorphism, “the natural numbers” is a property, not a choice of structure.

The HoTT version is finer. Working in the univalent universe $U$ , define $NNO : = Σ_{X : U} Σ_{x_{0} : X} Σ_{s : X \to X} isInitial (X, x_{0}, s),$ where $isInitial (X, x_{0}, s)$ denotes the proposition that $(X, x_{0}, s)$ is initial in the type-theoretic category of pointed dynamical systems. Theorem 2.7 of Paper III¹ (which we recapitulate in §2 as 7) and Theorem 4.4 of Paper V state that $NNO$ is contractible—a $(- 2)$ -type. The centre of contraction is $(N, zero, succ, ⋆)$ where $N$ is the inductive type of natural numbers and $⋆$ is the canonical proof of initiality. Crucially, contractibility is strictly stronger than “unique up to unique iso”: it asserts that every two NNOs are connected by a path (an equivalence, by univalence), and that every two such paths are themselves connected by a $2$ -path, ad infinitum.

By Shulman’s theorem , every Grothendieck $(\infty, 1)$ -topos $E$ models HoTT with univalence, and conjecturally so does every elementary $(\infty, 1)$ -topos. Therefore the contractibility theorem transports internally: for each such $E$ there is an internal type of NNO structures in $E$ , and this type is contractible. Externalising the internal contractibility yields a strong $\infty$ -categorical statement: the space $NNO (E)$ of NNO structures, formed in the $\infty$ -category $E$ , is a contractible Kan complex.

The aim of this paper is to make this transfer rigorous, and to compare it with the two existing definitions of $(\infty, 1)$ -NNO available in the literature: Lurie’s parametrised NNO , formulated for presentable $(\infty, 1)$ -toposes via a small-colimit-preserving recursion principle, and Rasekh’s NNO , which lives in any elementary $(\infty, 1)$ -topos and is constructed from the loop space of $S^{1}$ . The first is convenient when one has Giraud-style axioms; the second is intrinsic to the elementary axiomatic and was the missing piece to certify that elementary $(\infty, 1)$ -toposes are indeed natural homes for arithmetic.

Contributions

We give a self-contained statement of contractibility of the type of NNOs in HoTT (§2, 7), recall Lambek’s theorem at the $1$ -categorical level, and explain how rigidity at this level becomes contractibility once one moves from sets-of-iso-classes to $\infty$ -groupoids.
We give a precise account of Lurie’s parametrised NNO (§3, 12, 20) and prove its equivalence with the $1$ -categorical NNO when $E$ is the underlying $(2, 1)$ -category of a $1$ -topos.
We formalise the higher coherence problem (§4, 21) as the requirement that, for each $n \geq 0$ , the comparison maps between two NNOs are coherent up to $n$ -homotopy.
We prove our main theorem (§5, 23): in any $(\infty, 1)$ -topos $E$ that admits a HoTT model, the space $NNO (E)$ is contractible.
We compare with Rasekh’s circle-construction (§6) and exhibit the natural map identifying the two NNOs.
We discuss synthetic approaches via Riehl–Shulman simplicial type theory (§7) and list open problems (§10).

Outline

2 reviews the $1$ -categorical NNO, Lambek’s theorem, and the contractibility result of Paper III/V. 3 introduces Lurie’s parametrised NNO and Rasekh’s elementary $(\infty, 1)$ -NNO. 4 formalises the higher-coherence tower. 5 contains the main contractibility theorem. 6 relates the construction to the loop-space-of- $S^{1}$ approach. 7 discusses synthetic approaches. 10 closes with open problems.

Conventions

We use $Cat_{\infty}$ for the $(\infty, 2)$ -category of $(\infty, 1)$ -categories and $S$ for the $(\infty, 1)$ -category of $\infty$ -groupoids (“spaces”). For an $(\infty, 1)$ -category $C$ , $Map_{C} (X, Y) \in S$ denotes the mapping space. We write $1$ for a terminal object. Throughout, “HoTT” refers to Martin-Löf type theory with $Σ$ , $Π$ , identity types, finite coproducts, the natural numbers type, function extensionality, and the univalence axiom for at least one hierarchy of universes.

2 Background: 1-categorical NNO and contractibility

We begin by recalling the classical material in a form that will generalise cleanly to the $\infty$ -categorical setting.

2.1 Pointed endomorphisms and $1$ -NNO

Definition 1 (Pointed dynamical system). Let $C$ be a category with terminal object $1$ . The category $PtEndo (C)$ has as objects triples $(X, x_{0} : 1 \to X, f : X \to X)$ , and morphisms $(X, x_{0}, f) \to (Y, y_{0}, g)$ are arrows $h : X \to Y$ in $C$ such that $h \circ x_{0} = y_{0}$ and $h \circ f = g \circ h$ .

Definition 2 (NNO). A natural numbers object in $C$ is an initial object of $PtEndo (C)$ .

Equivalently, viewing the endofunctor $F : C \to C$ given by $F X = 1 + X$ (when coproducts exist), an NNO is an initial $F$ -algebra: a pair $(N, [0, s] : 1 + N \to N)$ initial in $F - Alg$ .

Lemma 3 (Rigidity of initial objects). If $I, I^{'}$ are initial in any category, there is a unique isomorphism $I \to I^{'}$ , and the automorphism group $Aut (I)$ is trivial.

Proof. Initiality of $I$ gives a unique map $u : I \to I^{'}$ , and dually a unique $v : I^{'} \to I$ . The composites $v \circ u$ and $id_{I}$ are both morphisms $I \to I$ ; since $I$ is initial, the hom-set $Hom (I, I)$ has exactly one element, hence $v \circ u = id_{I}$ . Similarly $u \circ v = id_{I^{'}}$ . Applying the same argument with $I = I^{'}$ , every endomorphism of $I$ equals $id_{I}$ , so $Aut (I) = {id_{I}}$ . ◻

Lemma 4 (Lambek). If $(I, ι : F I \to I)$ is an initial $F$ -algebra, then $ι$ is an isomorphism.

Proof. The map $F ι : F (F I) \to F I$ endows $F I$ with the structure of an $F$ -algebra, denoted $(F I, F ι)$ . By initiality of $(I, ι)$ there is a unique $F$ -algebra homomorphism $h : (I, ι) \to (F I, F ι)$ , that is, a morphism $h : I \to F I$ in $C$ with $h \circ ι = F ι \circ F h .$ On the other hand, $ι$ itself is an $F$ -algebra homomorphism $(F I, F ι) \to (I, ι)$ , since $ι \circ F ι = ι \circ F ι$ trivially. Thus $ι \circ h : (I, ι) \to (I, ι)$ is an $F$ -algebra endomorphism, and by initiality (applied to $(I, ι)$ as the source of a unique map to itself) it equals $id_{I}$ . We conclude $ι \circ h = id_{I}$ . For the other composite, observe $h \circ ι = F ι \circ F h = F (ι \circ h) = F (id_{I}) = id_{F I},$ using functoriality of $F$ . Thus $h$ is two-sided inverse to $ι$ , and $ι$ is an isomorphism. ◻

Remark 5. The Lambek square depicting the proof is $\begin{tikzcd}[column sep=large, row sep=large] FI \arrow[r, "Fh"] \arrow[d, "\iota"'] & F(FI) \arrow[d, "F\iota"] \\ I \arrow[r, "h"'] & FI \end{tikzcd}$ which commutes by definition of $h$ as an $F$ -algebra homomorphism.

Theorem 6 (Universal property of NNO). Let $(N, 0, s)$ be an NNO in $C$ . For every $(X, x_{0}, f)$ in $PtEndo (C)$ there exists a unique $h : N \to X$ in $C$ with $h \circ 0 = x_{0}$ and $h \circ s = f \circ h$ .

2.2 1-Categorical contractibility (rigidity of NNOs)

We use the standard truncation conventions: a $(- 2)$ -type is contractible, a $(- 1)$ -type is a (mere) proposition (a groupoid in which any two objects are connected by at most one morphism), and a $0$ -type is a set. A nonempty groupoid in which every hom-set is a singleton is contractible—a $(- 2)$ -type.

In $Set$ , the NNO is $(N, 0, succ)$ . By 3 the groupoid of NNOs in $Set$ has trivial automorphisms and a unique morphism between any two objects: it is a contractible groupoid, equivalently a $(- 2)$ -truncated space.

Theorem 7 (1-categorical contractibility of $NNO$ ). In any category $C$ with terminal object, the groupoid $NNO (C)$ of NNO structures is either empty or contractible (i.e. a $(- 2)$ -type). Equivalently, the moduli space of NNOs in $C$ is a (mere) proposition: existence implies essential uniqueness, with no nontrivial automorphisms or higher cells (which are absent at the $1$ -categorical level).

Proof. 3 provides a unique isomorphism between any two NNOs and triviality of automorphisms. Hence the groupoid has a unique morphism between any pair of objects. When nonempty, such a groupoid is equivalent to the terminal groupoid $1$ , hence contractible. ◻

2.3 HoTT contractibility

In HoTT we go further. Let $U$ be a univalent universe. The result we recall here is stated as Theorem 2.7 in our companion paper and as Theorem 4.4 in ; it is also implicit in the discussion of the natural numbers type in . Because those references rely on internal context (notation, intermediate lemmas), we restate the theorem and give a self-contained proof.

Definition 8 (Type of NNOs in HoTT). $NNO : = Σ_{X : U} Σ_{x_{0} : X} Σ_{s : X \to X} isInitial (X, x_{0}, s),$ where $isInitial (X, x_{0}, s) : = Π_{(Y, y_{0}, f) : PtEndo (U)} isContr (Σ_{h : X \to Y} (h x_{0} = y_{0}) \times Π_{x : X} (h (s x) = f (h x))) .$

Note that $isInitial (X, x_{0}, s)$ is, by construction, an iterated $Π$ -type whose body is $isContr$ of a $Σ$ -type; since $isContr$ is a (mere) proposition and $Π$ of propositions is a proposition, $isInitial$ is a proposition.

Theorem 9 (Contractibility of $NNO$ in HoTT ). The type $NNO$ is contractible. The centre of contraction is $(N, zero, succ, ⋆)$ where $N$ is the inductive type of natural numbers and $⋆$ is the canonical witness of initiality given by the standard recursor $rec_{N}$ together with its computation rules.

Proof. We must show $isContr (NNO)$ , i.e. produce a centre $c \in NNO$ and a continuous family of paths from $c$ to every point of $NNO$ .

Centre. Take $c = (N, zero, succ, ⋆)$ . The proof $⋆ : isInitial (N, zero, succ)$ is constructed as follows. Given $(Y, y_{0}, f)$ , define $h : = rec_{N} y_{0} f : N \to Y$ . By the computation rules of the recursor we have judgmentally $h (zero) \equiv y_{0}$ and $h (succ n) \equiv f (h n)$ , so the equations are witnessed by $refl$ . Uniqueness: if $h^{'} : N \to Y$ also satisfies $h^{'} zero = y_{0}$ and $Π_{n : N} h^{'} (succ n) = f (h^{'} n)$ , dependent induction $ind_{N}$ on the type-family $P (n) : = (h n = h^{'} n)$ produces a homotopy $h \sim h^{'}$ . By function extensionality (provable from univalence ), $h = h^{'}$ . Combining existence and uniqueness, the type $Σ_{h : N \to Y} (h zero = y_{0}) \times Π_{n : N} (h (succ n) = f (h n))$ is contractible: $h = rec_{N} y_{0} f$ together with the $refl$ -witnesses of the equations is the centre, and the contraction is provided by the $ind_{N}$ step above.

Contraction onto the centre. Take any $(X, x_{0}, s, ι) \in NNO$ . We must produce a path $p : (N, zero, succ, ⋆) = (X, x_{0}, s, ι) in NNO .$ Apply $ι$ to the pointed system $(N, zero, succ)$ : it yields a contractible type whose centre is a unique map $u : X \to N$ with $u x_{0} = zero$ and $u \circ s \sim succ \circ u$ . Apply $⋆$ to $(X, x_{0}, s)$ : a unique map $v : N \to X$ with $v zero = x_{0}$ and $v \circ succ \sim s \circ v$ . The composites $u \circ v : N \to N$ and $id_{N}$ both satisfy the universal-property equations for $(N, zero, succ, ⋆)$ ; uniqueness inside the contractible type of recursors forces $u \circ v = id_{N}$ via $ind_{N}$ , and likewise $v \circ u = id_{X}$ via $ι$ . Thus $u : X ≃ N$ is an equivalence (with quasi-inverse $v$ ). Univalence ( $ua$ ) converts the equivalence into a path $p_{1} : X = N$ in $U$ . Transporting $(x_{0}, s, ι)$ along $p_{1}$ produces $(zero, succ, ⋆^{'})$ for some witness $⋆^{'} : isInitial (N, zero, succ)$ . Since $isInitial$ is a proposition, $⋆^{'} = ⋆$ . Pairing yields the required path $p$ in $NNO$ .

The map $(X, x_{0}, s, ι) \mapsto p$ is itself constructed by transport and is thus a continuous family of paths from $c$ , exhibiting $c$ as the centre of contraction. ◻

Remark 10 (The infinite tower). The proof of 9 bundles infinitely many coherences into the propositional fact $isContr (NNO)$ . Path induction (the $J$ -rule) allows us to manipulate paths, $2$ -paths, $3$ -paths, and so on, with no extra effort: once we have $isContr (NNO)$ , we automatically get $isContr (Ω^{n} NNO)$ for every $n$ , by general HoTT lemmas.

Remark 11 (Why this is stronger). 7 says “unique iso between any two NNOs”. 9 says, in addition, that the space of paths between any two equivalences is contractible, the space of $2$ -paths is contractible, and so on. In a $1$ -category these higher cells are trivially identities; in an $\infty$ -category they need to be checked. HoTT performs all of this with one-and-the-same proof, because $isContr$ is a mere proposition that already absorbs the entire tower.

3 The $(\infty, 1)$ -categorical NNO

We now lift 2 to $(\infty, 1)$ -categories. There are two natural lifts: a parametrised one due to Lurie, and an absolute one suitable for elementary $(\infty, 1)$ -toposes.

3.1 Lurie’s parametrised NNO

Definition 12 ( $(\infty, 1)$ -NNO, Lurie). Let $E$ be a presentable $(\infty, 1)$ -topos with terminal object $1$ . An NNO is an object $N \in E$ together with morphisms $0 : 1 \to N$ and $s : N \to N$ such that for every diagram $1 x_{0} X f X$ in $E$ , the mapping space $Map_{PtEndo (E)} ((N, 0, s), (X, x_{0}, f))$ is contractible.

Here $PtEndo (E)$ is the $(\infty, 1)$ -category of pointed endomorphisms in $E$ . Concretely, an object of $PtEndo (E)$ is a triple $(X, x_{0} : 1 \to X, f : X \to X)$ where $X \in E$ , $x_{0}$ is a global element, and $f$ is an endomorphism. A morphism $(X, x_{0}, f) \to (Y, y_{0}, g)$ is a tuple $(h, α, β)$ where $h : X \to Y$ is a morphism in $E$ , $α : h \circ x_{0} \sim y_{0}$ is a $1$ -cell in $Map_{E} (1, Y)$ , and $β : h \circ f \sim g \circ h$ is a $1$ -cell in $Map_{E} (X, Y)$ , together with the higher cells provided by composing in $E$ . In symbols this is the $\infty$ -categorical limit (formally, an iterated comma object) $PtEndo (E) : = E_{1 /} \times_{E} E^{[1]}$ parametrising pairs $(x_{0} : 1 \to X, f : X \to X)$ .

Remark 13. Equivalently, an $(\infty, 1)$ -NNO is an initial object in $PtEndo (E)$ , where “initial” is interpreted in the $(\infty, 1)$ -categorical sense: the mapping space to every other object is contractible. Lurie phrases the definition via a small-colimit-preserving recursion functor; the equivalence is straightforward.

Example 14. When $E = S$ , the NNO is the constant functor at $N$ . Its existence and contractibility of the mapping space is the homotopy-coherent version of the Set-theoretic recursion principle.

Example 15. For $E = PSh (C)$ the $(\infty, 1)$ -category of presheaves of spaces on a small $(\infty, 1)$ -category $C$ , the NNO is the constant presheaf at $N$ , $c \mapsto N$ .

Example 16. For $E = Sh (X)$ the $(\infty, 1)$ -topos of sheaves on a topological space $X$ , the NNO is the constant sheaf $\underline{N}$ .

3.2 Existence in presentable $(\infty, 1)$ -toposes

Theorem 17 (Existence in presentable case). Every presentable $(\infty, 1)$ -topos has an NNO.

Sketch. Presentability ensures small colimits and a small generating set. Build $N$ as the sequential colimit $N = colim (1 j_{0} 1 ⊔ 1 j_{1} 1 ⊔ 1 ⊔ 1 j_{2} \dots),$ where $j_{n}$ adds a new copy of $1$ . Equivalently, $N = ⨆_{n \geq 0} 1$ . Verification of the universal property uses the universal property of sequential colimits and contractibility of the relevant mapping spaces. ◻

3.3 Elementary $(\infty, 1)$ -toposes and Rasekh’s NNO

A more delicate question is whether every elementary $(\infty, 1)$ -topos has an NNO; here we follow the axiomatic of Rasekh . Elementary $(\infty, 1)$ -toposes are axiomatised by:

finite limits,
locally cartesian closure,
subobject classifier,
object classifier (a univalent universe of small types),
finite colimits.

They need not be presentable.

Theorem 18 (Rasekh ). Every elementary $(\infty, 1)$ -topos has an NNO. In particular, the existence of the NNO does not need to be added as a separate axiom: it is derivable from the other axioms of an elementary $(\infty, 1)$ -topos.

Sketch of Rasekh’s argument. The circle $S^{1}$ exists in any elementary $(\infty, 1)$ -topos as a higher inductive type (or, more carefully, as the geometric realisation of the simplicial circle). Rasekh shows that the loop space $Ω S^{1}$ has a $Z$ -action and that its connected component of the basepoint (or, in pointed form, the universal cover) functions as an NNO. The argument uses descent, locality, and classification of univalent maps. ◻

Remark 19. Rasekh’s proof is striking because it derives a discrete, $0$ -truncated, NNO from a manifestly $1$ -truncated object, $S^{1}$ , via genuinely $\infty$ -categorical machinery. There is no $1$ -categorical analogue: $Ω S^{1}$ in the $1$ -topos of sets is a singleton.

3.4 Equivalence with the $1$ -NNO when $E$ is a $1$ -topos

Theorem 20 (Comparison). Let $E$ be a $1$ -topos with NNO $(N, 0, s)$ , and let $E^{(\infty)}$ be its embedding as a $(2, 1)$ -category, viewed as an $(\infty, 1)$ -category. Then $(N, 0, s)$ is an $(\infty, 1)$ -NNO of $E^{(\infty)}$ in the sense of 12.

Proof. The mapping spaces in $E^{(\infty)}$ are $0$ -truncated (sets). The mapping space $Map_{PtEndo (E^{(\infty)})} ((N, 0, s), (X, x_{0}, f))$ is therefore a set, and is the hom-set of 1. By the universal property in $E$ , this set has exactly one element, hence is contractible. ◻

4 Higher coherences

Why is the $(\infty, 1)$ -NNO “more delicate”? The naive answer is: in a $1$ -category, “unique map” is a single condition. In an $(\infty, 1)$ -category, “unique map” must be promoted to “unique up to coherent homotopy”. Concretely, given two NNOs $N_{1}, N_{2}$ in $E$ , we need a comparison map $u : N_{1} \to N_{2}$ together with the homotopies filling the squares $\begin{tikzcd}[column sep=large, row sep=large] \mathbf{1} \arrow[r, "0_{1}"] \arrow[dr, "0_{2}"'] & N_{1} \arrow[d, "u"] \arrow[r, "s_{1}"] \arrow[dr, phantom, "\Downarrow\,\beta", near start] & N_{1} \arrow[d, "u"] \\ & N_{2} \arrow[r, "s_{2}"'] & N_{2} \end{tikzcd}$ Filling the upper-left triangle is a $1$ -cell $α : u \circ 0_{1} \sim 0_{2}$ , and filling the right-hand square is a $1$ -cell $β : u \circ s_{1} \sim s_{2} \circ u$ . Beyond these, we need:

compatibilities of these homotopies (i.e. $2$ -cells filling in the obvious squares),
compatibilities of those compatibilities ( $3$ -cells),
and so on, ad infinitum.

Proposition 21 (Initiality absorbs the entire coherence tower). The initiality of an $(\infty, 1)$ -NNO already encodes, in a single property, the entire infinite tower of coherence data sketched above. Concretely, for any two $(\infty, 1)$ -NNOs $(N_{1}, 0_{1}, s_{1})$ and $(N_{2}, 0_{2}, s_{2})$ in an $(\infty, 1)$ -category $E$ , the mapping space $M : = Map_{PtEndo (E)} ((N_{1}, 0_{1}, s_{1}), (N_{2}, 0_{2}, s_{2}))$ is contractible.

Proof. By definition of $(\infty, 1)$ -NNO, both $(N_{1}, 0_{1}, s_{1})$ and $(N_{2}, 0_{2}, s_{2})$ are initial objects of $PtEndo (E)$ . Initial objects in any $(\infty, 1)$ -category have contractible mapping spaces to every object, in particular to each other. Contractibility of $M$ is equivalent to existence of a $0$ -cell (the comparison map $u$ and the homotopies $α, β$ ), uniqueness up to a contractible space of $1$ -cells (the next-level coherences), uniqueness of those up to a contractible space of $2$ -cells, and so on inductively at every level $n \geq 0$ . ◻

Remark 22. The content of 21 is that contractibility of $M$ is equivalent to:

$π_{0} M = *$ : existence and uniqueness up to homotopy of the comparison map;
$π_{n} M = 0$ for all $n \geq 1$ : triviality of all higher loop spaces, i.e. the entire tower of compatibilities.

4.1 Truncation level of $NNO (E)$

Define $NNO (E)$ as the full subspace of the $\infty$ -groupoid $PtEndo (E)^{≃}$ (the maximal sub- $\infty$ -groupoid of $PtEndo (E)$ ) on objects that are initial.

Theorem 23 (Contractibility of the $\infty$ -NNO space). For any $(\infty, 1)$ -topos $E$ in which an NNO exists, the space $NNO (E)$ is contractible.

Proof. The full sub- $\infty$ -groupoid of an $(\infty, 1)$ -category on the initial objects is either empty or contractible: this is the $\infty$ -categorical analogue of 3. Spelling this out: given any two initial objects $I_{1}, I_{2} \in PtEndo (E)$ , the mapping space $Map (I_{1}, I_{2})$ is contractible by 21; in particular it is inhabited, so the sub- $\infty$ -groupoid of initial objects is connected. The automorphism space $Map (I, I)$ of any initial object $I$ is also contractible (apply 21 with $I_{1} = I_{2} = I$ ), which forces all loop spaces $Ω^{n} Map (I, I)$ to be contractible, hence trivial. A connected $\infty$ -groupoid with trivial loop spaces is, by Whitehead’s theorem, contractible. ◻

5 The main theorem: contractibility for $(\infty, 1)$ -NNOs

5.1 Statement and proof

We now combine the HoTT contractibility result with Shulman’s interpretation theorem to give an internal-to-external argument for 23, and to compare it with Rasekh’s circle-construction.

Theorem 24 (Main theorem). Let $E$ be an $(\infty, 1)$ -topos that admits a model of HoTT + univalence (e.g. any Grothendieck $(\infty, 1)$ -topos, by ). Then:

There exists an $(\infty, 1)$ -NNO in $E$ (12).
The space $NNO (E)$ is contractible (a $(- 2)$ -type).
Any two $(\infty, 1)$ -NNOs in $E$ are connected by an essentially unique equivalence.
The automorphism $\infty$ -group of an $(\infty, 1)$ -NNO is contractible.

Proof. By Shulman’s theorem, $E$ admits a model of HoTT in which $U$ is interpreted as the object classifier and the type $NNO$ of 8 is interpreted as an internal object of $E$ (more precisely, as the underlying object of an $\infty$ -groupoid object of $E$ , classified by $U$ ). By 9, this internal type is contractible (i.e. the proposition $isContr (NNO)$ has a global element).

Externalisation. The functor $E \to S$ , $X \mapsto Map_{E} (1, X)$ , is the global-sections functor. It preserves limits and (since $1$ is the unit of the model) takes the internal type $NNO$ to the external $\infty$ -groupoid $NNO (E)$ . Internal contractibility of $NNO$ in the HoTT model is the global element of $isContr (NNO)$ , which under externalisation becomes a global point of $Map_{E} (1, isContr NNO) ≃ isContr (NNO (E))$ , witnessing that $NNO (E)$ is contractible in $S$ . (For a detailed account of the internal-to-external transfer of contractibility statements, see .)

Existence (1) follows from 17 when $E$ is presentable, or from 18 when $E$ is elementary. Statement (2) is the externalisation just described. Statements (3) and (4) follow from (2) by standard arguments: a contractible $\infty$ -groupoid has a unique-up-to-contractible-choice path between any two points, and trivial loop spaces at every point. ◻

5.2 What “contractible” contributes beyond “unique iso”

Remark 25 (Higher coherence cancellation). 24 packages infinitely many layers of coherence into one statement. To see the gain concretely, consider the recursion principle: given $(X, x_{0}, f)$ in $E$ , we get $h : N \to X$ in $E$ . In a $1$ -topos, this is a single morphism. In an $(\infty, 1)$ -topos, $h$ comes equipped with:

a $1$ -cell witnessing $h \circ 0 \sim x_{0}$ ,
a $1$ -cell witnessing $h \circ s \sim f \circ h$ ,
$2$ -cells expressing that the choice of $1$ -cells is unique up to homotopy,
$\dots$

24 guarantees that the data above is recoverable up to a contractible space of choices. In HoTT, the work is done by pattern-matching on identity types and using $isContr$ -elimination.

5.3 Identification with Rasekh’s NNO

Theorem 26 (Rasekh $=$ Lurie internally). Let $E$ be an elementary $(\infty, 1)$ -topos. The NNO constructed by Rasekh from the loop space of $S^{1}$ coincides, up to a contractible space of equivalences, with any presentation-based $(\infty, 1)$ -NNO in the sense of 12 (when both are defined).

Proof. By part (2) of 24, $NNO (E)$ is contractible whenever an NNO exists. Both Rasekh’s NNO (18) and any Lurie-style NNO (12) are points of $NNO (E)$ . Hence they are connected by a unique-up-to-contractible-choice equivalence. ◻

6 Rasekh’s circle-construction of the NNO

We now sharpen the discussion of Rasekh’s circle-construction.

6.1 The role of $S^{1}$

In an elementary $(\infty, 1)$ -topos $E$ , the circle $S^{1}$ is the higher inductive type generated by a point $base : 1 \to S^{1}$ and a loop $loop : base = base$ . (One must check that $E$ admits this HIT. Rasekh shows the relevant pushout exists using descent.) The loop space $Ω S^{1} : = base \times_{S^{1}} base$ is a group object in $E$ in the homotopical sense.

Theorem 27 (Rasekh, in HoTT form). $Ω S^{1} ≃ Z$ in any elementary $(\infty, 1)$ -topos $E$ , where $Z$ is the group object obtained from the type of integers in $E$ .

Idea. Use the encode–decode method (Licata–Shulman ) to construct a fibration $code : S^{1} \to U with code (base) ≃ Z,$ where the loop $loop$ acts as the successor equivalence $Z ≃ Z$ . The total space of $code$ is contractible, and the fibre over $base$ is $Z$ . ◻

Remark 28 (Recovery of $N$ from $Z$ ). Once $Z$ is constructed in $E$ (via 27), $N$ is obtained as the subobject of non-negative integers, which is isomorphic to the colimit construction in 17. The key point is that elementary $(\infty, 1)$ -toposes have enough structure—specifically, locally cartesian closure plus a univalent universe—to internalise this construction.

6.2 Why this fails in $1$ -topos theory

In a $1$ -topos $E_{1}$ , every type is $0$ -truncated, so $Ω S^{1} = S^{1} \times_{S^{1}} S^{1}$ is the singleton (a single point with no nontrivial loops, since paths don’t exist). The encode–decode argument collapses, and we cannot recover $Z$ or $N$ this way. The $\infty$ -categorical setting is therefore not just a technical generalisation: it makes essentially new constructions possible.

6.3 Higher inductive types in elementary $(\infty, 1)$ -toposes

The construction of $S^{1}$ as a HIT in an elementary $(\infty, 1)$ -topos is more delicate than the corresponding sheaf-theoretic construction. The required ingredient is the existence of geometric realisation of suitable diagrams; Rasekh’s approach is to encode $S^{1}$ as a particular pushout diagram and verify by descent that this pushout exists.

Remark 29 (Generalisation beyond $S^{1}$ ). The same strategy applies to higher spheres $S^{n}$ and Eilenberg–MacLane objects $K (G, n)$ . In particular, the loop space $Ω^{n} S^{n}$ in an elementary $(\infty, 1)$ -topos has a canonical $Z$ -action when $n \geq 1$ (by suspension), giving a more conceptual route to $Z$ and hence $N$ .

Proposition 30 (Universal cover viewpoint). In an elementary $(\infty, 1)$ -topos $E$ , the universal cover $S^{1} \to S^{1}$ has total space that, viewed as a discrete groupoid in $E$ , is the $Z$ -torsor $Z$ (with the $Z$ -action given by deck transformations). Restricting to non-negative components yields $N$ .

Sketch. The universal cover of $S^{1}$ in $Top$ is $R \to S^{1} = R / Z$ . In an elementary $(\infty, 1)$ -topos, this becomes a fibration whose fibre is $π_{1} (S^{1}) = Z$ . The discrete object underlying the fibre is the type of integers, which the elementary axiomatic supplies via the object classifier and locally cartesian closure. ◻

6.4 Power objects vs object classifier

A subtle point in the elementary axiomatic is whether one assumes power objects (like $1$ -toposes) or an object classifier (Lurie’s $(\infty, 1)$ -version). Power objects classify subobjects; the object classifier classifies all small maps.

Proposition 31 (Object classifier suffices). In an elementary $(\infty, 1)$ -topos with object classifier $U$ , the NNO can be constructed without separate appeal to power objects.

Proof. The construction in 27 uses only $U$ and pushouts; no separate power-object axiom is invoked. ◻

7 Synthetic approaches via simplicial type theory

Riehl–Shulman simplicial type theory (STT) extends HoTT with a directed interval $Δ^{1}$ and a directed path type $Hom_{A} (a, b)$ . The intent is to enable synthetic reasoning about $(\infty, 1)$ -categories rather than $\infty$ -groupoids.

7.1 Brief review of STT

Riehl–Shulman simplicial type theory adds to the type-theoretic context a directed interval $Δ^{1}$ (an extension type with two endpoints $0, 1$ and a unique non-identity directed path) and the corresponding hom-types $Hom_{A} (a, b) : = {f : Δ^{1} \to A f (0) \equiv a, f (1) \equiv b} .$ Unlike the symmetric path types of HoTT, hom-types are inherently directed: $Hom_{A} (a, b)$ and $Hom_{A} (b, a)$ are not interchangeable in general. To talk about $(\infty, 1)$ -categories synthetically, STT adds two predicates:

the Segal condition, asserting horn-filling for the inner $2$ -simplex $Λ_{1}^{2} ↪ Δ^{2}$ , which encodes composition;
the Rezk condition (also called “completeness”), asserting that all isomorphisms in the category are paths.

A type satisfying both is a synthetic $(\infty, 1)$ -category. The universe $U_{Rezk}$ of Rezk-complete types is itself a Rezk-complete type and forms a synthetic $(\infty, 1)$ -category of $(\infty, 1)$ -categories.

7.2 An NNO in STT

In STT, one can define the type $NNO_{dir} : = Σ_{X} Σ_{x_{0} : 1 \to X} Σ_{s : X \to X} isInitial_{dir} (X, x_{0}, s),$ where $isInitial_{dir}$ uses directed mapping spaces. The contractibility of $NNO_{dir}$ should follow once the universe is shown to be Rezk-complete in STT—a property partially proved by Gratzer–Weinberger–Buchholtz for the universe of discrete types.

Remark 32 (Open). A complete contractibility result for $NNO_{dir}$ in the universe of discrete types of would give a synthetic proof of 24, internal to STT. We are not aware of a published proof.

7.3 Cubical type theory

Cubical type theory provides a constructive interpretation of the univalence axiom: rather than postulating $ua$ as an axiom, cubical type theory produces it as a defined term. The interpretation uses a primitive notion of path based on the cube category.

Remark 33. In cubical type theory, the contractibility of $NNO$ (9) becomes a constructive theorem: the centre of contraction $(N, zero, succ, ⋆)$ can be computed, and the contraction map sends each $(X, x_{0}, s, ι)$ to a concrete cube witnessing the path. This is the basis for a Cubical Agda formalisation; we leave such a formalisation to future work.

Remark 34 (Cubical NNO). The constructive content of Lambek’s theorem (4) is also more transparent in cubical type theory: the inverse $h : N \to 1 + N$ of the structure map is computed by case analysis on $zero$ vs $succ n$ , with the round-trip equations $ι \circ h = id$ and $h \circ ι = id$ holding judgmentally.

7.4 Comparing internal language flavours

HoTT internal language: $(\infty, 1)$ -toposes (Shulman ); types are $\infty$ -groupoids.
STT internal language: $(\infty, 1)$ -categories (Riehl–Shulman ). Types are general $(\infty, 1)$ -spaces.
Cohesive HoTT: differential and geometric ambient toposes (Schreiber–Shulman ).

For the NNO, all three internal languages give equivalent answers when restricted to discrete types, but only the first two have published contractibility theorems.

8 Free pointed dynamical system on the empty set

A useful recasting of the NNO is as the free pointed dynamical system on the empty set.

Theorem 35 (NNO as left adjoint to a forgetful). The forgetful functor $U : PtEndo (Set) \to Set$ , $(X, x_{0}, f) \mapsto X$ , has a left adjoint $F : Set \to PtEndo (Set)$ . Moreover, $F (\emptyset) = (N, zero, succ)$ , the NNO of $Set$ .

Proof. Define $F (A) : = (A ⊔ N \times A, inj_{2} (0, -), shift)$ where $shift$ takes $a \in A$ to $inj_{2} (1, a)$ and $(n, a)$ to $(succ n, a)$ . The unit $η_{A} : A \to U (F (A)) = A ⊔ N \times A$ is the inclusion of $A$ as the first summand. The counit $ϵ_{(X, x_{0}, f)} : F (U (X, x_{0}, f)) \to (X, x_{0}, f)$ extends $id_{X}$ on the $X$ -summand and applies $f^{n}$ to $(n, x)$ on the $N \times X$ -summand. Verification of the triangle identities is straightforward.

For $A = \emptyset$ , $F (\emptyset) = (\emptyset ⊔ N \times \emptyset, -, -) = (N, zero, succ)$ since $N \times \emptyset ≃ \emptyset$ and the basepoint becomes $zero$ , the shift becomes the successor. ◻

Corollary 36 (Hom characterisation). $Hom_{PtEndo (Set)} ((N, zero, succ), (X, x_{0}, f))$ is naturally isomorphic to a singleton, expressing that $N$ is initial.

Proof. By adjunction $Hom_{PtEndo} (N, (X, x_{0}, f)) ≅ Hom_{Set} (\emptyset, X) = 1$ . ◻

8.1 Lifting to $(\infty, 1)$ -toposes

The same construction applies in any $(\infty, 1)$ -topos $E$ with finite coproducts and pullbacks: $F ⊣ U$ where $U : PtEndo (E) \to E$ is the underlying-object functor. The image of the empty (initial) object under $F$ is the NNO of $E$ .

Remark 37. This is the cleanest abstract characterisation: the NNO is the value of the free-pointed-dynamical-system functor at the initial object. 9 then says that this functor is well-defined up to a contractible space of choices.

9 Lurie’s parametrised NNO in detail

Lurie’s actual definition in is somewhat more subtle than 12: it is parametrised over a base.

Definition 38 (Parametrised NNO ). Let $E$ be an $(\infty, 1)$ -topos and let $S \in E$ . A relative NNO over $S$ is an object $N_{S} \to S$ in $E / S$ , equipped with $0_{S} : S \to N_{S}$ and $s_{S} : N_{S} \to N_{S}$ over $S$ , such that $(N_{S}, 0_{S}, s_{S})$ is the NNO of the slice $E / S$ .

The absolute case is recovered by taking $S = 1$ .

Theorem 39 (Parametrisation is contractibly functorial). The assignment $S \mapsto NNO (E / S)$ extends to a functor $E^{op} \to S$ , valued in contractible spaces. Equivalently, the parametrised NNO is, up to a contractible space of choices, functorial in the base.

Sketch. Functoriality is a consequence of pullback functoriality of slices: a morphism $f : S^{'} \to S$ in $E$ induces $f^{*} : E / S \to E / S^{'}$ , which preserves the NNO universal property. Contractibility of each $NNO (E / S)$ is 24 applied to the slice. The two together give a homotopy-coherent functor; the precise claim is that the space of such functors is itself contractible. ◻

Remark 40 (Globalness). Theorem 39 is the precise statement of “the NNO is uniquely determined globally, not just locally.” In a $1$ -topos this would be a single global iso between any two parametrised NNOs; in an $(\infty, 1)$ -topos it is a contractible space of comparison data, which is the right $\infty$ -categorical strengthening.

9.1 Relation to spectra

In stable $(\infty, 1)$ -categories (or more generally in $(\infty, 1)$ -toposes with stable structure), the NNO can be seen as the truncation of a more refined object: the sphere spectrum $S$ , whose underlying space is $Ω^{\infty} S ≃ \prod_{n \geq 0} K (π_{n} S, n)$ .

Remark 41. The $0$ -truncation of the connective sphere spectrum $τ_{\leq 0} S$ is the discrete $Z$ , whose non-negative part is the NNO. This relates the NNO to the homotopy theory of spectra and chromatic homotopy theory.

10 Open problems

Internal-to-external transfer. Make the externalisation step in the proof of 24 fully precise. This includes coherent strictification of the internal type $NNO$ to an external $\infty$ -groupoid.
Elementary case (Rasekh). Prove 23 for elementary $(\infty, 1)$ -toposes without invoking Shulman’s theorem. The latter is currently stated for Grothendieck $(\infty, 1)$ -toposes; the elementary case is conjectural.
Synthetic NNO contractibility in STT. Prove that $NNO_{dir}$ is contractible in simplicial type theory, using only Rezk-completeness of the universe of discrete types.
Course-of-values and primitive recursion. Develop the theory of course-of-values recursion (Paper III Prop. 6.3) at the $(\infty, 1)$ -categorical level, including coherent dependent induction.
Lurie’s parametrised NNO. Compare the parametrised version (over a base $S \in E$ ) with the absolute version studied here. Show that the parametrisation is functorial up to contractible choice.
Cubical Agda formalisation. Formalise 24 in Cubical Agda, using the existing development of $(\infty, 1)$ -toposes-as-models (cf. Mortberg–Vezzosi).
Univalent foundations of arithmetic. Use 24 to formalise basic arithmetic theorems—associativity and commutativity of $+$ , distributivity—at the $(\infty, 1)$ -categorical level, with all coherences automatic.

11 Recursion principles at the $(\infty, 1)$ -categorical level

The recursion principle $rec_{N}$ generalises in several ways inside an $(\infty, 1)$ -topos. In this section we collect those generalisations and explain the role played by contractibility in each.

11.1 Iteration vs primitive recursion

Definition 42 (Primitive recursion). Given $X \in E$ , $x_{0} : 1 \to X$ , and $k : N \times X \to X$ , primitive recursion produces $g : N \to X$ with $g (zero) = x_{0}$ and $g (succ n) = k (n, g (n))$ .

Proposition 43 (Primitive recursion from iteration). Primitive recursion is reducible to iteration via the state-space pointed dynamical system $(N \times X, (0, x_{0}), step)$ with $step (n, x) : = (succ n, k (n, x))$ . The recursor for this system, post-composed with the projection $pr_{2} : N \times X \to X$ , gives $g$ .

Proof. The recursor $h : N \to N \times X$ for $(N \times X, (0, x_{0}), step)$ satisfies $h (zero) = (0, x_{0})$ and $h (succ n) = step (h (n))$ . Inductively, $pr_{1} (h (n)) = n$ and $pr_{2} (h (n)) = g (n)$ , where $g$ is defined by the primitive-recursion equations. ◻

11.2 Course-of-values recursion

Definition 44 (Course-of-values recursion). Given $X \in E$ and $ϕ : (N \to X) \to (N \to X)$ such that $ϕ (f) (n)$ depends only on the values $f (0), \dots, f (n - 1)$ , course-of-values recursion produces a unique fixed point $g : N \to X$ .

The standard reduction uses the history state space $List (X)$ :

Proposition 45. Course-of-values recursion is reducible to iteration via the state space $(N \times List (X), (0, nil), step_{List})$ , where $step_{List} (n, ℓ) : = (succ n, ℓ + + [ϕ (lookup (ℓ)) (n)])$ .

11.3 Dependent induction

In a locally cartesian closed $(\infty, 1)$ -category, the NNO satisfies dependent induction.

Theorem 46 (Dependent induction from NNO). Let $E$ be locally cartesian closed with NNO $(N, 0, s)$ . For any morphism $P : N \to U$ , with $p_{0} : 1 \to P (0)$ and $p_{s} : \prod_{n : N} P (n) \to P (succ n)$ , there is a unique section $p : \prod_{n : N} P (n)$ with $p (0) = p_{0}$ and $p (succ n) = p_{s} (p (n))$ .

Sketch. Apply iteration in the slice $E / N$ . The total space $Σ_{n : N} P (n)$ becomes a pointed dynamical system over $N$ , and the NNO universal property in the slice gives the section. Locally cartesian closure ensures the slice has the requisite structure. By contractibility (24), the section is unique up to a contractible space of choices. ◻

12 Worked examples

In this section we illustrate 24 on three concrete $(\infty, 1)$ -toposes, in order of increasing geometric complexity.

12.1 The terminal $(\infty, 1)$ -topos: $S$

The $(\infty, 1)$ -category $S$ of $\infty$ -groupoids (“spaces”) is the terminal $(\infty, 1)$ -topos. By 17 it has an NNO; concretely, this is the discrete groupoid $N$ viewed as a $0$ -truncated space.

Example 47 (NNO in $S$ ). The space $NNO (S)$ has as objects pairs $(X, ρ)$ where $X \in S$ and $ρ$ is initial-data identifying $X$ with $N$ . By 24(2), $NNO (S)$ is contractible. Concretely, every object can be connected to $(N, id)$ by a unique-up-to-contractible-choice path, and the higher-dimensional cells of $NNO (S)$ are all contractible.

12.2 Presheaf $(\infty, 1)$ -toposes

For a small $(\infty, 1)$ -category $C$ , the $(\infty, 1)$ -topos $PSh (C) : = Fun (C^{op}, S)$ is presentable, hence by 17 has an NNO.

Proposition 48. The NNO of $PSh (C)$ is the constant functor $c \mapsto N \in S$ , with structure maps inherited pointwise. Its space of NNO structures is contractible.

Proof. Since the constant functor $Δ : S \to PSh (C)$ preserves limits (it is right adjoint to the colimit-evaluation), it sends the NNO $N \in S$ to a pointed dynamical system in $PSh (C)$ , denoted $Δ (N)$ . The recursion principle for $Δ (N)$ is verified pointwise. Contractibility follows from 24 applied to $PSh (C)$ . ◻

Example 49 (Simplicial spaces). For $C = Δ^{op}$ , $PSh (Δ^{op})$ is the $(\infty, 1)$ -topos of simplicial spaces; the NNO is the bisimplicial set whose every level is the discrete space $N$ .

12.3 Sheaves on a topological space

Example 50 (Sheaf $(\infty, 1)$ -topos). For a topological space $T$ (or, more generally, a Grothendieck site $C$ ), the $(\infty, 1)$ -topos $Sh (T)$ has as NNO the constant sheaf $\underline{N}$ , which assigns to each open $U \subseteq T$ the discrete space of locally constant $N$ -valued functions $U \to N$ . Equivalently, $\underline{N} = colim_{n \geq 0} 1_{T}^{⊔ n}$ . Its NNO-space is contractible by 24.

12.4 The cohesive case

When $E$ is a cohesive $(\infty, 1)$ -topos , the NNO sits in the discrete sub- $(\infty, 1)$ -topos $disc (S) ↪ E$ and remains contractible there. The cohesive structure adds geometric information (smooth, differential, supersmooth) but does not affect the discrete arithmetic; this is the modular composition pattern in action.

13 Comparison with classical Peano arithmetic

We pause to relate the universal-property NNO to Peano’s axioms, as a sanity check that all the abstract machinery agrees with the classical picture.

Theorem 51 (Equivalence NNO $\Leftrightarrow$ Peano in $Set$ ). A triple $(N, 0 : 1 \to N, s : N \to N)$ in $Set$ is an NNO iff it satisfies the Peano axioms:

$0 \in N$ .
$s$ is a function $N \to N$ .
$s (n) \neq = 0$ for all $n \in N$ .
$s$ is injective.
Induction: any subset $A \subseteq N$ with $0 \in A$ and closed under $s$ equals $N$ .

Sketch. ( $\Rightarrow$ ) Suppose $(N, 0, s)$ is an NNO. (P1)–(P2) are immediate. (P3): the recursor for $({T, F}, T, \neg)$ produces $h : N \to {T, F}$ with $h (0) = T$ and $h (s n) = \neg h (n)$ ; injectivity of ${T, F}$ -valued recursion forces $s (n) \neq = 0$ . (P4) is more subtle: a clever choice of pointed dynamical system (with carrier $1 + N$ ) yields a left-inverse to $s$ , hence injectivity. (P5) is the universal property restricted to subsets, characteristic-functioned via ${T, F}$ . ( $\Leftarrow$ ) Conversely, Peano’s axioms define a unique-up-to-iso initial pointed dynamical system; the iteration construction yields the recursor. ◻

Remark 52. In an arbitrary $1$ -topos, “injectivity” must be expressed via monomorphisms, “not equal” via disjointness in $1 ⨿ N$ , and “induction over subsets” via the subobject classifier. The proof goes through with these modifications. In an $(\infty, 1)$ -topos, induction must additionally be replaced by induction over $(- 1)$ -truncated maps; the contractibility theorem ensures this still gives an NNO.

13.1 Internal Peano in HoTT

In HoTT, Peano’s axioms are not separate theorems but are packaged into the inductive type $N$ together with the propositional uniqueness encoded by the recursion and induction principles. This is again an instance of the modular composition: each axiom emerges as a corollary of the universal property, hence of contractibility.

Proposition 53 (Disjointness of constructors). In HoTT, $Π_{n : N} \neg (succ n = zero)$ , and similarly $Π_{m, n : N} (succ m = succ n) \to (m = n)$ .

Idea. Define $decode : N \to Type$ by $decode (zero) : = 1$ , $decode (succ n) : = 0$ . By $succ n = zero$ , transport gives $0 \to 1$ , contradicting $0$ ’s emptiness when combined with the inhabitant of $decode (zero)$ . ◻

14 Discussion

14.1 Philosophical remarks

The contractibility theorem solves, at the $(\infty, 1)$ -categorical level, a version of Benacerraf’s problem : “which set is the natural numbers?” becomes “which $\infty$ -groupoid is the natural numbers?” The answer is: any one of them, but they are all canonically the same—and the canonicality is itself part of the data. There is no genuine choice to be made beyond “the type of NNOs is contractible.”

14.2 Relationship to other modular foundations

In the modular framework adopted by the broader research programme, the NNO sits at the bottom of a tower:

NNO (this paper): provides arithmetic.
Real numbers HIIT: built on $N$ (Paper V §5).
Coalgebraic transcendentals: built on streams over $R$ (Topic 1).
$(\infty, 1)$ -Langlands: built on $R, Q_{p}, A$ (Topic 2).
Higher inductive types of all kinds: built on the entire HoTT framework (Topic 6).

The contractibility of NNO at the $(\infty, 1)$ -level ensures that everything built on top of NNO inherits a unique, canonical foundation. This is the modular composition principle: each layer is uniquely determined by the previous one, up to contractible choice.

14.3 Limitations

Shulman’s interpretation theorem currently covers Grothendieck $(\infty, 1)$ -toposes, not all elementary ones. The full transfer of 9 to elementary $(\infty, 1)$ -toposes therefore remains conjectural.
Higher coherence verification, while “automatic” in HoTT, requires actual computation in concrete models. We have not exhibited explicit cellular witnesses for, say, the bisimplicial set model.
The connection to Rasekh’s circle-construction is via contractibility: we know the two NNOs agree, but we do not give an explicit comparison map.

15 Conclusion

The natural numbers object is one of the simplest universal constructions in category theory; nonetheless, lifting it from the $1$ -categorical to the $(\infty, 1)$ -categorical setting illustrates the full power of modern higher-categorical machinery. The key insight is that contractibility, as defined in HoTT (a single propositional condition), automatically encodes an infinite tower of homotopy coherences. This makes HoTT the ideal language to state and prove $(\infty, 1)$ -categorical universal properties without the bookkeeping of explicit cell-by-cell verification.

We have presented:

the $1$ -categorical NNO and its contractibility (7);
Lurie’s parametrised $(\infty, 1)$ -NNO (12) and its existence for presentable $E$ (17);
Rasekh’s circle-construction of an NNO in any elementary $(\infty, 1)$ -topos (18);
the main contractibility theorem (24) showing $NNO (E)$ is contractible whenever HoTT models in $E$ ;
a synthetic perspective via simplicial type theory.

The remaining open problems—particularly the synthetic STT proof and the Cubical Agda formalisation—are within reach of current methods. Once completed, they will close the gap between the conceptual “contractibility solves it” answer and the explicit cellular-coherent verification.

Acknowledgements

The author thanks the Magneton Research Collective for ongoing discussion, and acknowledges the foundational work of Lurie, Rasekh, Shulman, Riehl, and the HoTT community.

16 Operational verification in Haskell

The companion source tree at src/infinity-nno/ contains a Haskell encoding of the NNO universal property. The relevant types and functions are:

NNO.PtEndo a – a record type with fields ptBase :: a and ptStep :: a -> a, representing a pointed dynamical system on a Haskell type a.
NNO.rec :: PtEndo a -> Integer -> a – the recursor witnessing the universal property of $(N, zero, succ)$ . By construction rec pe 0 == ptBase pe and rec pe (n+1) == ptStep pe (rec pe n) for $n \geq 0$ .
NNO.lambekIso :: Integer -> Bool – a property check that the structure map $[zero, succ] : 1 + N \to N$ is invertible (Lambek’s theorem in operational form).
Properties.runChecks :: Bool – a battery of property checks combining prop_rec_zero, prop_rec_step, and prop_lambek.
Proofs.canonicalIsoIsId and Proofs.uniqueAutoIsId – operational counterparts of 3 and 7, demonstrating that the canonical iso between two NNOs is the identity and that the automorphism group is trivial.

The Main.hs module exhibits the universal property on concrete examples including factorial via primitive recursion (43).

17 Mechanised proof in Lean 4

The companion Lean file lean/infinity-nno/NNO.lean contains a self-contained mechanisation of the universal property and Lambek’s theorem, suitable for use with Mathlib4. Highlights:

InfinityNNO.PtEndo – a structure on a type $α$ with fields base : $α$ and step : $α \to α$ .
InfinityNNO.rec – the recursor, defined by pattern matching on Nat.
InfinityNNO.recExists – existence half of the universal property: $\exists h : N \to α$ satisfying both equations.
InfinityNNO.recUnique – uniqueness, by induction on Nat.
InfinityNNO.recUniversal – combined statement: the recursor is the unique such function.
InfinityNNO.lambek – the structure map $[zero, succ] : Unit \oplus N \to N$ is bijective.
InfinityNNO.aut_is_id – any successor-preserving automorphism of $N$ fixing $zero$ is the identity.

The Lean development is intentionally minimal. A more ambitious development would use Mathlib’s CategoryTheory.NaturalNumberObject formalisation and prove the universal property at the level of arbitrary categories with a terminal object.

18 Notation summary

For reference, we collect the principal symbols used in this paper.

$E$ – a (1- or $(\infty, 1)$ -)topos.
$1$ – a terminal object of $E$ .
$PtEndo (E)$ – the (1- or $(\infty, 1)$ -)category of pointed dynamical systems in $E$ .
$(N, 0, s)$ – an NNO: object, basepoint, successor.
$rec (x_{0}, f)$ – the recursor: the unique map $N \to X$ given $(X, x_{0}, f) \in PtEndo (E)$ .
$NNO$ – in HoTT, the type of NNO structures (8).
$NNO (E)$ – the external space of NNO structures in $E$ .
$S$ – the $(\infty, 1)$ -category of $\infty$ -groupoids (“spaces”).
$S^{1}$ – the circle as a HIT.
$Map_{C} (X, Y)$ – the mapping space in an $(\infty, 1)$ -category $C$ .
$isContr$ , $isProp$ , $isSet$ – the standard truncation predicates.
$≃$ – type-theoretic equivalence; $≅$ – categorical isomorphism.
$ua$ – the univalence axiom; $idtoeqv$ – its inverse.

J. Lurie, Higher Topos Theory, Annals of Mathematics Studies, vol. 170, Princeton University Press, 2009. arXiv:math/0608040.

J. Lurie, Spectral Algebraic Geometry, manuscript, February 2018. https://www.math.ias.edu/~lurie/papers/SAG-rootfile.pdf.

N. Rasekh, A Theory of Elementary Higher Toposes, 2018. arXiv:1805.03805.

N. Rasekh, Every Elementary Higher Topos has a Natural Number Object, Theory and Applications of Categories 37, no. 13 (2021), 337–377. arXiv:1809.01734.

M. Shulman, All $(\infty, 1)$ -toposes have strict univalent universes, 2019. arXiv:1904.07004.

The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study, 2013. https://homotopytypetheory.org/book/.

D. R. Licata and M. Shulman, Calculating the fundamental group of the circle in homotopy type theory, LICS 2013, 223–232.

E. Riehl and M. Shulman, A type theory for synthetic $\infty$ -categories, Higher Structures 1 (2017), no. 1, 147–224. arXiv:1705.07442.

D. Gratzer, J. Weinberger, and U. Buchholtz, Directed univalence in simplicial homotopy type theory, 2024. arXiv:2407.09146.

U. Schreiber and M. Shulman, Quantum gauge field theory in cohesive homotopy type theory, EPTCS 158 (2014), 109–126.

J. Lambek, A fixpoint theorem for complete categories, Math. Z. 103 (1968), 151–161.

F. W. Lawvere, An elementary theory of the category of sets, PNAS 52 (1964), 1506–1511.

S. Awodey, Type theory and homotopy, in Epistemology versus Ontology, Springer, 2012, 183–201.

P. Benacerraf, What numbers could not be, Philosophical Review 74 (1965), 47–73.

V. Voevodsky, Univalent foundations, lecture notes, Institute for Advanced Study, 2011. https://www.math.ias.edu/vladimir/Site3/Univalent_Foundations.html.

P. Martin-Löf, Intuitionistic Type Theory, Bibliopolis, Naples, 1984.

C. Rezk, Toposes and homotopy toposes, lecture notes, University of Illinois at Urbana–Champaign, 2010. https://faculty.math.illinois.edu/~rezk/homotopy-topos-sketch.pdf.

A. Joyal, Notes on quasi-categories, manuscript, June 2008. https://www.math.uchicago.edu/~may/IMA/Joyal.pdf.

D.-C. Cisinski, Higher Categories and Homotopical Algebra, Cambridge Studies in Advanced Mathematics, vol. 180, Cambridge University Press, 2019.

YonedaAI, The Universal Property Perspective: Numbers as Initial Successor Structures, Magneton Research Collective, 2026.

YonedaAI, The HoTT Perspective: Numbers as Inductive Types up to Path Equivalence, Magneton Research Collective, 2026.

YonedaAI, The Univalent Correspondence: Synthesis, Magneton Research Collective, 2026.

K. Kapulkin and P. L. Lumsdaine, The simplicial model of univalent foundations (after Voevodsky), J. Eur. Math. Soc. 23 (2021), 2071–2126.

C. Cohen, T. Coquand, S. Huber, and A. Mörtberg, Cubical Type Theory: a constructive interpretation of the univalence axiom, TYPES 2015. arXiv:1611.02108.

E. Riehl, Synthetic perspectives on spaces and categories, 2025. arXiv:2510.15795.

The nLab, elementary $(\infty, 1)$ -topos, https://ncatlab.org/nlab/show/elementary+(infinity,1)-topos, accessed 2026.

The nLab, natural numbers object, https://ncatlab.org/nlab/show/natural+numbers+object, accessed 2026.

Throughout, “Paper III”, “Paper V”, etc. refer to companion papers in the present author’s series The Univalent Correspondence, cited in the bibliography. The relevant statements and proofs are reproduced inline in this paper.↩︎