nLab natural numbers type

Redirected from "type of natural numbers".
Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Deduction and Induction

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

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. type formation rule:

    | |:Type \frac{}{ \mathclap{\phantom{\vert^{\vert}}} \mathbb{N} \,\colon\, Type }
  2. term introduction rules:

    | |0:n:| || |succ(n): \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. term elimination rule:

    n:P(n):Type;0 P:P(0);n:,p:P(x)succ P(n,p):P(succ(n))| || |n:ind (P,0 P,succ P)(n):P(n) \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. computation rules:

    n:P(n):Type;0 P:P(0);n:,p:P(x)succ P(n,p):P(succ(n))| || |ind (P,0 P,succ P)(0)=0 P \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

    n:P(x):Type;0 P:P(0);n:,p:P(x)succ P(x,p):P(sx);n:| || |ind (P,0 P,succ P)(succ(n))=succ P(n,ind (P,0 P,succ P)(n)) \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 FF that sends an object to its coproduct with the terminal object

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

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

F(X)=1+X. 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()F(\mathbb{N}) \to \mathbb{N} that defines the algebra structure are the 0-element 0:*0 \,\colon\, * \to \mathbb{N} and the successor endomorphism succ:succ \colon \mathbb{N} \to \mathbb{N}

(0,succ):*. (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:

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

Introduction rules for the natural numbers type:

ΓctxΓ0:ΓctxΓs:\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:

Γ,x:C(x)typeΓc 0:C(0)Γc s: x:C(x)C(s(x))Γn:Γind C(c 0,c s,n):C(n)\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:

Γ,x:C(x)typeΓc 0:C(0)Γc s: x:C(x)C(s(x))Γβ 0(c 0,c s):Id C(0)ind 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))}{\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)}
Γ,x:C(x)typeΓc 0:C(0)Γc s: x:C(x)C(s(x))Γn:Γβ s(c 0,c s,n):Id C(s(n))(ind C(c 0,c s,s(n)),c s(n)(ind C(c 0,c s,n)))\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:

Γ,x:C(x)typeΓc: x:C(x)Γn:Γη (c,n):Id C(n)(ind C(c(0),λx:.c(s(x)),n),c(n))\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:

Γ,x:C(x)typeΓc 0:C(0)Γc s: x:C(x)C(s(x))Γup C(c 0,c s):!c: x:C(x).Id C(0)(c(0),c 0)× x:Id C(s(x))(c(s(x)),c s(c(x)))\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)))}

The dependent universal property of the natural numbers is used to characterize the dependent product type of an type family C(x)C(x) dependent on x:x:\mathbb{N}, and states that the fibers of the function

λc.(c(0),λx.c(s(x))): x:C(x)(C(0)× x:C(x)C(s(x)))\lambda c.(c(0), \lambda x.c(s(x))):\prod_{x:\mathbb{N}} C(x) \to \left(C(0) \times \prod_{x:\mathbb{N}} C(x) \to C(s(x))\right)

are contractible types. This is equivalent to saying that the above function is an equivalence of types:

isEquiv(λc.(c(0),λx.c(s(x))))\mathrm{isEquiv}(\lambda c.(c(0), \lambda x.c(s(x))))

The non-dependent universal property similarly says that given a type CC the function

λc.(c(0),λx.c(s(x))):(C)(C×(CC))\lambda c.(c(0), \lambda x.c(s(x))):(\mathbb{N} \to C) \to \left(C \times (\mathbb{N} \to C \to C)\right)

is an equivalence of types

isEquiv(λc.(c(0),λx.c(s(x))))\mathrm{isEquiv}(\lambda c.(c(0), \lambda x.c(s(x))))

Generalized induction principle

There is also a generalized induction principle (cf. the talk slides in LumsdaineShulman17), which uses a type CC and a function f:Cf:C \to \mathbb{N} instead of a type family x:P(x)x:\mathbb{N} \vdash P(x), and one uses the fiber z:Cf(z)= n\sum_{z:C} f(z) =_\mathbb{N} n to express the generalized induction principle.

