The type of natural numbers
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Elisabeth Stenholm and Elif Uskuplu.
Created on 2022-01-26.
Last modified on 2024-04-17.
module elementary-number-theory.natural-numbers where
Imports
open import foundation.dependent-pair-types open import foundation.universe-levels open import foundation-core.empty-types open import foundation-core.function-types open import foundation-core.identity-types open import foundation-core.injective-maps open import foundation-core.negation
Idea
The natural numbers is an inductively generated type by the zero element and the successor function. The induction principle for the natural numbers works to construct sections of type families over the natural numbers.
Definitions
The inductive definition of the type of natural numbers
data ℕ : UU lzero where zero-ℕ : ℕ succ-ℕ : ℕ → ℕ {-# BUILTIN NATURAL ℕ #-} second-succ-ℕ : ℕ → ℕ second-succ-ℕ = succ-ℕ ∘ succ-ℕ third-succ-ℕ : ℕ → ℕ third-succ-ℕ = succ-ℕ ∘ second-succ-ℕ fourth-succ-ℕ : ℕ → ℕ fourth-succ-ℕ = succ-ℕ ∘ third-succ-ℕ
Useful predicates on the natural numbers
These predicates can of course be asserted directly without much trouble. However, using the defined predicates ensures uniformity, and helps naming definitions.
is-zero-ℕ : ℕ → UU lzero is-zero-ℕ n = (n = zero-ℕ) is-zero-ℕ' : ℕ → UU lzero is-zero-ℕ' n = (zero-ℕ = n) is-successor-ℕ : ℕ → UU lzero is-successor-ℕ n = Σ ℕ (λ y → n = succ-ℕ y) is-nonzero-ℕ : ℕ → UU lzero is-nonzero-ℕ n = ¬ (is-zero-ℕ n) is-one-ℕ : ℕ → UU lzero is-one-ℕ n = (n = 1) is-one-ℕ' : ℕ → UU lzero is-one-ℕ' n = (1 = n) is-not-one-ℕ : ℕ → UU lzero is-not-one-ℕ n = ¬ (is-one-ℕ n) is-not-one-ℕ' : ℕ → UU lzero is-not-one-ℕ' n = ¬ (is-one-ℕ' n)
Properties
The induction principle of ℕ
ind-ℕ : {l : Level} {P : ℕ → UU l} → P 0 → ((n : ℕ) → P n → P (succ-ℕ n)) → ((n : ℕ) → P n) ind-ℕ p-zero p-succ 0 = p-zero ind-ℕ p-zero p-succ (succ-ℕ n) = p-succ n (ind-ℕ p-zero p-succ n)
The recursion principle of ℕ
rec-ℕ : {l : Level} {A : UU l} → A → (ℕ → A → A) → (ℕ → A) rec-ℕ = ind-ℕ
The successor function on ℕ is injective
is-injective-succ-ℕ : is-injective succ-ℕ is-injective-succ-ℕ refl = refl
Successors are nonzero
is-nonzero-succ-ℕ : (x : ℕ) → is-nonzero-ℕ (succ-ℕ x) is-nonzero-succ-ℕ x () is-nonzero-is-successor-ℕ : {x : ℕ} → is-successor-ℕ x → is-nonzero-ℕ x is-nonzero-is-successor-ℕ (x , refl) () is-successor-is-nonzero-ℕ : {x : ℕ} → is-nonzero-ℕ x → is-successor-ℕ x is-successor-is-nonzero-ℕ {zero-ℕ} H = ex-falso (H refl) pr1 (is-successor-is-nonzero-ℕ {succ-ℕ x} H) = x pr2 (is-successor-is-nonzero-ℕ {succ-ℕ x} H) = refl has-no-fixed-points-succ-ℕ : (x : ℕ) → ¬ (succ-ℕ x = x) has-no-fixed-points-succ-ℕ x ()
Basic nonequalities
is-nonzero-one-ℕ : is-nonzero-ℕ 1 is-nonzero-one-ℕ () is-not-one-zero-ℕ : is-not-one-ℕ zero-ℕ is-not-one-zero-ℕ () is-nonzero-two-ℕ : is-nonzero-ℕ 2 is-nonzero-two-ℕ () is-not-one-two-ℕ : is-not-one-ℕ 2 is-not-one-two-ℕ ()
See also
- The based induction principle is defined in
based-induction-natural-numbers
. - The strong induction principle is defined in
strong-induction-natural-numbers
. - The based strong induction principle is defined in
based-strong-induction-natural-numbers
.
Recent changes
- 2024-04-17. Fredrik Bakke. Splitting idempotents (#1105).
- 2023-10-22. Fredrik Bakke and Egbert Rijke. Peano arithmetic (#876).
- 2023-10-09. Fredrik Bakke and Egbert Rijke. Negated equality (#822).
- 2023-09-28. Egbert Rijke and Fredrik Bakke. Cyclic types (#800).
- 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).