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
- 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
.