Similarity of positive real numbers

Content created by Louis Wasserman.

Created on 2025-11-09.
Last modified on 2025-12-03.

module real-numbers.similarity-positive-real-numbers where
Imports 
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.large-equivalence-relations
open import foundation.large-similarity-relations
open import foundation.propositions
open import foundation.universe-levels

open import real-numbers.positive-real-numbers
open import real-numbers.raising-universe-levels-real-numbers
open import real-numbers.similarity-real-numbers

Idea

Two positive real numbers are similar if they are similar as real numbers.

Definition

sim-prop-ℝ⁺ : {l1 l2 : Level} → ℝ⁺ l1 → ℝ⁺ l2 → Prop (l1 ⊔ l2)
sim-prop-ℝ⁺ (x , _) (y , _) = sim-prop-ℝ x y

sim-ℝ⁺ : {l1 l2 : Level} → ℝ⁺ l1 → ℝ⁺ l2 → UU (l1 ⊔ l2)
sim-ℝ⁺ (x , _) (y , _) = sim-ℝ x y

Properties

Similarity is a large equivalence relation

abstract
  refl-sim-ℝ⁺ : {l : Level} (x : ℝ⁺ l) → sim-ℝ⁺ x x
  refl-sim-ℝ⁺ (x , _) = refl-sim-ℝ x

  symmetric-sim-ℝ⁺ :
    {l1 l2 : Level} (x : ℝ⁺ l1) (y : ℝ⁺ l2) → sim-ℝ⁺ x y → sim-ℝ⁺ y x
  symmetric-sim-ℝ⁺ _ _ = symmetric-sim-ℝ

  transitive-sim-ℝ⁺ :
    {l1 l2 l3 : Level} (x : ℝ⁺ l1) (y : ℝ⁺ l2) (z : ℝ⁺ l3) →
    sim-ℝ⁺ y z → sim-ℝ⁺ x y → sim-ℝ⁺ x z
  transitive-sim-ℝ⁺ (x , _) (y , _) (z , _) = transitive-sim-ℝ x y z

large-equivalence-relation-sim-ℝ⁺ : Large-Equivalence-Relation (_⊔_) ℝ⁺
large-equivalence-relation-sim-ℝ⁺ =
  make-Large-Equivalence-Relation
    ( sim-prop-ℝ⁺)
    ( refl-sim-ℝ⁺)
    ( symmetric-sim-ℝ⁺)
    ( transitive-sim-ℝ⁺)

Similarity is a large similarity relation

abstract
  eq-sim-ℝ⁺ :
    {l : Level} (x y : ℝ⁺ l) → sim-ℝ⁺ x y → x ＝ y
  eq-sim-ℝ⁺ x y x~y = eq-ℝ⁺ x y (eq-sim-ℝ x~y)

large-similarity-relation-sim-ℝ⁺ : Large-Similarity-Relation (_⊔_) ℝ⁺
large-similarity-relation-sim-ℝ⁺ =
  make-Large-Similarity-Relation
    ( large-equivalence-relation-sim-ℝ⁺)
    ( eq-sim-ℝ⁺)

Positive real numbers are similar to their raised universe level counterparts

abstract
  sim-raise-ℝ⁺ : {l0 : Level} (l : Level) (x : ℝ⁺ l) → sim-ℝ⁺ x (raise-ℝ⁺ l x)
  sim-raise-ℝ⁺ l (x , _) = sim-raise-ℝ l x

Recent changes