Contents

foundations

# Contents

## Idea

In type theory: the the natural numbers type is the type of natural numbers.

## Definition

###### Definition

The type of natural numbers $\mathbb{N}$ is the inductive type defined by the following inference rules.

1. $\frac{}{ \mathclap{\phantom{\vert^{\vert}}} \mathbb{N} \,\colon\, Type }$
2. $\frac{}{ \mathclap{\phantom{\vert^{\vert}}} 0 \,\colon\, \mathbb{N} } \;\;\;\;\;\;\;\; \frac{ n \,\colon\, \mathbb{N} \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} succ(n) \,\colon\, \mathbb{N} }$
3. $\frac{ n \,\colon\, \mathbb{N} \;\vdash\; P(n) \,\colon\, Type \;; \;\;\;\; \vdash\; 0_P \,\colon\, P(0) \;; \;\;\;\; n \,\colon\, \mathbb{N} \,, \; p \,\colon\, P(x) \;\vdash\; succ_P(n,\,p) \,\colon\, P\big(succ(n)\big) \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} n \,\colon\, \mathbb{N} \;\vdash\; ind_{(P, 0_P, succ_P)}(n) \,\colon\, P(n) }$
4. $\frac{ n \,\colon\, \mathbb{N} \;\vdash\; P(n) \,\colon\, Type \;; \;\;\;\; \vdash\; 0_P \,\colon\, P(0) \;; \;\;\;\; n \,\colon\, \mathbb{N} \,, \; p \,\colon\, P(x) \;\vdash\; succ_P(n,p) \,\colon\, P\big(succ(n)\big) \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} ind_{(P, 0_P, succ_P)}(0) \,=\, 0_P }$

and

$\frac{ n \,\colon\, \mathbb{N} \;\vdash\; P(x) \,\colon\, Type \;; \;\;\;\; \vdash\; 0_P \,\colon\, P(0) \;; \;\;\;\; n \,\colon\, \mathbb{N} \,, \; p \,\colon\, P(x) \;\vdash\; succ_P(x,p) \,\colon\, P(s x) \;; \;\;\;\; \vdash\; n \,\colon\, \mathbb{N} \mathclap{\phantom{\vert_{\vert}}} }{ \mathclap{\phantom{\vert^{\vert}}} ind_{(P, 0_P, succ_P)}\big(succ(n)\big) \,=\, succ_P\big(n,\, ind_{(P, 0_P, succ_P)}(n) \big) }$

(In the last line, “$=$” denotes judgemental equality.)

That this is the right definition (and a special case of the general principle of inductive types) was clearly understood around Martin-Löf (1984), pp. 38; Coquand & Paulin (1990, p. 52-53); Paulin-Mohring (1993, §1.3); Dybjer (1994, §3). For review see also, e.g., Pfenning (2009, §2); UFP (2013, §1.9); Söhnen (2018, §2.4.5).

In Coq-syntax the natural numbers are the inductive type defined [cf. Paulin-Mohring (2014, p. 6)] by:

Inductive nat : Type :=
| zero : nat
| succ : nat -> nat.

In the categorical semantics (via the categorical model of dependent types, see below) this is interpreted as the initial algebra for the endofunctor $F$ that sends an object to its coproduct with the terminal object

(1)$F(X) \;\coloneqq\; * \sqcup X \,,$

or in different equivalent notation, which is very suggestive here:

$F(X) \;=\; 1 + X \,.$

That initial algebra is (as also explained there) precisely a natural number object $\mathbb{N}$. The two components of the morphism $F(\mathbb{N}) \to \mathbb{N}$ that defines the algebra structure are the 0-element $0 \,\colon\, * \to \mathbb{N}$ and the successor endomorphism $succ \colon \mathbb{N} \to \mathbb{N}$

$(0 ,\, succ) \;\colon\; * \sqcup \mathbb{N} \longrightarrow \mathbb{N} \,.$

### With typal computation and uniqueness rules

Assuming that identification types, function types and dependent sequence types exist in the type theory, the natural numbers type is the inductive type generated by an element and a function:

Formation rules for the natural numbers type:

$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathbb{N} \; \mathrm{type}}$

Introduction rules for the natural numbers type:

$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 0:\mathbb{N}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash s:\mathbb{N} \to \mathbb{N}}$