Then the induction principle states that given a type CC and a function f:Cf:C \to \mathbb{N} along with

  • dependent pair
c 0: z:Cf(z)= 0c_0:\sum_{z:C} f(z) =_\mathbb{N} 0
  • dependent function
c s: n:( z:Cf(z)= n)( z:Cf(z)= s(n))c_s:\prod_{n:\mathbb{N}} \left(\sum_{z:C} f(z) =_\mathbb{N} n\right) \to \left(\sum_{z:C} f(z) =_\mathbb{N} s(n)\right)
  • and natural number n:n:\mathbb{N}

one could construct the dependent pair

ind C(f,c 0,c s,n): z:Cf(z)= n\mathrm{ind}_\mathbb{N}^C(f, c_0, c_s, n):\sum_{z:C} f(z) =_\mathbb{N} n

such that

ind C(f,c 0,c s,0)c 0\mathrm{ind}_\mathbb{N}^C(f, c_0, c_s, 0) \equiv c_0

and for all n:n:\mathbb{N}

ind C(f,c 0,c s,s(n))c s(n,ind(f,c 0,c s,n))\mathrm{ind}_\mathbb{N}^C(f, c_0, c_s, s(n)) \equiv c_s(n, \mathrm{ind}(f, c_0, c_s, n))

However, by the rules of dependent pair types, one could instead postulate separate elements and identifications instead of an element of a fiber type throughout the generalized principle.

Instead of the dependent pair c 0: z:Cf(z)= 0c_0:\sum_{z:C} f(z) =_\mathbb{N} 0 we have the element c 0:Cc_0:C and identificaiton p 0:f(c 0)= 0p_0:f(c_0) =_\mathbb{N} 0, where the original element is given by (c 0,p 0)(c_0, p_0). In addition, given the dependent type

c s: n:( z:Cf(z)= n)( z:Cf(z)= s(n))c_s:\prod_{n:\mathbb{N}} \left(\sum_{z:C} f(z) =_\mathbb{N} n\right) \to \left(\sum_{z:C} f(z) =_\mathbb{N} s(n)\right)

by currying this is equivalent to

c s: n: z:C(f(z)= n)( z:Cf(z)= s(n))c_s:\prod_{n:\mathbb{N}} \prod_{z:C} \left(f(z) =_\mathbb{N} n\right) \to \left(\sum_{z:C} f(z) =_\mathbb{N} s(n)\right)

and by the type theoretic axiom of choice this is equivalent to

c s: n: y:C g:(f(y)= n)C p:f(y)= nf(g(p))= s(n)c_s:\prod_{n:\mathbb{N}} \prod_{y:C} \sum_{g:(f(y) =_\mathbb{N} n) \to C} \prod_{p:f(y) =_\mathbb{N} n} f(g(p)) =_\mathbb{N} s(n)

By the rules of dependent pair types, the family of dependent pair types could be split up into

c s: n: y:C(f(y)= n)Cc_s:\prod_{n:\mathbb{N}} \prod_{y:C} (f(y) =_\mathbb{N} n) \to C
p s: n: y:C p:f(y)= nf(c s(n,y,p))= s(n)p_s:\prod_{n:\mathbb{N}} \prod_{y:C} \prod_{p:f(y) =_\mathbb{N} n} f(c_s(n, y, p)) =_\mathbb{N} s(n)

where the original dependent funciton is given by

λn:.λy:C.(c s(n,y),p s(n,y))\lambda n:\mathbb{N}.\lambda y:C.(c_s(n, y), p_s(n, y))

Then the induction principle of the natural numbers states that given a type CC and a function f:Cf:C \to \mathbb{N}, along with

  • an element c 0:Cc_0:C

  • an identification p 0:f(c 0)= 0p_0:f(c_0) =_\mathbb{N} 0

  • dependent functions

c s: n: y:C(f(y)= n)Cc_s:\prod_{n:\mathbb{N}} \prod_{y:C} (f(y) =_\mathbb{N} n) \to C
p s: n: y:C p:f(y)= nf(c s(n,y,p))= s(n)p_s:\prod_{n:\mathbb{N}} \prod_{y:C} \prod_{p:f(y) =_\mathbb{N} n} f(c_s(n, y, p)) =_\mathbb{N} s(n)

