Raising the universe levels of real numbers

Content created by Louis Wasserman and malarbol.

Created on 2025-03-03.
Last modified on 2026-01-14.

module real-numbers.raising-universe-levels-real-numbers where
Imports 
open import elementary-number-theory.rational-numbers
open import elementary-number-theory.strict-inequality-rational-numbers

open import foundation.cartesian-product-types
open import foundation.conjunction
open import foundation.dependent-pair-types
open import foundation.disjunction
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-disjunction
open import foundation.identity-types
open import foundation.inhabited-subtypes
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.raising-universe-levels
open import foundation.subtypes
open import foundation.universe-levels

open import logic.functoriality-existential-quantification

open import real-numbers.dedekind-real-numbers
open import real-numbers.lower-dedekind-real-numbers
open import real-numbers.similarity-real-numbers
open import real-numbers.upper-dedekind-real-numbers

Idea

For every universe 𝒰 there is a type of real numbers ℝ relative to 𝒰, ℝ 𝒰. Given a larger universe 𝒱, then we may raise a real number x from the universe 𝒰 to a similar real number in the universe 𝒱.

Definition

Raising lower Dedekind real numbers

module _
  {l0 : Level} (l : Level) (x : lower-ℝ l0)
  where

  cut-raise-lower-ℝ : subtype (l0 ⊔ l) ℚ
  cut-raise-lower-ℝ = raise-subtype l (cut-lower-ℝ x)

  abstract
    is-inhabited-cut-raise-lower-ℝ : is-inhabited-subtype cut-raise-lower-ℝ
    is-inhabited-cut-raise-lower-ℝ =
      map-tot-exists (λ _ → map-raise) (is-inhabited-cut-lower-ℝ x)

    is-rounded-cut-raise-lower-ℝ :
      (q : ℚ) →
      is-in-subtype cut-raise-lower-ℝ q ↔
      exists ℚ (λ r → le-ℚ-Prop q r ∧ cut-raise-lower-ℝ r)
    pr1 (is-rounded-cut-raise-lower-ℝ q) (map-raise q<x) =
      map-tot-exists
        ( λ _ → map-product id map-raise)
        ( forward-implication (is-rounded-cut-lower-ℝ x q) q<x)
    pr2 (is-rounded-cut-raise-lower-ℝ q) ∃r =
      map-raise
        ( backward-implication
          ( is-rounded-cut-lower-ℝ x q)
          ( map-tot-exists (λ _ → map-product id map-inv-raise) ∃r))

  raise-lower-ℝ : lower-ℝ (l0 ⊔ l)
  raise-lower-ℝ =
    cut-raise-lower-ℝ ,
    is-inhabited-cut-raise-lower-ℝ ,
    is-rounded-cut-raise-lower-ℝ

Raising upper Dedekind real numbers

module _
  {l0 : Level} (l : Level) (x : upper-ℝ l0)
  where

  cut-raise-upper-ℝ : subtype (l0 ⊔ l) ℚ
  cut-raise-upper-ℝ = raise-subtype l (cut-upper-ℝ x)

  abstract
    is-inhabited-cut-raise-upper-ℝ : is-inhabited-subtype cut-raise-upper-ℝ
    is-inhabited-cut-raise-upper-ℝ =
      map-tot-exists (λ _ → map-raise) (is-inhabited-cut-upper-ℝ x)

    is-rounded-cut-raise-upper-ℝ :
      (q : ℚ) →
      is-in-subtype cut-raise-upper-ℝ q ↔
      exists ℚ (λ p → le-ℚ-Prop p q ∧ cut-raise-upper-ℝ p)
    pr1 (is-rounded-cut-raise-upper-ℝ q) (map-raise x<q) =
      map-tot-exists
        ( λ _ → map-product id map-raise)
        ( forward-implication (is-rounded-cut-upper-ℝ x q) x<q)
    pr2 (is-rounded-cut-raise-upper-ℝ q) ∃p =
      map-raise
        ( backward-implication
          ( is-rounded-cut-upper-ℝ x q)
          ( map-tot-exists (λ _ → map-product id map-inv-raise) ∃p))

  raise-upper-ℝ : upper-ℝ (l0 ⊔ l)
  raise-upper-ℝ =
    cut-raise-upper-ℝ ,
    is-inhabited-cut-raise-upper-ℝ ,
    is-rounded-cut-raise-upper-ℝ

Raising Dedekind real numbers