Elimination rules for the natural numbers type:

$\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x)) \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \mathrm{ind}_\mathbb{N}^C(c_0, c_s, n):C(n)}$

Computation rules for the natural numbers type:

$\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x))}{\Gamma \vdash \beta_\mathbb{N}^0(c_0, c_s):\mathrm{Id}_{C(0)}\mathrm{ind}_\mathbb{N}^C(c_0, c_s, 0), c_0)}$
$\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x)) \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \beta_\mathbb{N}^s(c_0, c_s, n):\mathrm{Id}_{C(s(n))}(\mathrm{ind}_\mathbb{N}^C(c_0, c_s, s(n)), c_s(n)(\mathrm{ind}_\mathbb{N}^C(c_0, c_s, n)))}$

Uniqueness rules for the natural numbers type:

$\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c:\prod_{x:\mathbb{N}} C(x) \quad \Gamma \vdash n:\mathbb{N}}{\Gamma \vdash \eta_\mathbb{N}(c, n):\mathrm{Id}_{C(n)}(\mathrm{ind}_\mathbb{N}^C(c(0), \lambda x:\mathbb{N}.c(s(x)), n), c(n))}$

The elimination, computation, and uniqueness rules for the natural numbers type state that the natural numbers type satisfy the dependent universal property of the natural numbers. If the dependent type theory also has dependent sum types and product types, allowing one to define the uniqueness quantifier, the dependent universal property of the natural numbers could be simplified to the following rule:

$\frac{\Gamma, x:\mathbb{N} \vdash C(x) \; \mathrm{type} \quad \Gamma \vdash c_0:C(0) \quad \Gamma \vdash c_s:\prod_{x:\mathbb{N}} C(x) \to C(s(x))}{\Gamma \vdash \mathrm{up}_\mathbb{N}^C(c_0, c_s):\exists!c:\prod_{x:\mathbb{N}} C(x).\mathrm{Id}_{C(0)}(c(0), c_0) \times \prod_{x:\mathbb{N}} \mathrm{Id}_{C(s(x))}(c(s(x)), c_s(c(x)))}$

### Extensionality principle of the natural numbers

First we inductively define a binary function into the boolean domain called observational equality of the natural numbers:

$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Eq}_\mathbb{N}:\mathbb{N} \times \mathbb{N} \to \mathrm{Bit}}$
$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \delta^{0, 0}:\mathrm{Id}_\mathrm{Bit}(\mathrm{Eq}_\mathbb{N}(0, 0), 1)} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, n:\mathbb{N} \vdash \delta^{0, s}(n):\mathrm{Id}_\mathrm{Bit}(\mathrm{Eq}_\mathbb{N}(0, s(n)), 0)}$
$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, m:\mathbb{N} \vdash \delta^{s, 0}(m):\mathrm{Id}_\mathrm{Bit}(\mathrm{Eq}_\mathbb{N}(s(m), 0), 0)} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma, m:\mathbb{N}, n:\mathbb{N} \vdash \delta^{s, s}(m, n):\mathrm{Id}_\mathrm{Bit}(\mathrm{Eq}_\mathbb{N}(s(m), s(n)),\mathrm{Eq}_\mathbb{N}(m, n))}$

The extensionality principle of the natural numbers states that the natural numbers has decidable equality given by observational equality:

$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, m:\mathbb{N}, n:\mathbb{N} \vdash \delta(m, n):\mathrm{Id}_\mathbb{N}(m, n) \simeq \mathrm{El}_\mathrm{Bit}(\mathrm{Eq}_\mathbb{N}(m, n))}$

or equivalently

$\frac{\Gamma \; \mathrm{ctx}}{\Gamma, m:\mathbb{N}, n:\mathbb{N} \vdash \delta(m, n):\mathrm{Id}_\mathbb{N}(m, n) \simeq \mathrm{Id}_\mathbb{2}(\mathrm{Eq}_\mathbb{N}(m, n), 1)}$

## Properties

### General

###### Example

(natural numbers type as a $\mathcal{W}$-type)
The natural numbers type $(\mathbb{N},\, 0,\, succ)$ (Def. ) is equivalently the $\mathcal{W}$-type $\underset{c \colon C}{\mathcal{W}} A(c)$ with:

