Redirected from "dependent universal property of the natural numbers".
Contents
Context
Type theory
Deduction and Induction
Foundations
foundations
The basis of it all
mathematical logic
deduction system , natural deduction , sequent calculus , lambda-calculus , judgment
type theory , simple type theory , dependent type theory
collection , object , type , term , set , element
equality , judgmental equality , typal equality
universe , size issues
higher-order logic
Set theory
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 .
type formation rule :
| | ℕ : Type
\frac{}{
\mathclap{\phantom{\vert^{\vert}}}
\mathbb{N} \,\colon\, Type
}
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}
}
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)
}
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 ( s x ) ; ⊢ 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 F F 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 C C the function
λ c . ( c ( 0 ) , λ x . c ( s ( x ) ) ) : ( ℕ → C ) → ( C × ( ℕ → C → C ) ) \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 C C and a function f : C → ℕ f:C \to \mathbb{N} instead of a type family x : ℕ ⊢ P ( x ) x:\mathbb{N} \vdash P(x) , and one uses the fiber ∑ z : C f ( 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 C C and a function f : C → ℕ f:C \to \mathbb{N} along with
c 0 : ∑ z : C f ( z ) = ℕ 0 c_0:\sum_{z:C} f(z) =_\mathbb{N} 0
c s : ∏ n : ℕ ( ∑ z : C f ( z ) = ℕ n ) → ( ∑ z : C f ( 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 : C f ( 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 : C f ( z ) = ℕ 0 c_0:\sum_{z:C} f(z) =_\mathbb{N} 0 we have the element c 0 : C c_0:C and identificaiton p 0 : f ( c 0 ) = ℕ 0 p_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 : C f ( z ) = ℕ n ) → ( ∑ z : C f ( 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 : C f ( 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 ) = ℕ n f ( 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 ) → C c_s:\prod_{n:\mathbb{N}} \prod_{y:C} (f(y) =_\mathbb{N} n) \to C p s : ∏ n : ℕ ∏ y : C ∏ p : f ( y ) = ℕ n f ( 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 C C and a function f : C → ℕ f:C \to \mathbb{N} , along with
c s : ∏ n : ℕ ∏ y : C ( f ( y ) = ℕ n ) → C c_s:\prod_{n:\mathbb{N}} \prod_{y:C} (f(y) =_\mathbb{N} n) \to C p s : ∏ n : ℕ ∏ y : C ∏ p : f ( y ) = ℕ n f ( 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 f f , 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 :
Γ ⊢ C type Γ ⊢ 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 ) = ℕ n f ( 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}
Γ ⊢ C type Γ ⊢ 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 ) = ℕ n f ( 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 :
Γ ⊢ C type Γ ⊢ 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 ) = ℕ n f ( 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}
Γ ⊢ C type Γ ⊢ 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 ) = ℕ n f ( 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}
Γ ⊢ C type Γ ⊢ 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 ) = ℕ n f ( 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))}
Γ ⊢ C type Γ ⊢ 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 ) = ℕ n f ( 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 ≡ π 1 f \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 ≡ ℕ × X C \equiv \mathbb{N} \times X and f ≡ π 1 f \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
[
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 : FinType A:\mathrm{FinType} and B : FinType B:\mathrm{FinType} and finite families C : A → FinType C:A \to \mathrm{FinType} , we have
0 = ℕ [ ∅ ] 0 1 = ℕ [ 𝟙 ] 0 0 =_\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 : A C ( 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 : A C ( x ) ] 0 \prod_{x = 1}^{[A]_0} [C]_0(x) =_\mathbb{N} \left[\prod_{x:A} C(x)\right]_0 [ B ] 0 [ A ] 0 = ℕ [ A → B ] 0 [B]_0^{[A]_0} =_\mathbb{N} [A \to B]_0 [ A ] 0 = ℕ [ B ] 0 ≔ [ A ≃ B ] ( − 1 ) or [ A = FinType B ] ( − 1 ) [A]_0 =_\mathbb{N} [B]_0 \coloneqq [A \simeq B]_{(-1)} \; \mathrm{or} \; [A =_\mathrm{FinType} B]_{(-1)} [ A ] 0 ≤ [ B ] 0 ≔ [ A ↪ B ] ( − 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) F Alg ( 𝒞 ) → underlying 𝒞
F Alg(\mathcal{C}) \xrightarrow{underlying} \mathcal{C}
for the category of algebras over the endofunctor F 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 F -algebra ( D , ( 0 D , succ D ) ) ∈ F Alg ( 𝒞 ) \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 : D → D .
succ_D \colon D \to D
\,.
By initiality of the F F -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 rec rec is the function defined recursively by
rec ( 0 ) = 0 D
rec(0) \;=\; 0_D
and
More generally, consider an F F -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 F F -algebra structure may now depend on ℕ \mathbb{N} :
in that
succ D : ℕ × D → D
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 F Alg ( 𝒞 ) 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 F Alg ( 𝒞 ) / ( ℕ , ( 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 f f 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
Induction
Dropping the above constraint (4) on the dependent F 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 P depending on the natural numbers is true at n = 0 n = 0 and such that if it is true for some n n then it is true for n + 1 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 P 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 P P 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 n n 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 P 0_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 n ∈ ℕ n \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)
n ∈ ℕ ⊢ succ 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 + 1 n+1 for n n 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 P → s * P P \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
P P being a proposition depending on natural numbers which holds at 0 and which holds at n + 1 n+1 if it holds at n n
is interpreted precisely as an endofunctor-algebra homomorphism
P ↓ ℕ .
\array{
P
\\
\downarrow
\\
\mathbb{N}
}
\,.
for the endofunctor F F (1) .
The induction principle is supposed to deduce from this that P P holds for every n n , hence that there is a proof ind ( n ) : P ( n ) ind(n) \colon P(n) for all n n :
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 : ℕ → P 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 F -algebra ℕ \mathbb{N} gives.
References
Original articles with emphasis on the nature of ℕ \mathbb{N} as an inductive type :
Per Martin-Löf (notes by Giovanni Sambin ), pp. 38 of: Intuitionistic type theory , Lecture notes Padua 1984, Bibliopolis, Napoli (1984) [pdf , pdf ]
Thierry Coquand , Christine Paulin , p. 52-53 in: Inductively defined types , COLOG-88 Lecture Notes in Computer Science 417 , Springer (1990) 50-66 [doi:10.1007/3-540-52335-9_47 ]
Christine Paulin-Mohring , §1.3 in: Inductive definitions in the system Coq – Rules and Properties , in: Typed Lambda Calculi and Applications TLCA 1993, Lecture Notes in Computer Science 664 Springer (1993) [doi:10.1007/BFb0037116 ]
Peter Dybjer , §3 in: Inductive families , Formal Aspects of Computing 6 (1994) 440–465 [ [ doi:10.1007/BF01211308 , doi:10.1007/BF01211308 , pdf ] ]
The syntax in Coq :
See also:
Discussion in a context of homotopy type theory and in view of higher inductive types :
Univalent Foundations Project , §1.9 in: Homotopy Type Theory – Univalent Foundations of Mathematics (2013) [web , pdf ]
Egbert Rijke , §3 in: Introduction to Homotopy Type Theory , Cambridge Studies in Advanced Mathematics, Cambridge University Press (arXiv:2212.11082 )
Kajetan Söhnen, §2.4.5 in: Higher Inductive Types in Homotopy Type Theory , Munich (2018) [pdf , pdf ]
Peter LeFanu Lumsdaine , Mike Shulman , Semantics of higher inductive types , Math. Proc. Camb. Phil. Soc. 169 (2020) 159-208 [arXiv:1705.07088 , talk slides pdf , doi:10.1017/S030500411900015X ]
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: