Natural numbers from integers

TL;DR

The paper addresses constructing a natural number type from an integer type in predicative homotopy type theory without universes. It presents two complementary strategies: a direct approach that builds a near-natural-number that stabilizes to $\mathbb{N}$ by decomposing $\mathbb{Z}$ into halves and using a universal-property argument, and an indirect approach that builds a small, custom universe from fixpoints on $\mathbb{Z} \sqcup \mathbb{Z}$, employs counting structures and stabilization, and then extracts $\mathbb{N}$. Both constructions rely on a restricted toolkit (finite sums, identity types, extensional products) plus a descent principle for a two-element type $\mathbf{2}$, enabling a universe-free realization of natural numbers from integers. A key result is the equivalence $\mathbb{Z} \simeq \mathbb{Z} \sqcup \mathbb{Z}$ and the subsequent decomposition into subparts that guide the natural-number construction; the work generalizes to locally cartesian closed categories with finite colimits satisfying descent. The authors formalize the first approach in Agda, show that the natural numbers are 0-truncated, and articulate broader categorical implications, demonstrating that a natural-number object can be derived from an integer object in a broad predicative setting. The work provides a simpler, universe-free pathway to natural numbers from integers, with potential impact on models of HoTT and constructive type theories.

Abstract

In homotopy type theory, a natural number type is freely generated by an element and an endomorphism. Similarly, an integer type is freely generated by an element and an automorphism. Using only dependent sums, identity types, extensional dependent products, and a type of two elements with large elimination, we construct a natural number type from an integer type. As a corollary, homotopy type theory with only $Σ$, $\mathsf{Id}$, $Π$, and finite colimits with descent (and no universes) admits a natural number type. This improves and simplifies a result by Rose.

Theorems & Definitions (22)

• lemma 1
• definition 1
• lemma 2
• theorem 1
• lemma 3: \agdahtmlurlDoubling.html#1151
• Remark 4.1
• lemma 4: \agdahtmlurlSigns.html
• lemma 5: \agdahtmlurlRollingRule.html
• proposition 1: \agdahtmlurlM.html#3387
• lemma 6: \agdahtmlurlM.html#1690