• $C \,\coloneqq\, \{0, succ\} \,\simeq\, \ast \sqcup \ast$;

• $A_0 \,\coloneqq\, \varnothing$ (empty type);

$A_{succ} \,\coloneqq\, \ast$ (unit type)

[Martin-Löf (1984), pp. 45, Dybjer (1997, p. 330, 333)]

### Categorical semantics

We spell out how under the canonical categorical model of dependent types, the categorical semantics of the natural numbers types yields a natural numbers object together with its expected recursion and induction principle.

Throughout, we consider an ambient category $\mathcal{C}$ (e.g. $\mathcal{C} =$ Set) and write

(2)$F Alg(\mathcal{C}) \xrightarrow{underlying} \mathcal{C}$

for the category of algebras over the endofunctor $F$ (1).

#### Recursion

We spell out how the fact that $\mathbb{N}$ satisfies Def. is the classical recursion principle.

We begin with a simple special case of recursion (cf. Rem. ), where not only the underlying type but also its successor-map is independent of $\mathbb{N}$ (we come to the general form of recursion further below).

So consider any $F$-algebra $\big(D, (0_D, succ_D)\big) \,\in\, F Alg(\mathcal{C})$ (2), hence an object $D \in \mathcal{C}$ equipped with a morphism

$0_D \colon * \to D$

and a morphism

$succ_D \colon D \to D \,.$

By initiality of the $F$-algebra $\mathbb{N}$, there is then a (unique) morphism

$rec \,\colon\, \mathbb{N} \to D$

such that the following diagram commutes:

$\array{ * &\stackrel{0}{\longrightarrow}& \mathbb{N} &\stackrel{succ}{\longrightarrow}& \mathbb{N} \\ \big\downarrow && \big\downarrow\mathrlap{^\mathrlap{rec}} && \big\downarrow\mathrlap{^\mathrlap{rec}} \\ * &\underset{0_D}{\longrightarrow}& D &\underset{succ_D}{\longrightarrow}& D }$

This means precisely that $rec$ is the function defined recursively by

$rec(0) \;=\; 0_D$

and

(3)$rec\big(succ(n)\big) \;=\; succ_D\big(rec(n)\big) \,.$

More generally, consider an $F$-algebra in the slice over $\big(\mathbb{N}, (0,succ)\big)$, but with the underlying slice object assumed (dropping also this assumption leads to the fully general notion of induction further below) to be independent of $\mathbb{N}$, hence of the form

(4)$\left[ \array{ \mathbb{N} \times D \\ \big\downarrow\mathrlap{^{pr_{\mathbb{N}}}} \\ \mathbb{N} } \;\;\; \right] \;\in\; \mathcal{C}_{/\mathbb{N}} \,,$

while the $F$-algebra structure may now depend on $\mathbb{N}$:

in that

$succ_D \;\colon\; \mathbb{N} \times D \to D$

may depend on $\mathbb{N}$.

Now, since with $\big(\mathbb{N},(0,\mathrm{succ})\big)$ being the initial object in $F Alg(\mathcal{C})$, the identity morphism on $\big(\mathbb{N},(0,\mathrm{succ})\big)$ is the initial object in the slice category $F Alg(\mathcal{C})_{/\big(\mathbb{N}, (0,succ)\big)}$ (cf. there), it follows that from such data is induced a unique morphism $f$ in the following commuting diagram:

Here the commutativity of the top square means equivalently that

$\mathrm{rec}(0) \,=\, 0_D$

and

(5)$\mathrm{rec}\big( \mathrm{succ}(n) \big) \;=\; \mathrm{succ}_D\big(n,\, \mathrm{rec}(n)\big) \,.$

###### Remark

(the need for dependent recursion [cf. Paulin-Mohring (1993, p. 330)])
The appearance of the argument “$n$” on the right of (5) – in contrast to formula (3) for non-dependent recursion – means (in view of the argument “$succ(n)$” on the left) that the recursor $succ_D$ has access to the predecessor partial function $pred \,\colon\,succ(n) \,\mapsto\, n$. This is necessary in order to express all computable functions on the natural numbers inductively and hence explains the need for the dependently typed recursion principle (4)

#### Induction

Dropping the above constraint (4) on the dependent $F$-algebra, we spell out in detail how the fact that $\mathbb{N}$ satisfied Def. is the classical induction principle.

