The type of natural numbers

module elementary-number-theory.natural-numbers where
Imports 
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.equivalences
open import foundation.functions
open import foundation.homotopies
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.propositions
open import foundation.sets
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.coproduct-types

Idea

The type of natural numbers is inductively generated 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 ℕ #-}

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-ℕ p0 pS 0 = p0
ind-ℕ p0 pS (succ-ℕ n) = pS n (ind-ℕ p0 pS n)

Peano's 7th axiom

is-injective-succ-ℕ : is-injective succ-ℕ
is-injective-succ-ℕ refl = refl

private
  Peano-7 :
    (x y : ℕ) → (x ＝ y) ↔ (succ-ℕ x ＝ succ-ℕ y)
  pr1 (Peano-7 x y) refl = refl
  pr2 (Peano-7 x y) = is-injective-succ-ℕ

Peano's 8th axiom

private
  Peano-8 : (x : ℕ) → is-nonzero-ℕ (succ-ℕ x)
  Peano-8 x ()

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-ℕ (pair 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 inequalities

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-nonzero-succ-ℕ 1

is-not-one-two-ℕ : is-not-one-ℕ 2
is-not-one-two-ℕ ()

The type of natural numbers is a set

Eq-ℕ : ℕ → ℕ → UU lzero
Eq-ℕ zero-ℕ zero-ℕ = unit
Eq-ℕ zero-ℕ (succ-ℕ n) = empty
Eq-ℕ (succ-ℕ m) zero-ℕ = empty
Eq-ℕ (succ-ℕ m) (succ-ℕ n) = Eq-ℕ m n

abstract
  is-prop-Eq-ℕ :
    (n m : ℕ) → is-prop (Eq-ℕ n m)
  is-prop-Eq-ℕ zero-ℕ zero-ℕ = is-prop-unit
  is-prop-Eq-ℕ zero-ℕ (succ-ℕ m) = is-prop-empty
  is-prop-Eq-ℕ (succ-ℕ n) zero-ℕ = is-prop-empty
  is-prop-Eq-ℕ (succ-ℕ n) (succ-ℕ m) = is-prop-Eq-ℕ n m

refl-Eq-ℕ : (n : ℕ) → Eq-ℕ n n
refl-Eq-ℕ zero-ℕ = star
refl-Eq-ℕ (succ-ℕ n) = refl-Eq-ℕ n

Eq-eq-ℕ : {x y : ℕ} → x ＝ y → Eq-ℕ x y
Eq-eq-ℕ {x} {.x} refl = refl-Eq-ℕ x

eq-Eq-ℕ : (x y : ℕ) → Eq-ℕ x y → x ＝ y
eq-Eq-ℕ zero-ℕ zero-ℕ e = refl
eq-Eq-ℕ (succ-ℕ x) (succ-ℕ y) e = ap succ-ℕ (eq-Eq-ℕ x y e)

abstract
  is-set-ℕ : is-set ℕ
  is-set-ℕ =
    is-set-prop-in-id
      Eq-ℕ
      is-prop-Eq-ℕ
      refl-Eq-ℕ
      eq-Eq-ℕ

ℕ-Set : Set lzero
pr1 ℕ-Set = ℕ
pr2 ℕ-Set = is-set-ℕ

is-prop-is-zero-ℕ : (n : ℕ) → is-prop (is-zero-ℕ n)
is-prop-is-zero-ℕ n = is-set-ℕ n zero-ℕ

is-zero-ℕ-Prop : ℕ → Prop lzero
pr1 (is-zero-ℕ-Prop n) = is-zero-ℕ n
pr2 (is-zero-ℕ-Prop n) = is-prop-is-zero-ℕ n

is-prop-is-one-ℕ : (n : ℕ) → is-prop (is-one-ℕ n)
is-prop-is-one-ℕ n = is-set-ℕ n 1

is-one-ℕ-Prop : ℕ → Prop lzero
pr1 (is-one-ℕ-Prop n) = is-one-ℕ n
pr2 (is-one-ℕ-Prop n) = is-prop-is-one-ℕ n

The natural numbers is a fixpoint to the functor X ↦ 1 + X

map-equiv-ℕ : ℕ → unit + ℕ
map-equiv-ℕ zero-ℕ = inl star
map-equiv-ℕ (succ-ℕ n) = inr n

map-inv-equiv-ℕ : unit + ℕ → ℕ
map-inv-equiv-ℕ (inl x) = zero-ℕ
map-inv-equiv-ℕ (inr n) = succ-ℕ n

isretr-map-inv-equiv-ℕ :
  ( map-inv-equiv-ℕ ∘ map-equiv-ℕ) ~ id
isretr-map-inv-equiv-ℕ zero-ℕ = refl
isretr-map-inv-equiv-ℕ (succ-ℕ n) = refl

issec-map-inv-equiv-ℕ :
  ( map-equiv-ℕ ∘ map-inv-equiv-ℕ) ~ id
issec-map-inv-equiv-ℕ (inl star) = refl
issec-map-inv-equiv-ℕ (inr n) = refl

equiv-ℕ : ℕ ≃ (unit + ℕ)
pr1 equiv-ℕ = map-equiv-ℕ
pr2 equiv-ℕ =
  is-equiv-has-inverse
    map-inv-equiv-ℕ
    issec-map-inv-equiv-ℕ
    isretr-map-inv-equiv-ℕ

See also