module _
  {l0 : Level} (l : Level) (x : ℝ l0)
  where

  lower-real-raise-ℝ : lower-ℝ (l0 ⊔ l)
  lower-real-raise-ℝ = raise-lower-ℝ l (lower-real-ℝ x)

  upper-real-raise-ℝ : upper-ℝ (l0 ⊔ l)
  upper-real-raise-ℝ = raise-upper-ℝ l (upper-real-ℝ x)

  abstract
    is-disjoint-cut-raise-ℝ :
      (q : ℚ) →
      ¬
        ( is-in-cut-lower-ℝ lower-real-raise-ℝ q ×
          is-in-cut-upper-ℝ upper-real-raise-ℝ q)
    is-disjoint-cut-raise-ℝ q (map-raise q<x , map-raise x<q) =
      is-disjoint-cut-ℝ x q (q<x , x<q)

    is-located-lower-upper-cut-raise-ℝ :
      (p q : ℚ) → le-ℚ p q →
      type-disjunction-Prop
        ( cut-lower-ℝ lower-real-raise-ℝ p)
        ( cut-upper-ℝ upper-real-raise-ℝ q)
    is-located-lower-upper-cut-raise-ℝ p q p<q =
      map-disjunction
        ( map-raise)
        ( map-raise)
        ( is-located-lower-upper-cut-ℝ x p<q)

  raise-ℝ : ℝ (l0 ⊔ l)
  raise-ℝ =
    real-lower-upper-ℝ
      ( lower-real-raise-ℝ)
      ( upper-real-raise-ℝ)
      ( is-disjoint-cut-raise-ℝ)
      ( is-located-lower-upper-cut-raise-ℝ)

Properties

Reals are similar to their raised-universe equivalents

abstract opaque
  unfolding sim-ℝ

  sim-raise-ℝ : {l0 : Level} (l : Level) (x : ℝ l0) → sim-ℝ x (raise-ℝ l x)
  pr1 (sim-raise-ℝ l x) _ = map-raise
  pr2 (sim-raise-ℝ l x) _ = map-inv-raise

abstract
  sim-raise-ℝ' : {l0 : Level} (l : Level) (x : ℝ l0) → sim-ℝ (raise-ℝ l x) x
  sim-raise-ℝ' l x = symmetric-sim-ℝ (sim-raise-ℝ l x)

  sim-raise-raise-ℝ :
    {l0 : Level} (l1 l2 : Level) (x : ℝ l0) →
    sim-ℝ (raise-ℝ l1 x) (raise-ℝ l2 x)
  sim-raise-raise-ℝ l1 l2 x =
    transitive-sim-ℝ _ _ _ (sim-raise-ℝ l2 x) (sim-raise-ℝ' l1 x)

Raising a real to its own level is the identity

eq-raise-ℝ : {l : Level} → (x : ℝ l) → x ＝ raise-ℝ l x
eq-raise-ℝ {l} x = eq-sim-ℝ (sim-raise-ℝ l x)

x and y are similar if and only if x raised to y’s universe level equals y raised to x’s universe level

module _
  {l1 l2 : Level}
  {x : ℝ l1}
  {y : ℝ l2}
  where

  abstract
    eq-raise-sim-ℝ : sim-ℝ x y → raise-ℝ l2 x ＝ raise-ℝ l1 y
    eq-raise-sim-ℝ x~y =
      eq-sim-ℝ
        ( similarity-reasoning-ℝ
          raise-ℝ l2 x
          ~ℝ x
            by sim-raise-ℝ' l2 x
          ~ℝ y
            by x~y
          ~ℝ raise-ℝ l1 y
            by sim-raise-ℝ l1 y)

    sim-eq-raise-ℝ : raise-ℝ l2 x ＝ raise-ℝ l1 y → sim-ℝ x y
    sim-eq-raise-ℝ l2x=l1y =
      similarity-reasoning-ℝ
        x
        ~ℝ raise-ℝ l2 x
          by sim-raise-ℝ l2 x
        ~ℝ raise-ℝ l1 y
          by sim-eq-ℝ l2x=l1y
        ~ℝ y
          by sim-raise-ℝ' l1 y

Raising a real by two universe levels is equivalent to raising by the least upper bound of the universe levels

abstract
  raise-raise-ℝ :
    {l1 l2 l3 : Level} (x : ℝ l1) →
    raise-ℝ l2 (raise-ℝ l3 x) ＝ raise-ℝ (l2 ⊔ l3) x
  raise-raise-ℝ {l1} {l2} {l3} x =
    eq-sim-ℝ
      ( similarity-reasoning-ℝ
        raise-ℝ l2 (raise-ℝ l3 x)
        ~ℝ raise-ℝ l3 x
          by sim-raise-ℝ' l2 _
        ~ℝ raise-ℝ (l2 ⊔ l3) x
          by sim-raise-raise-ℝ l3 (l2 ⊔ l3) x)

Recent changes