Initial segments of the natural numbers

module elementary-number-theory.initial-segments-natural-numbers where

Imports

open import elementary-number-theory.maximum-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.functions
open import foundation.identity-types
open import foundation.propositions
open import foundation.subtypes
open import foundation.universe-levels

Idea

An initial segment of the natural numbers is a subtype P : ℕ → Prop such that the implication

  P (n + 1) → P n

holds for every n : ℕ.

Definitions

Initial segments

is-initial-segment-subset-ℕ-Prop : {l : Level} (P : subtype l ℕ) → Prop l
is-initial-segment-subset-ℕ-Prop P =
  Π-Prop ℕ (λ n → implication-Prop (P (succ-ℕ n)) (P n))

is-initial-segment-subset-ℕ : {l : Level} (P : subtype l ℕ) → UU l
is-initial-segment-subset-ℕ P = type-Prop (is-initial-segment-subset-ℕ-Prop P)

initial-segment-ℕ : (l : Level) → UU (lsuc l)
initial-segment-ℕ l = type-subtype is-initial-segment-subset-ℕ-Prop

module _
  {l : Level} (I : initial-segment-ℕ l)
  where

  subset-initial-segment-ℕ : subtype l ℕ
  subset-initial-segment-ℕ = pr1 I

  is-initial-segment-initial-segment-ℕ :
    is-initial-segment-subset-ℕ subset-initial-segment-ℕ
  is-initial-segment-initial-segment-ℕ = pr2 I

  is-in-initial-segment-ℕ : ℕ → UU l
  is-in-initial-segment-ℕ = is-in-subtype subset-initial-segment-ℕ

  is-closed-under-eq-initial-segment-ℕ :
    {x y : ℕ} → is-in-initial-segment-ℕ x → x ＝ y → is-in-initial-segment-ℕ y
  is-closed-under-eq-initial-segment-ℕ =
    is-closed-under-eq-subtype subset-initial-segment-ℕ

  is-closed-under-eq-initial-segment-ℕ' :
    {x y : ℕ} → is-in-initial-segment-ℕ y → x ＝ y → is-in-initial-segment-ℕ x
  is-closed-under-eq-initial-segment-ℕ' =
    is-closed-under-eq-subtype' subset-initial-segment-ℕ

Shifting initial segments

shift-initial-segment-ℕ :
  {l : Level} → initial-segment-ℕ l → initial-segment-ℕ l
pr1 (shift-initial-segment-ℕ I) = subset-initial-segment-ℕ I ∘ succ-ℕ
pr2 (shift-initial-segment-ℕ I) =
  is-initial-segment-initial-segment-ℕ I ∘ succ-ℕ

Properties

Inhabited initial segments contain `0`

contains-zero-initial-segment-ℕ :
  {l : Level} (I : initial-segment-ℕ l) →
  (x : ℕ) → is-in-initial-segment-ℕ I x → is-in-initial-segment-ℕ I 0
contains-zero-initial-segment-ℕ I zero-ℕ H = H
contains-zero-initial-segment-ℕ I (succ-ℕ x) H =
  is-initial-segment-initial-segment-ℕ I 0
    ( contains-zero-initial-segment-ℕ (shift-initial-segment-ℕ I) x H)

Initial segments that contain a successor contain `1`

contains-one-initial-segment-ℕ :
  {l : Level} (I : initial-segment-ℕ l) →
  (x : ℕ) → is-in-initial-segment-ℕ I (succ-ℕ x) → is-in-initial-segment-ℕ I 1
contains-one-initial-segment-ℕ I =
  contains-zero-initial-segment-ℕ (shift-initial-segment-ℕ I)

Initial segments are closed under `max-ℕ`

max-initial-segment-ℕ :
  {l : Level} (I : initial-segment-ℕ l) →
  (x y : ℕ) → is-in-initial-segment-ℕ I x → is-in-initial-segment-ℕ I y →
  is-in-initial-segment-ℕ I (max-ℕ x y)
max-initial-segment-ℕ I zero-ℕ y H K = K
max-initial-segment-ℕ I (succ-ℕ x) zero-ℕ H K = H
max-initial-segment-ℕ I (succ-ℕ x) (succ-ℕ y) H K =
  max-initial-segment-ℕ (shift-initial-segment-ℕ I) x y H K