This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The type of natural numbers

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