Strictly ordered pairs of natural numbers

module elementary-number-theory.strictly-ordered-pairs-of-natural-numbers where
Imports 
open import elementary-number-theory.natural-numbers
open import elementary-number-theory.strict-inequality-natural-numbers

open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.functions
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.negation
open import foundation.pairs-of-distinct-elements
open import foundation.unit-type
open import foundation.universe-levels

Idea

A strictly ordered pair of natural numbers consists of x y : ℕ such that x < y.

Definition

strictly-ordered-pair-ℕ : UU lzero
strictly-ordered-pair-ℕ = Σ ℕ (λ x → Σ ℕ (λ y → le-ℕ x y))

module _
  (p : strictly-ordered-pair-ℕ)
  where

  first-strictly-ordered-pair-ℕ : ℕ
  first-strictly-ordered-pair-ℕ = pr1 p

  second-strictly-ordered-pair-ℕ : ℕ
  second-strictly-ordered-pair-ℕ = pr1 (pr2 p)

  strict-inequality-strictly-ordered-pair-ℕ :
    le-ℕ first-strictly-ordered-pair-ℕ second-strictly-ordered-pair-ℕ
  strict-inequality-strictly-ordered-pair-ℕ = pr2 (pr2 p)

Properties

Strictly ordered pairs of natural numbers are pairs of distinct elements

pair-of-distinct-elements-strictly-ordered-pair-ℕ :
  strictly-ordered-pair-ℕ → pair-of-distinct-elements ℕ
pair-of-distinct-elements-strictly-ordered-pair-ℕ (a , b , H) =
  (a , b , neq-le-ℕ H)

Any pair of distinct elements of natural numbers can be strictly ordered

strictly-ordered-pair-pair-of-distinct-elements-ℕ' :
  (a b : ℕ) → ¬ (a ＝ b) → strictly-ordered-pair-ℕ
strictly-ordered-pair-pair-of-distinct-elements-ℕ' zero-ℕ zero-ℕ H =
  ex-falso (H refl)
strictly-ordered-pair-pair-of-distinct-elements-ℕ' zero-ℕ (succ-ℕ b) H =
  (0 , succ-ℕ b , star)
strictly-ordered-pair-pair-of-distinct-elements-ℕ' (succ-ℕ a) zero-ℕ H =
  (0 , succ-ℕ a , star)
strictly-ordered-pair-pair-of-distinct-elements-ℕ' (succ-ℕ a) (succ-ℕ b) H =
  map-Σ
    ( λ x → Σ ℕ (λ y → le-ℕ x y))
    ( succ-ℕ)
    ( λ x →
      map-Σ (le-ℕ (succ-ℕ x)) succ-ℕ (λ y → id))
    ( strictly-ordered-pair-pair-of-distinct-elements-ℕ' a b
      ( λ p → H (ap succ-ℕ p)))

strictly-ordered-pair-pair-of-distinct-elements-ℕ :
  pair-of-distinct-elements ℕ → strictly-ordered-pair-ℕ
strictly-ordered-pair-pair-of-distinct-elements-ℕ (a , b , H) =
  strictly-ordered-pair-pair-of-distinct-elements-ℕ' a b H