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