we have a function

ind C(f,c 0,p 0,c s,p s):C\mathrm{ind}_\mathbb{N}^{C}(f, c_0, p_0, c_s, p_s):\mathbb{N} \to C

and a homotopy

ind C,sec(f,c 0,p 0,c s,p s): n:f(ind C(f,c 0,p 0,c s,p s,n))= n\mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s):\prod_{n:\mathbb{N}} f(\mathrm{ind}_\mathbb{N}^{C}(f, c_0, p_0, c_s, p_s, n)) =_\mathbb{N} n

indicating that ind C(f,c 0,p 0,c s,p s)\mathrm{ind}_\mathbb{N}^{C}(f, c_0, p_0, c_s, p_s) is a section of ff, such that

ind C(f,c 0,p 0,c s,p s,0)c 0\mathrm{ind}_\mathbb{N}^{C}(f, c_0, p_0, c_s, p_s, 0) \equiv c_0
ind C,sec(f,c 0,p 0,c s,p s,0)p 0\mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, 0) \equiv p_0

and for all n:n:\mathbb{N},

ind C(f,c 0,p 0,c s,p s,s(n))c s(n,ind C(f,c 0,p 0,c s,p s,n),ind C,sec(f,c 0,p 0,c s,p s,n))\mathrm{ind}_\mathbb{N}^{C}(f, c_0, p_0, c_s, p_s, s(n)) \equiv c_s(n, \mathrm{ind}_\mathbb{N}^{C}(f, c_0, p_0, c_s, p_s, n), \mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, n))
ind C,sec(f,c 0,p 0,c s,p s,s(n))p s(n,ind C(f,c 0,p 0,c s,p s,n),ind C,sec(f,c 0,p 0,c s,p s,n))\mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, s(n)) \equiv p_s(n, \mathrm{ind}_\mathbb{N}^{C}(f, c_0, p_0, c_s, p_s, n), \mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, n))

As inference rules these are given by the following:

elimination rules:

ΓCtypeΓf:CΓc 0:CΓp 0:f(c 0)= 0 Γc s: n: y:C(f(y)= n)CΓp s: n: y:C p:f(y)= nf(c s(n,y,p))= s(n)Γind C(f,c 0,p 0,c s,p s):C\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to \mathbb{N} \quad \Gamma \vdash c_0:C \quad \Gamma \vdash p_0:f(c_0) =_\mathbb{N} 0 \\ \Gamma \vdash c_s:\prod_{n:\mathbb{N}} \prod_{y:C} (f(y) =_\mathbb{N} n) \to C \quad \Gamma \vdash p_s:\prod_{n:\mathbb{N}} \prod_{y:C} \prod_{p:f(y) =_\mathbb{N} n} f(c_s(n, y, p)) =_\mathbb{N} s(n) \end{array} }{\Gamma \vdash \mathrm{ind}_\mathbb{N}^{C}(f, c_0, p_0, c_s, p_s):\mathbb{N} \to C}
ΓCtypeΓf:CΓc 0:CΓp 0:f(c 0)= 0 Γc s: n: y:C(f(y)= n)CΓp s: n: y:C p:f(y)= nf(c s(n,y,p))= s(n)Γind C,sec(f,c 0,p 0,c s,p s): n:f(ind C(f,c 0,p 0,c s,p s,n))= n\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to \mathbb{N} \quad \Gamma \vdash c_0:C \quad \Gamma \vdash p_0:f(c_0) =_\mathbb{N} 0 \\ \Gamma \vdash c_s:\prod_{n:\mathbb{N}} \prod_{y:C} (f(y) =_\mathbb{N} n) \to C \quad \Gamma \vdash p_s:\prod_{n:\mathbb{N}} \prod_{y:C} \prod_{p:f(y) =_\mathbb{N} n} f(c_s(n, y, p)) =_\mathbb{N} s(n) \end{array} }{\Gamma \vdash \mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s):\prod_{n:\mathbb{N}} f(\mathrm{ind}_\mathbb{N}^{C}(f, c_0, p_0, c_s, p_s, n)) =_\mathbb{N} n}