That principle says informally that if a proposition $P$ depending on the natural numbers is true at $n = 0$ and such that if it is true for some $n$ then it is true for $n+1$, then it is true for all natural numbers.

Here is how this is formalized in type theory and then interpreted in some suitable ambient category $\mathcal{C}$.

First of all, that $P$ is a proposition depending on the natural numbers means that it is a dependent type

$n \,\colon\, \mathbb{N} \;\;\vdash\;\; P(n) \,\colon\, Type \,.$

The categorical interpretation of this is by a display map

(6)$\array{ P \\ \big\downarrow\mathrlap{^{\pi_P}} \\ \mathbb{N} }$

in the given category $\mathcal{C}$.

With this, the commuting diagram which interprets the induction principle is the following:

We now unwind again how this comes about and what it all means:

First, the fact that $P$ holds at 0 means that there is a (proof-)term

$\vdash \;\; 0_P \,\colon\, P(0) \,.$

In the categorical semantics the substitution of $n$ for 0 that gives $P(0)$ is given by the pullback of the given display map (6):

$\array{ 0^* P &\longrightarrow& P \\ \big\downarrow && \big\downarrow \\ * &\underset{0}{\longrightarrow}& \mathbb{N} }$

and the term $0_P$ is interpreted as a section of the resulting fibration over the terminal object

$\array{ * &\overset{p_0}{\longrightarrow}& 0^* P & \longrightarrow & P \\ &\searrow& \big\downarrow && \big\downarrow \\ && * &\underset{0}{\longrightarrow}& \mathbb{N} } \,.$

But by the defining universal property of the pullback, this is equivalently just a commuting diagram

$\array{ * &\stackrel{p_0}{\longrightarrow}& P \\ \big\downarrow && \big\downarrow \\ * &\underset{0}{\longrightarrow}& \mathbb{N} } \,.$

Next the induction step. Formally it says that for all $n \in \mathbb{N}$ there is an implication $succ_P(n) \,\colon\, P(n) \to P(n+1)$

$n \in \mathbb{N} \;\;\;\vdash\;\;\; succ_P(n) \,\colon\, P(n) \to P(n+1) \,.$

The categorical semantics of the substitution of $n+1$ for $n$ is given by the pullback

$\array{ P\big(\ast \sqcup (-)\big) \coloneqq & s^*P &\longrightarrow& P \\ & \big\downarrow && \big\downarrow \\ & \mathbb{N} &\underset{s}{\longrightarrow}& \mathbb{N} }$

and the interpretation of the implication term $succ_P(n)$ is as a morphism $P \to s^* P$ in $\mathcal{C}_{/\mathbb{N}}$

$\array{ P & \overset{p_s}{\longrightarrow} & s^*P &\longrightarrow& P \\ &\searrow & \big\downarrow && \big\downarrow \\ && \mathbb{N} &\overset{s}{\longrightarrow}& \mathbb{N} } \,.$

Again by the universal property of the pullback this is equivalently a commuting diagram

$\array{ P &\overset{succ_P}{\longrightarrow}& P \\ \big\downarrow && \big\downarrow \\ \mathbb{N} &\underset{s}{\longrightarrow}& \mathbb{N} } \,.$

In summary this shows that

• $P$ being a proposition depending on natural numbers which holds at 0 and which holds at $n+1$ if it holds at $n$

is interpreted precisely as an endofunctor-algebra homomorphism

$\array{ P \\ \downarrow \\ \mathbb{N} } \,.$

for the endofunctor $F$ (1).

The induction principle is supposed to deduce from this that $P$ holds for every $n$, hence that there is a proof $ind(n) \colon P(n)$ for all $n$:

$n \,\colon\, \mathbb{N} \;\;\;\vdash\;\;\; ind(n) \,\colon\, P(n) \,.$

The categorical interpretation of this is as a morphism $p \,\colon\, \mathbb{N} \to P$ in $\mathcal{C}_{/\mathbb{N}}$. The existence of this is indeed exactly what the interpretation of the elimination rule (Def. ) gives exactly what the initiality of the $F$-algebra $\mathbb{N}$ gives.

Original articles with emphasis on the nature of $\mathbb{N}$ as an inductive type:

The syntax in Coq: