Inequality on the real numbers

Content created by Louis Wasserman, Fredrik Bakke and malarbol.

Created on 2025-02-05.
Last modified on 2025-09-06.

{-# OPTIONS --lossy-unification #-}

module real-numbers.inequality-real-numbers where
Imports 
open import elementary-number-theory.inequality-rational-numbers
open import elementary-number-theory.positive-rational-numbers
open import elementary-number-theory.rational-numbers
open import elementary-number-theory.strict-inequality-rational-numbers

open import foundation.action-on-identifications-functions
open import foundation.binary-transport
open import foundation.complements-subtypes
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.empty-types
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.functoriality-cartesian-product-types
open import foundation.identity-types
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import logic.functoriality-existential-quantification

open import order-theory.large-posets
open import order-theory.large-preorders
open import order-theory.posets
open import order-theory.preorders
open import order-theory.similarity-of-elements-large-posets

open import real-numbers.addition-real-numbers
open import real-numbers.dedekind-real-numbers
open import real-numbers.difference-real-numbers
open import real-numbers.inequality-lower-dedekind-real-numbers
open import real-numbers.inequality-upper-dedekind-real-numbers
open import real-numbers.lower-dedekind-real-numbers
open import real-numbers.negation-lower-upper-dedekind-real-numbers
open import real-numbers.negation-real-numbers
open import real-numbers.rational-real-numbers
open import real-numbers.similarity-real-numbers
open import real-numbers.upper-dedekind-real-numbers

Idea

The standard ordering on the real numbers is defined as the lower cut of one being a subset of the lower cut of the other. This is the definition used in [UF13], section 11.2.1.

Definition

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

  opaque
    leq-ℝ : UU (l1 ⊔ l2)
    leq-ℝ = leq-lower-ℝ (lower-real-ℝ x) (lower-real-ℝ y)

    is-prop-leq-ℝ : is-prop leq-ℝ
    is-prop-leq-ℝ = is-prop-leq-lower-ℝ (lower-real-ℝ x) (lower-real-ℝ y)

  leq-prop-ℝ : Prop (l1 ⊔ l2)
  leq-prop-ℝ = (leq-ℝ , is-prop-leq-ℝ)

infix 30 _≤-ℝ_
_≤-ℝ_ = leq-ℝ

Properties

Equivalence with inequality on upper cuts

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

  opaque
    leq-ℝ' : UU (l1 ⊔ l2)
    leq-ℝ' = leq-upper-ℝ (upper-real-ℝ x) (upper-real-ℝ y)

    is-prop-leq-ℝ' : is-prop leq-ℝ'
    is-prop-leq-ℝ' = is-prop-leq-upper-ℝ (upper-real-ℝ x) (upper-real-ℝ y)

  leq-prop-ℝ' : Prop (l1 ⊔ l2)
  leq-prop-ℝ' = (leq-ℝ' , is-prop-leq-ℝ')

  opaque
    unfolding leq-ℝ leq-ℝ'

    leq'-leq-ℝ : leq-ℝ x y → leq-ℝ'
    leq'-leq-ℝ lx⊆ly q y<q =
      elim-exists
        ( upper-cut-ℝ x q)
        ( λ p (p<q , p≮y) →
          subset-upper-cut-upper-complement-lower-cut-ℝ
            ( x)
            ( q)
            ( intro-exists
              ( p)
              ( p<q ,
                reverses-order-complement-subtype
                  ( lower-cut-ℝ x)
                  ( lower-cut-ℝ y)
                  ( lx⊆ly)
                  ( p)
                  ( p≮y))))
        ( subset-upper-complement-lower-cut-upper-cut-ℝ y q y<q)

    leq-leq'-ℝ : leq-ℝ' → leq-ℝ x y
    leq-leq'-ℝ uy⊆ux p p<x =
      elim-exists
        ( lower-cut-ℝ y p)
        ( λ q (p<q , x≮q) →
          subset-lower-cut-lower-complement-upper-cut-ℝ
            ( y)
            ( p)
            ( intro-exists
              ( q)
              ( p<q ,
                reverses-order-complement-subtype
                  ( upper-cut-ℝ y)
                  ( upper-cut-ℝ x)
                  ( uy⊆ux)
                  ( q)
                  ( x≮q))))
        ( subset-lower-complement-upper-cut-lower-cut-ℝ x p p<x)

    leq-iff-ℝ' : leq-ℝ x y ↔ leq-ℝ'
    leq-iff-ℝ' = (leq'-leq-ℝ , leq-leq'-ℝ)

Inequality on the real numbers is reflexive

opaque
  unfolding leq-ℝ

  refl-leq-ℝ : {l : Level} → (x : ℝ l) → leq-ℝ x x
  refl-leq-ℝ x = refl-leq-Large-Preorder lower-ℝ-Large-Preorder (lower-real-ℝ x)

  leq-eq-ℝ : {l : Level} → (x y : ℝ l) → x ＝ y → leq-ℝ x y
  leq-eq-ℝ x y x=y = tr (leq-ℝ x) x=y (refl-leq-ℝ x)

opaque
  unfolding leq-ℝ sim-ℝ

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

Inequality on the real numbers is antisymmetric

opaque
  unfolding leq-ℝ sim-ℝ

  sim-antisymmetric-leq-ℝ :
    {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2) → leq-ℝ x y → leq-ℝ y x → sim-ℝ x y
  sim-antisymmetric-leq-ℝ _ _ = pair

  antisymmetric-leq-ℝ :
    {l : Level} → (x y : ℝ l) → leq-ℝ x y → leq-ℝ y x → x ＝ y
  antisymmetric-leq-ℝ x y x≤y y≤x =
    eq-sim-ℝ (sim-antisymmetric-leq-ℝ x y x≤y y≤x)

Inequality on the real numbers is transitive

module _
  {l1 l2 l3 : Level}
  (x : ℝ l1)
  (y : ℝ l2)
  (z : ℝ l3)
  where

  opaque
    unfolding leq-ℝ

    transitive-leq-ℝ : leq-ℝ y z → leq-ℝ x y → leq-ℝ x z
    transitive-leq-ℝ =
      transitive-leq-subtype (lower-cut-ℝ x) (lower-cut-ℝ y) (lower-cut-ℝ z)

The large preorder of real numbers

ℝ-Large-Preorder : Large-Preorder lsuc _⊔_
type-Large-Preorder ℝ-Large-Preorder = ℝ
leq-prop-Large-Preorder ℝ-Large-Preorder = leq-prop-ℝ
refl-leq-Large-Preorder ℝ-Large-Preorder = refl-leq-ℝ
transitive-leq-Large-Preorder ℝ-Large-Preorder = transitive-leq-ℝ

The large poset of real numbers

ℝ-Large-Poset : Large-Poset lsuc _⊔_
large-preorder-Large-Poset ℝ-Large-Poset = ℝ-Large-Preorder
antisymmetric-leq-Large-Poset ℝ-Large-Poset = antisymmetric-leq-ℝ

Similarity in the large poset of real numbers is equivalent to similarity

opaque
  unfolding leq-ℝ sim-ℝ

  sim-sim-leq-ℝ :
    {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} →
    sim-Large-Poset ℝ-Large-Poset x y → sim-ℝ x y
  sim-sim-leq-ℝ = id

  sim-leq-sim-ℝ :
    {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} →
    sim-ℝ x y → sim-Large-Poset ℝ-Large-Poset x y
  sim-leq-sim-ℝ = id

  sim-iff-sim-leq-ℝ :
    {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} →
    sim-ℝ x y ↔ sim-Large-Poset ℝ-Large-Poset x y
  sim-iff-sim-leq-ℝ = id-iff

The partially ordered set of reals at a specific level

ℝ-Preorder : (l : Level) → Preorder (lsuc l) l
ℝ-Preorder = preorder-Large-Preorder ℝ-Large-Preorder

ℝ-Poset : (l : Level) → Poset (lsuc l) l
ℝ-Poset = poset-Large-Poset ℝ-Large-Poset

The canonical map from rational numbers to the reals preserves and reflects inequality

opaque
  unfolding leq-ℝ real-ℚ

  preserves-leq-real-ℚ : (x y : ℚ) → leq-ℚ x y → leq-ℝ (real-ℚ x) (real-ℚ y)
  preserves-leq-real-ℚ = preserves-leq-lower-real-ℚ

  reflects-leq-real-ℚ : (x y : ℚ) → leq-ℝ (real-ℚ x) (real-ℚ y) → leq-ℚ x y
  reflects-leq-real-ℚ = reflects-leq-lower-real-ℚ

  iff-leq-real-ℚ : (x y : ℚ) → leq-ℚ x y ↔ leq-ℝ (real-ℚ x) (real-ℚ y)
  iff-leq-real-ℚ = iff-leq-lower-real-ℚ

Negation reverses inequality on the real numbers

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

  opaque
    unfolding leq-ℝ leq-ℝ' neg-ℝ

    neg-leq-ℝ : leq-ℝ x y → leq-ℝ (neg-ℝ y) (neg-ℝ x)
    neg-leq-ℝ x≤y = leq-leq'-ℝ (neg-ℝ y) (neg-ℝ x) (x≤y ∘ neg-ℚ)

Inequality on the real numbers is invariant under similarity

module _
  {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) (x~y : sim-ℝ x y)
  where

  opaque
    unfolding leq-ℝ sim-ℝ

    preserves-leq-left-sim-ℝ : leq-ℝ x z → leq-ℝ y z
    preserves-leq-left-sim-ℝ x≤z q q<y = x≤z q (pr2 x~y q q<y)

    preserves-leq-right-sim-ℝ : leq-ℝ z x → leq-ℝ z y
    preserves-leq-right-sim-ℝ z≤x q q<z = pr1 x~y q (z≤x q q<z)

module _
  {l1 l2 l3 l4 : Level}
  (x1 : ℝ l1) (x2 : ℝ l2) (y1 : ℝ l3) (y2 : ℝ l4)
  (x1~x2 : sim-ℝ x1 x2) (y1~y2 : sim-ℝ y1 y2)
  where

  preserves-leq-sim-ℝ : leq-ℝ x1 y1 → leq-ℝ x2 y2
  preserves-leq-sim-ℝ x1≤y1 =
    preserves-leq-left-sim-ℝ
      ( y2)
      ( x1)
      ( x2)
      ( x1~x2)
      ( preserves-leq-right-sim-ℝ x1 y1 y2 y1~y2 x1≤y1)

Inequality on the real numbers is translation invariant

module _
  {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3)
  where

  opaque
    unfolding add-ℝ leq-ℝ

    preserves-leq-right-add-ℝ : leq-ℝ x y → leq-ℝ (x +ℝ z) (y +ℝ z)
    preserves-leq-right-add-ℝ x≤y _ =
      map-tot-exists (λ (qx , _) → map-product (x≤y qx) id)

    preserves-leq-left-add-ℝ : leq-ℝ x y → leq-ℝ (z +ℝ x) (z +ℝ y)
    preserves-leq-left-add-ℝ x≤y _ =
      map-tot-exists (λ (_ , qx) → map-product id (map-product (x≤y qx) id))

abstract
  preserves-leq-diff-ℝ :
    {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3) →
    leq-ℝ x y → leq-ℝ (x -ℝ z) (y -ℝ z)
  preserves-leq-diff-ℝ z = preserves-leq-right-add-ℝ (neg-ℝ z)

module _
  {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3)
  where

  abstract
    reflects-leq-right-add-ℝ : leq-ℝ (x +ℝ z) (y +ℝ z) → leq-ℝ x y
    reflects-leq-right-add-ℝ x+z≤y+z =
      preserves-leq-sim-ℝ
        ( (x +ℝ z) -ℝ z)
        ( x)
        ( (y +ℝ z) -ℝ z)
        ( y)
        ( cancel-right-add-diff-ℝ x z)
        ( cancel-right-add-diff-ℝ y z)
        ( preserves-leq-right-add-ℝ (neg-ℝ z) (x +ℝ z) (y +ℝ z) x+z≤y+z)

    reflects-leq-left-add-ℝ : leq-ℝ (z +ℝ x) (z +ℝ y) → leq-ℝ x y
    reflects-leq-left-add-ℝ z+x≤z+y =
      reflects-leq-right-add-ℝ
        ( binary-tr
          ( leq-ℝ)
          ( commutative-add-ℝ z x)
          ( commutative-add-ℝ z y)
          ( z+x≤z+y))

module _
  {l1 l2 l3 : Level} (z : ℝ l1) (x : ℝ l2) (y : ℝ l3)
  where

  iff-translate-right-leq-ℝ : leq-ℝ x y ↔ leq-ℝ (x +ℝ z) (y +ℝ z)
  pr1 iff-translate-right-leq-ℝ = preserves-leq-right-add-ℝ z x y
  pr2 iff-translate-right-leq-ℝ = reflects-leq-right-add-ℝ z x y

  iff-translate-left-leq-ℝ : leq-ℝ x y ↔ leq-ℝ (z +ℝ x) (z +ℝ y)
  pr1 iff-translate-left-leq-ℝ = preserves-leq-left-add-ℝ z x y
  pr2 iff-translate-left-leq-ℝ = reflects-leq-left-add-ℝ z x y

abstract
  preserves-leq-add-ℝ :
    {l1 l2 l3 l4 : Level} (a : ℝ l1) (b : ℝ l2) (c : ℝ l3) (d : ℝ l4) →
    leq-ℝ a b → leq-ℝ c d → leq-ℝ (a +ℝ c) (b +ℝ d)
  preserves-leq-add-ℝ a b c d a≤b c≤d =
    transitive-leq-ℝ
      ( a +ℝ c)
      ( a +ℝ d)
      ( b +ℝ d)
      ( preserves-leq-right-add-ℝ d a b a≤b)
      ( preserves-leq-left-add-ℝ a c d c≤d)

Transposition laws

module _
  {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3)
  where

  abstract
    leq-transpose-left-diff-ℝ : leq-ℝ (x -ℝ y) z → leq-ℝ x (z +ℝ y)
    leq-transpose-left-diff-ℝ x-y≤z =
      preserves-leq-left-sim-ℝ
        ( z +ℝ y)
        ( (x -ℝ y) +ℝ y)
        ( x)
        ( cancel-right-diff-add-ℝ x y)
        ( preserves-leq-right-add-ℝ y (x -ℝ y) z x-y≤z)

    leq-transpose-left-add-ℝ : leq-ℝ (x +ℝ y) z → leq-ℝ x (z -ℝ y)
    leq-transpose-left-add-ℝ x+y≤z =
      preserves-leq-left-sim-ℝ
        (z -ℝ y)
        ( (x +ℝ y) -ℝ y)
        ( x)
        ( cancel-right-add-diff-ℝ x y)
        ( preserves-leq-right-add-ℝ (neg-ℝ y) (x +ℝ y) z x+y≤z)

    leq-transpose-right-add-ℝ : leq-ℝ x (y +ℝ z) → leq-ℝ (x -ℝ z) y
    leq-transpose-right-add-ℝ x≤y+z =
      preserves-leq-right-sim-ℝ
        ( x -ℝ z)
        ( (y +ℝ z) -ℝ z)
        ( y)
        ( cancel-right-add-diff-ℝ y z)
        ( preserves-leq-right-add-ℝ (neg-ℝ z) x (y +ℝ z) x≤y+z)

    leq-transpose-right-diff-ℝ : leq-ℝ x (y -ℝ z) → leq-ℝ (x +ℝ z) y
    leq-transpose-right-diff-ℝ x≤y-z =
      preserves-leq-right-sim-ℝ
        ( x +ℝ z)
        ( (y -ℝ z) +ℝ z)
        ( y)
        ( cancel-right-diff-add-ℝ y z)
        ( preserves-leq-right-add-ℝ z x (y -ℝ z) x≤y-z)

Swapping laws

abstract
  swap-right-diff-leq-ℝ :
    {l1 l2 l3 : Level} (x : ℝ l1) (y : ℝ l2) (z : ℝ l3) →
    leq-ℝ (x -ℝ y) z → leq-ℝ (x -ℝ z) y
  swap-right-diff-leq-ℝ x y z x-y≤z =
    leq-transpose-right-add-ℝ
      ( x)
      ( y)
      ( z)
      ( tr
        ( leq-ℝ x)
        ( commutative-add-ℝ _ _)
        ( leq-transpose-left-diff-ℝ x y z x-y≤z))

Addition of real numbers preserves lower neighborhoods

module _
  {l1 l2 l3 : Level} (d : ℚ⁺)
  (x : ℝ l1) (y : ℝ l2) (z : ℝ l3)
  where

  abstract
    preserves-lower-neighborhood-leq-left-add-ℝ :
      leq-ℝ y (z +ℝ real-ℚ⁺ d) →
      leq-ℝ
        ( add-ℝ x y)
        ( (add-ℝ x z) +ℝ real-ℚ⁺ d)
    preserves-lower-neighborhood-leq-left-add-ℝ z≤y+d =
      inv-tr
        ( leq-ℝ (x +ℝ y))
        ( associative-add-ℝ x z (real-ℚ⁺ d))
        ( preserves-leq-left-add-ℝ
          ( x)
          ( y)
          ( z +ℝ real-ℚ⁺ d)
          ( z≤y+d))

    preserves-lower-neighborhood-leq-right-add-ℝ :
      leq-ℝ y (z +ℝ real-ℚ⁺ d) →
      leq-ℝ
        ( add-ℝ y x)
        ( (add-ℝ z x) +ℝ real-ℚ⁺ d)
    preserves-lower-neighborhood-leq-right-add-ℝ z≤y+d =
      binary-tr
        ( λ u v → leq-ℝ u (v +ℝ real-ℚ⁺ d))
        ( commutative-add-ℝ x y)
        ( commutative-add-ℝ x z)
        ( preserves-lower-neighborhood-leq-left-add-ℝ z≤y+d)

Addition of real numbers reflects lower neighborhoods

module _
  {l1 l2 l3 : Level} (d : ℚ⁺)
  (x : ℝ l1) (y : ℝ l2) (z : ℝ l3)
  where

  abstract
    reflects-lower-neighborhood-leq-left-add-ℝ :
      leq-ℝ
        ( add-ℝ x y)
        ( (add-ℝ x z) +ℝ real-ℚ⁺ d) →
      leq-ℝ y (z +ℝ real-ℚ⁺ d)
    reflects-lower-neighborhood-leq-left-add-ℝ x+y≤x+z+d =
      reflects-leq-left-add-ℝ
        ( x)
        ( y)
        ( z +ℝ real-ℚ⁺ d)
        ( tr
          ( leq-ℝ (x +ℝ y))
          ( associative-add-ℝ x z (real-ℚ⁺ d))
          ( x+y≤x+z+d))

    reflects-lower-neighborhood-leq-right-add-ℝ :
      leq-ℝ
        ( add-ℝ y x)
        ( (add-ℝ z x) +ℝ real-ℚ⁺ d) →
      leq-ℝ y (z +ℝ real-ℚ⁺ d)
    reflects-lower-neighborhood-leq-right-add-ℝ y+x≤z+y+d =
      reflects-lower-neighborhood-leq-left-add-ℝ
        ( binary-tr
          ( λ u v → leq-ℝ u (v +ℝ real-ℚ⁺ d))
          ( commutative-add-ℝ y x)
          ( commutative-add-ℝ z x)
          ( y+x≤z+y+d))

Negation of real numbers reverses lower neighborhoods

module _
  {l1 l2 : Level} (d : ℚ⁺)
  (x : ℝ l1) (y : ℝ l2)
  where

  reverses-lower-neighborhood-neg-ℝ :
    leq-ℝ x (y +ℝ real-ℚ⁺ d) →
    leq-ℝ (neg-ℝ y) (neg-ℝ x +ℝ real-ℚ⁺ d)
  reverses-lower-neighborhood-neg-ℝ x≤y+d =
    tr
      ( leq-ℝ (neg-ℝ y))
      ( ( distributive-neg-add-ℝ x ((neg-ℝ ∘ real-ℚ ∘ rational-ℚ⁺) d)) ∙
        ( ap (add-ℝ (neg-ℝ x)) (neg-neg-ℝ (real-ℚ⁺ d))))
      ( neg-leq-ℝ
        ( x -ℝ real-ℚ⁺ d)
        ( y)
        ( leq-transpose-right-add-ℝ
          ( x)
          ( y)
          ( real-ℚ⁺ d)
          ( x≤y+d)))

x ≤ q for a rational q if and only if q ∉ lower-cut-ℝ x

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

  opaque
    unfolding leq-ℝ leq-ℝ' real-ℚ

    not-in-lower-cut-leq-ℝ : leq-ℝ x (real-ℚ q) → ¬ (is-in-lower-cut-ℝ x q)
    not-in-lower-cut-leq-ℝ x≤q q<x =
      let open do-syntax-trunc-Prop empty-Prop
      in do
        (r , q<r , r<x) ← forward-implication (is-rounded-lower-cut-ℝ x q) q<x
        is-disjoint-cut-ℝ x r (r<x , leq'-leq-ℝ x (real-ℚ q) x≤q r q<r)

    leq-not-in-lower-cut-ℝ : ¬ (is-in-lower-cut-ℝ x q) → leq-ℝ x (real-ℚ q)
    leq-not-in-lower-cut-ℝ q≮x r r<x =
      trichotomy-le-ℚ q r
        ( λ q<r →
          ex-falso
            ( q≮x
              ( backward-implication
                ( is-rounded-lower-cut-ℝ x q)
                ( intro-exists r (q<r , r<x)))))
        ( λ q=r → ex-falso (q≮x (inv-tr (is-in-lower-cut-ℝ x) q=r r<x)))
        ( λ r<q → r<q)

  leq-iff-not-in-lower-cut-ℝ : leq-ℝ x (real-ℚ q) ↔ ¬ (is-in-lower-cut-ℝ x q)
  leq-iff-not-in-lower-cut-ℝ = (not-in-lower-cut-leq-ℝ , leq-not-in-lower-cut-ℝ)

If y ≤ q ⇒ x ≤ q for every rational q, then x ≤ y

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

  opaque
    unfolding leq-ℝ'

    leq-leq-rational-ℝ :
      ((q : ℚ) → leq-ℝ y (real-ℚ q) → leq-ℝ x (real-ℚ q)) → x ≤-ℝ y
    leq-leq-rational-ℝ H =
      leq-leq'-ℝ x y
        ( λ q y<q →
          let open do-syntax-trunc-Prop (upper-cut-ℝ x q)
          in do
            (p , p<q , p≮y) ←
              subset-upper-complement-lower-cut-upper-cut-ℝ y q y<q
            subset-upper-cut-upper-complement-lower-cut-ℝ x q
              ( intro-exists
                ( p)
                ( p<q ,
                  not-in-lower-cut-leq-ℝ x p
                    ( H p (leq-not-in-lower-cut-ℝ y p p≮y)))))

If x and y are less than or equal to the same rational numbers, they are similar

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

  abstract
    sim-leq-same-rational-ℝ :
      ((q : ℚ) → leq-ℝ x (real-ℚ q) ↔ leq-ℝ y (real-ℚ q)) →
      sim-ℝ x y
    sim-leq-same-rational-ℝ H =
      sim-sim-leq-ℝ
        ( leq-leq-rational-ℝ x y (λ q → backward-implication (H q)) ,
          leq-leq-rational-ℝ y x (λ q → forward-implication (H q)))

References

[UF13]
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: https://homotopytypetheory.org/book/, arXiv:1308.0729.

Recent changes