computation rules:

ΓCtypeΓf:CΓc 0:CΓp 0:f(c 0)= 0 Γc s: n: y:C(f(y)= n)CΓp s: n: y:C p:f(y)= nf(c s(n,y,p))= s(n)Γind C(f,c 0,p 0,c s,p s,0)c 0\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to \mathbb{N} \quad \Gamma \vdash c_0:C \quad \Gamma \vdash p_0:f(c_0) =_\mathbb{N} 0 \\ \Gamma \vdash c_s:\prod_{n:\mathbb{N}} \prod_{y:C} (f(y) =_\mathbb{N} n) \to C \quad \Gamma \vdash p_s:\prod_{n:\mathbb{N}} \prod_{y:C} \prod_{p:f(y) =_\mathbb{N} n} f(c_s(n, y, p)) =_\mathbb{N} s(n) \end{array} }{\Gamma \vdash \mathrm{ind}_\mathbb{N}^{C}(f, c_0, p_0, c_s, p_s, 0) \equiv c_0}
ΓCtypeΓf:CΓc 0:CΓp 0:f(c 0)= 0 Γc s: n: y:C(f(y)= n)CΓp s: n: y:C p:f(y)= nf(c s(n,y,p))= s(n)Γind C,sec(f,c 0,p 0,c s,p s,0)p 0\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to \mathbb{N} \quad \Gamma \vdash c_0:C \quad \Gamma \vdash p_0:f(c_0) =_\mathbb{N} 0 \\ \Gamma \vdash c_s:\prod_{n:\mathbb{N}} \prod_{y:C} (f(y) =_\mathbb{N} n) \to C \quad \Gamma \vdash p_s:\prod_{n:\mathbb{N}} \prod_{y:C} \prod_{p:f(y) =_\mathbb{N} n} f(c_s(n, y, p)) =_\mathbb{N} s(n) \end{array} }{\Gamma \vdash \mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, 0) \equiv p_0}
ΓCtypeΓf:CΓc 0:CΓp 0:f(c 0)= 0 Γc s: n: y:C(f(y)= n)CΓp s: n: y:C p:f(y)= nf(c s(n,y,p))= s(n)Γn:Γind C(f,c 0,p 0,c s,p s,s(n))c s(n,ind C(f,c 0,p 0,c s,p s,n),ind C,sec(f,c 0,p 0,c s,p s,n))\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to \mathbb{N} \quad \Gamma \vdash c_0:C \quad \Gamma \vdash p_0:f(c_0) =_\mathbb{N} 0 \\ \Gamma \vdash c_s:\prod_{n:\mathbb{N}} \prod_{y:C} (f(y) =_\mathbb{N} n) \to C \quad \Gamma \vdash p_s:\prod_{n:\mathbb{N}} \prod_{y:C} \prod_{p:f(y) =_\mathbb{N} n} f(c_s(n, y, p)) =_\mathbb{N} s(n) \quad \Gamma \vdash n:\mathbb{N} \end{array} }{\Gamma \vdash \mathrm{ind}_\mathbb{N}^{C}(f, c_0, p_0, c_s, p_s, s(n)) \equiv c_s(n, \mathrm{ind}_\mathbb{N}^{C}(f, c_0, p_0, c_s, p_s, n), \mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, n))}
ΓCtypeΓf:CΓc 0:CΓp 0:f(c 0)= 0 Γc s: n: y:C(f(y)= n)CΓp s: n: y:C p:f(y)= nf(c s(n,y,p))= s(n)Γn:Γind C,sec(f,c 0,p 0,c s,p s,s(n))p s(n,ind C(f,c 0,p 0,c s,p s,n),ind C,sec(f,c 0,p 0,c s,p s,n))\frac{ \begin{array}{c} \Gamma \vdash C \; \mathrm{type} \quad \Gamma \vdash f:C \to \mathbb{N} \quad \Gamma \vdash c_0:C \quad \Gamma \vdash p_0:f(c_0) =_\mathbb{N} 0 \\ \Gamma \vdash c_s:\prod_{n:\mathbb{N}} \prod_{y:C} (f(y) =_\mathbb{N} n) \to C \quad \Gamma \vdash p_s:\prod_{n:\mathbb{N}} \prod_{y:C} \prod_{p:f(y) =_\mathbb{N} n} f(c_s(n, y, p)) =_\mathbb{N} s(n) \quad \Gamma \vdash n:\mathbb{N} \end{array} }{\Gamma \vdash \mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, s(n)) \equiv p_s(n, \mathrm{ind}_\mathbb{N}^{C}(f, c_0, p_0, c_s, p_s, n), \mathrm{ind}_\mathbb{N}^{C, \mathrm{sec}}(f, c_0, p_0, c_s, p_s, n))}

One gets back the usual induction principle of the natural numbers type when C n:P(n)C \equiv \sum_{n:\mathbb{N}} P(n) and fπ 1f \equiv \pi_1 the first projection function of the dependent sum type, and one gets back the recursion principle of the natural numbers type when C×XC \equiv \mathbb{N} \times X and fπ 1f \equiv \pi_1 the first projection function of the product type.

Extensionality principle of the natural numbers

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

ΓctxΓEq :×Bit\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Eq}_\mathbb{N}:\mathbb{N} \times \mathbb{N} \to \mathrm{Bit}}
ΓctxΓδ 0,0:Id Bit(Eq (0,0),1)ΓctxΓ,n:δ 0,s(n):Id Bit(Eq (0,s(n)),0)\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)}
ΓctxΓ,m:δ s,0(m):Id Bit(Eq (s(m),0),0)ΓctxΓ,m:,n:δ s,s(m,n):Id Bit(Eq (s(m),s(n)),Eq (m,n))\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:

ΓctxΓ,m:,n:δ(m,n):Id (m,n)El Bit(Eq (m,n))\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

ΓctxΓ,m:,n:δ(m,n):Id (m,n)Id 𝟚(Eq (m,n),1)\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 (,0,succ)(\mathbb{N},\, 0,\, succ) (Def. ) is equivalently the 𝒲 \mathcal{W} -type 𝒲c:CA(c)\underset{c \colon C}{\mathcal{W}} A(c) with:

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

  • A 0A_0 \,\coloneqq\, \varnothing (empty type);

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

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

Relation to the type of finite types

The natural numbers type is equivalent to the set truncation of the type of finite types:

[FinType] 0\mathbb{N} \simeq [\mathrm{FinType}]_0

This is the type theoretic analogue of the decategorification of the permutation category resulting in the set of natural numbers.

This gives us an alternate definition of the natural numbers as the type of finite types

[FinType] 0\mathbb{N} \coloneqq [\mathrm{FinType}]_0

One has [] 0:FinType[FinType] 0[-]_0:\mathrm{FinType} \to [\mathrm{FinType}]_0 by the introduction rules of set truncation.

The arithmetic operations and order relations on the natural numbers type can be defined by induction on set truncation:

For all finite types A:FinTypeA:\mathrm{FinType} and B:FinTypeB:\mathrm{FinType} and finite families C:AFinTypeC:A \to \mathrm{FinType}, we have

0= [] 01= [𝟙] 00 =_\mathbb{N} [\emptyset]_0 \quad 1 =_\mathbb{N} [\mathbb{1}]_0
[A] 0+[B] 0= [A+B] 0[A]_0 + [B]_0 =_\mathbb{N} [A + B]_0
x=1 [A] 0[C] 0(x)= [ x:AC(x)] 0\sum_{x = 1}^{[A]_0} [C]_0(x) =_\mathbb{N} \left[\sum_{x:A} C(x)\right]_0
[A] 0[B] 0= [A×B] 0[A]_0 \cdot [B]_0 =_\mathbb{N} [A \times B]_0
x=1 [A] 0[C] 0(x)= [ x:AC(x)] 0\prod_{x = 1}^{[A]_0} [C]_0(x) =_\mathbb{N} \left[\prod_{x:A} C(x)\right]_0
[B] 0 [A] 0= [AB] 0[B]_0^{[A]_0} =_\mathbb{N} [A \to B]_0
[A] 0= [B] 0[AB] (1)or[A= FinTypeB] (1)[A]_0 =_\mathbb{N} [B]_0 \coloneqq [A \simeq B]_{(-1)} \; \mathrm{or} \; [A =_\mathrm{FinType} B]_{(-1)}
[A] 0[B] 0[AB] (1)[A]_0 \leq [B]_0 \coloneqq [A \hookrightarrow B]_{(-1)}

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)FAlg(𝒞)underlying𝒞 F Alg(\mathcal{C}) \xrightarrow{underlying} \mathcal{C}

for the category of algebras over the endofunctor FF (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 FF-algebra (D,(0 D,succ D))FAlg(𝒞)\big(D, (0_D, succ_D)\big) \,\in\, F Alg(\mathcal{C}) (2), hence an object D𝒞D \in \mathcal{C} equipped with a morphism

0 D:*D 0_D \colon * \to D

and a morphism

succ D:DD. succ_D \colon D \to D \,.

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

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

such that the following diagram commutes:

* 0 succ rec rec * 0 D D succ D D \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 recrec is the function defined recursively by

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

and

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

More generally, consider an FF-algebra in the slice over (,(0,succ))\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)[×D pr ]𝒞 /, \left[ \array{ \mathbb{N} \times D \\ \big\downarrow\mathrlap{^{pr_{\mathbb{N}}}} \\ \mathbb{N} } \;\;\; \right] \;\in\; \mathcal{C}_{/\mathbb{N}} \,,

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

in that

succ D:×DD succ_D \;\colon\; \mathbb{N} \times D \to D

may depend on \mathbb{N}.

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

Here the commutativity of the top square means equivalently that

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

and

(5)rec(succ(n))=succ D(n,rec(n)). \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 “nn” on the right of (5) – in contrast to formula (3) for non-dependent recursion – means (in view of the argument “succ(n)succ(n)” on the left) that the recursor succ Dsucc_D has access to the predecessor partial function pred:succ(n)npred \,\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 FF-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 PP depending on the natural numbers is true at n=0n = 0 and such that if it is true for some nn then it is true for n+1n+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 PP is a proposition depending on the natural numbers means that it is a dependent type

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

The categorical interpretation of this is by a display map

(6)P π P \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 PP holds at 0 means that there is a (proof-)term

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

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

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

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

* p 0 0 *P P * 0 . \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

* p 0 P * 0 . \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 nn \in \mathbb{N} there is an implication succ P(n):P(n)P(n+1)succ_P(n) \,\colon\, P(n) \to P(n+1)

nsucc P(n):P(n)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+1n+1 for nn is given by the pullback

P(*()) s *P P s \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)succ_P(n) is as a morphism Ps *PP \to s^* P in 𝒞 /\mathcal{C}_{/\mathbb{N}}

P p s s *P P s . \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

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

In summary this shows that

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

is interpreted precisely as an endofunctor-algebra homomorphism

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

for the endofunctor FF (1).

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

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

The categorical interpretation of this is as a morphism p:Pp \,\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 FF-algebra \mathbb{N} gives.

References

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

The syntax in Coq:

See also:

Discussion in a context of homotopy type theory and in view of higher inductive types:

Equivalence to binary presentations:

  • Nicolas Magaud?, Yves Bertot?, Changing Data Structures in Type Theory: A Study of Natural Numbers, in Types for Proofs and Programs. TYPES 2000, Lecture Notes in Computer Science 2277 [doi:10.1007/3-540-45842-5_12, pdf]

  • Nicolas Magaud?, Changing Data Representation within the Coq, in Theorem Proving in Higher Order Logics. TPHOLs 2003, Lecture Notes in Computer Science 2758 [doi:10.1007/10930755_6]

That one can construct the natural numbers type from the integers type can be found in:

Last revised on February 4, 2024 at 22:08:41. See the history of this page for a list of all contributions to it.