Andrew Sneap, March 2021
Updated March 2022

In this file I define the Dedekind reals, and prove that the rationals
are embedded in the reals.

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan renaming (_+_ to _โˆ”_)

open import Integers.Type
open import Notation.CanonicalMap
open import Notation.Order
open import Rationals.Order
open import Rationals.Type
open import UF.Base
open import UF.FunExt
open import UF.Powerset
open import UF.PropTrunc
open import UF.Sets
open import UF.Sets-Properties
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties

module DedekindReals.Type
         (fe : Fun-Ext)
         (pe : Prop-Ext)
         (pt : propositional-truncations-exist)
       where

open PropositionalTruncation pt

inhabited-left : (L : ๐“Ÿ โ„š) โ†’ ๐“คโ‚€ ฬ‡
inhabited-left L = (โˆƒ p ๊ž‰ โ„š , p โˆˆ L)

inhabited-right : (R : ๐“Ÿ โ„š) โ†’ ๐“คโ‚€ ฬ‡
inhabited-right R = (โˆƒ q ๊ž‰ โ„š , q โˆˆ R)

rounded-left : (L : ๐“Ÿ โ„š) โ†’ ๐“คโ‚€ ฬ‡
rounded-left L = (x : โ„š) โ†’ (x โˆˆ L โ†” (โˆƒ p ๊ž‰ โ„š , (x < p) ร— p โˆˆ L))

rounded-right : (R : ๐“Ÿ โ„š) โ†’ ๐“คโ‚€ ฬ‡
rounded-right R = (x : โ„š) โ†’ x โˆˆ R โ†” (โˆƒ q ๊ž‰ โ„š , (q < x) ร— q โˆˆ R)

disjoint : (L R : ๐“Ÿ โ„š) โ†’ ๐“คโ‚€ ฬ‡
disjoint L R = (p q : โ„š) โ†’ p โˆˆ L ร— q โˆˆ R โ†’ p < q

located : (L R : ๐“Ÿ โ„š) โ†’ ๐“คโ‚€ ฬ‡
located L R = (p q : โ„š) โ†’ p < q โ†’ p โˆˆ L โˆจ q โˆˆ R

isCut : (L R : ๐“Ÿ โ„š) โ†’ ๐“คโ‚€ ฬ‡
isCut L R = inhabited-left L
          ร— inhabited-right R
          ร— rounded-left L
          ร— rounded-right R
          ร— disjoint L R
          ร— located L R

โ„ : ๐“คโ‚ ฬ‡
โ„ = ฮฃ (L , R) ๊ž‰ ๐“Ÿ โ„š ร— ๐“Ÿ โ„š , isCut L R

subset-of-โ„š-is-set : is-set (๐“Ÿ โ„š)
subset-of-โ„š-is-set = powersets-are-sets fe pe

inhabited-left-is-prop : (L : ๐“Ÿ โ„š) โ†’ is-prop (inhabited-left L)
inhabited-left-is-prop L = โˆƒ-is-prop

inhabited-right-is-prop : (R : ๐“Ÿ โ„š) โ†’ is-prop (inhabited-right R)
inhabited-right-is-prop R = โˆƒ-is-prop

rounded-left-a : (L : ๐“Ÿ โ„š) โ†’ rounded-left L โ†’ (x y : โ„š) โ†’ x โ‰ค y โ†’ y โˆˆ L โ†’ x โˆˆ L
rounded-left-a L r x y l y-L = II (โ„šโ‰ค-split x y l)
 where
  I : (โˆƒ p ๊ž‰ โ„š , (x < p) ร— p โˆˆ L) โ†’ x โˆˆ L
  I = prโ‚‚ (r x)
  II : (x < y) โˆ” (x ๏ผ y) โ†’ x โˆˆ L
  II (inl l) = I โˆฃ y , (l , y-L) โˆฃ
  II (inr r) = transport (_โˆˆ L) (r โปยน) y-L

rounded-left-b : (L : ๐“Ÿ โ„š) โ†’ rounded-left L โ†’ (x : โ„š) โ†’ x โˆˆ L โ†’ (โˆƒ p ๊ž‰ โ„š , (x < p) ร— p โˆˆ L)
rounded-left-b L r x x-L = (prโ‚ (r x)) x-L

rounded-left-c : (L : ๐“Ÿ โ„š) โ†’ rounded-left L โ†’ (x y : โ„š) โ†’ x < y โ†’ y โˆˆ L โ†’ x โˆˆ L
rounded-left-c L r x y l yL = prโ‚‚ (r x) โˆฃ y , (l , yL) โˆฃ

rounded-right-a : (R : ๐“Ÿ โ„š) โ†’ rounded-right R โ†’ (x y : โ„š) โ†’ x โ‰ค y โ†’ x โˆˆ R โ†’ y โˆˆ R
rounded-right-a R r x y l x-R = II (โ„šโ‰ค-split x y l)
 where
  I : (โˆƒ p ๊ž‰ โ„š , (p < y) ร— p โˆˆ R) โ†’ y โˆˆ R
  I = prโ‚‚ (r y)
  II : (x < y) โˆ” (x ๏ผ y) โ†’ y โˆˆ R
  II (inl r) = I โˆฃ x , (r , x-R) โˆฃ
  II (inr r) = transport (_โˆˆ R) r x-R

rounded-right-b : (R : ๐“Ÿ โ„š) โ†’ rounded-right R โ†’ (x : โ„š) โ†’ x โˆˆ R โ†’ (โˆƒ q ๊ž‰ โ„š , (q < x) ร— q โˆˆ R)
rounded-right-b R r x x-R = (prโ‚ (r x)) x-R

rounded-right-c : (R : ๐“Ÿ โ„š) โ†’ rounded-right R โ†’ (x y : โ„š) โ†’ x < y โ†’ x โˆˆ R โ†’ y โˆˆ R
rounded-right-c R r x y l xR = prโ‚‚ (r y) โˆฃ x , (l , xR) โˆฃ

rounded-left-is-prop : (L : ๐“Ÿ โ„š) โ†’ is-prop (rounded-left L)
rounded-left-is-prop L = ฮ -is-prop fe ฮด
 where
  ฮด : (x : โ„š) โ†’ is-prop (x โˆˆ L โ†” (โˆƒ p ๊ž‰ โ„š , (x < p) ร— p โˆˆ L))
  ฮด x = ร—-is-prop (ฮ -is-prop fe (ฮป _ โ†’ โˆƒ-is-prop)) (ฮ -is-prop fe (ฮป _ โ†’ โˆˆ-is-prop L x))

rounded-right-is-prop : (R : ๐“Ÿ โ„š) โ†’ is-prop (rounded-right R)
rounded-right-is-prop R = ฮ -is-prop fe ฮด
 where
  ฮด : (x : โ„š) โ†’ is-prop (x โˆˆ R โ†” (โˆƒ q ๊ž‰ โ„š , (q < x) ร— q โˆˆ R))
  ฮด x = ร—-is-prop (ฮ -is-prop fe (ฮป _ โ†’ โˆƒ-is-prop)) (ฮ -is-prop fe (ฮป _ โ†’ โˆˆ-is-prop R x))

disjoint-is-prop : (L R : ๐“Ÿ โ„š) โ†’ is-prop (disjoint L R)
disjoint-is-prop L R = ฮ โ‚ƒ-is-prop fe (ฮป x y _ โ†’ โ„š<-is-prop x y)

located-is-prop : (L R : ๐“Ÿ โ„š) โ†’ is-prop (located L R)
located-is-prop L R = ฮ โ‚ƒ-is-prop fe (ฮป _ _ _ โ†’ โˆจ-is-prop)


isCut-is-prop : (L R : ๐“Ÿ โ„š) โ†’ is-prop (isCut L R)
isCut-is-prop L R = ร—-is-prop (inhabited-left-is-prop L)
                   (ร—-is-prop (inhabited-right-is-prop R)
                   (ร—-is-prop (rounded-left-is-prop L)
                   (ร—-is-prop (rounded-right-is-prop R)
                   (ร—-is-prop (disjoint-is-prop L R)
                              (located-is-prop L R)))))

โ„-is-set : is-set โ„
โ„-is-set = ฮฃ-is-set (ร—-is-set subset-of-โ„š-is-set subset-of-โ„š-is-set)
            ฮป (L , R) โ†’ props-are-sets (isCut-is-prop L R)

lower-cut-of : โ„ โ†’ ๐“Ÿ โ„š
lower-cut-of ((L , R) , _) = L

upper-cut-of : โ„ โ†’ ๐“Ÿ โ„š
upper-cut-of ((L , R) , _) = R

in-lower-cut : โ„š โ†’ โ„ โ†’ ๐“คโ‚€ ฬ‡
in-lower-cut q ((L , R) , _) = q โˆˆ L

in-upper-cut : โ„š โ†’ โ„ โ†’ ๐“คโ‚€ ฬ‡
in-upper-cut q ((L , R) , _) = q โˆˆ R

โ„-locatedness : (((L , R) , _) : โ„) โ†’ (p q : โ„š) โ†’ p < q โ†’ p โˆˆ L โˆจ q โˆˆ R
โ„-locatedness ((L , R) , _ , _ , _ , _ , _ , located-y) = located-y

inhabited-from-real-L : (((L , R) , i) : โ„) โ†’ inhabited-left L
inhabited-from-real-L ((L , R) , inhabited-L , _) = inhabited-L

inhabited-from-real-R : (((L , R) , i) : โ„) โ†’ inhabited-left R
inhabited-from-real-R ((L , R) , _ , inhabited-R , _) = inhabited-R

rounded-from-real-L : (((L , R) , i) : โ„) โ†’ rounded-left L
rounded-from-real-L ((L , R) , _ , _ , rounded-L , _) = rounded-L

rounded-from-real-R : (((L , R) , i) : โ„) โ†’ rounded-right R
rounded-from-real-R ((L , R) , _ , _ , _ , rounded-R , _) = rounded-R

disjoint-from-real : (((L , R) , i) : โ„) โ†’ disjoint L R
disjoint-from-real ((L , R) , _ , _ , _ , _ , disjoint , _) = disjoint

โ„š-rounded-leftโ‚ : (y : โ„š) (x : โ„š) โ†’ x < y โ†’ ฮฃ p ๊ž‰ โ„š , (x < p < y)
โ„š-rounded-leftโ‚ y x l = โ„š-dense x y l

โ„š-rounded-leftโ‚‚ : (y : โ„š) (x : โ„š) โ†’ ฮฃ p ๊ž‰ โ„š , (x < p < y) โ†’ x < y
โ„š-rounded-leftโ‚‚ y x (p , lโ‚ , lโ‚‚) = โ„š<-trans x p y lโ‚ lโ‚‚

โ„š-rounded-rightโ‚ : (y : โ„š) (x : โ„š) โ†’ y < x โ†’ ฮฃ q ๊ž‰ โ„š , (q < x) ร— (y < q)
โ„š-rounded-rightโ‚ y x l = I (โ„š-dense y x l)
 where
  I : ฮฃ q ๊ž‰ โ„š , (y < q) ร— (q < x)
    โ†’ ฮฃ q ๊ž‰ โ„š , (q < x) ร— (y < q)
  I (q , lโ‚ , lโ‚‚) = q , lโ‚‚ , lโ‚

โ„š-rounded-rightโ‚‚ : (y : โ„š) (x : โ„š) โ†’ ฮฃ q ๊ž‰ โ„š , (q < x) ร— (y < q) โ†’ y < x
โ„š-rounded-rightโ‚‚ y x (q , lโ‚ , lโ‚‚) = โ„š<-trans y q x lโ‚‚ lโ‚


_โ„š<โ„_  : โ„š โ†’ โ„ โ†’ ๐“คโ‚€ ฬ‡
p โ„š<โ„ x = p โˆˆ lower-cut-of x

_โ„<โ„š_  : โ„ โ†’ โ„š โ†’ ๐“คโ‚€ ฬ‡
x โ„<โ„š q = q โˆˆ upper-cut-of x

instance
 Strict-Order-โ„š-โ„ : Strict-Order โ„š โ„
 _<_ {{Strict-Order-โ„š-โ„}} = _โ„š<โ„_

 Strict-Order-โ„-โ„š : Strict-Order โ„ โ„š
 _<_ {{Strict-Order-โ„-โ„š}} = _โ„<โ„š_

 Strict-Order-Chain-โ„š-โ„-โ„š : Strict-Order-Chain โ„š โ„ โ„š _<_ _<_
 _<_<_ {{Strict-Order-Chain-โ„š-โ„-โ„š}} p q r = (p < q) ร— (q < r)

 Strict-Order-Chain-โ„š-โ„š-โ„ : Strict-Order-Chain โ„š โ„š โ„ _<_ _<_
 _<_<_ {{Strict-Order-Chain-โ„š-โ„š-โ„}} p q r = (p < q) ร— (q < r)

 Strict-Order-Chain-โ„-โ„š-โ„š : Strict-Order-Chain โ„ โ„š โ„š _<_ _<_
 _<_<_ {{Strict-Order-Chain-โ„-โ„š-โ„š}} p q r = (p < q) ร— (q < r)

 Strict-Order-Chain-โ„-โ„š-โ„ : Strict-Order-Chain โ„ โ„š โ„ _<_ _<_
 _<_<_ {{Strict-Order-Chain-โ„-โ„š-โ„}} p q r = (p < q) ร— (q < r)

โ„š<-not-itself-from-โ„ : (p : โ„š) โ†’ (x : โ„) โ†’ ยฌ (p < x < p)
โ„š<-not-itself-from-โ„ p x (lโ‚ , lโ‚‚) = โ„š<-irrefl p (disjoint-from-real x p p (lโ‚ , lโ‚‚))

embedding-โ„š-to-โ„ : โ„š โ†’ โ„
embedding-โ„š-to-โ„ x = (L , R) , inhabited-left'
                             , inhabited-right'
                             , rounded-left'
                             , rounded-right'
                             , disjoint'
                             , located'
 where
  L R : ๐“Ÿ โ„š
  L p = p < x , โ„š<-is-prop p x
  R q = x < q , โ„š<-is-prop x q

  inhabited-left' : โˆƒ p ๊ž‰ โ„š , p < x
  inhabited-left' = โˆฃ โ„š-no-least-element x โˆฃ

  inhabited-right' : โˆƒ q ๊ž‰ โ„š , x < q
  inhabited-right' = โˆฃ โ„š-no-max-element x โˆฃ

  rounded-left' :  (p : โ„š) โ†’ (p โˆˆ L โ†” (โˆƒ p' ๊ž‰ โ„š , p < p' < x))
  rounded-left' p = ฮฑ , ฮฒ
   where
    ฮฑ : p < x โ†’  (โˆƒ p' ๊ž‰ โ„š , p < p' < x)
    ฮฑ l = โˆฃ โ„š-dense p x l โˆฃ

    ฮฒ :  (โˆƒ p' ๊ž‰ โ„š , p < p' < x โ†’ p < x)
    ฮฒ l = โˆฅโˆฅ-rec (โ„š<-is-prop p x) ฮด l
     where
      ฮด : ฮฃ p' ๊ž‰ โ„š , p < p' < x โ†’ p < x
      ฮด (p' , a , b) = โ„š<-trans p p' x a b

  rounded-right' : (q : โ„š) โ†’ q > x โ†” (โˆƒ q' ๊ž‰ โ„š , (q' < q) ร— q' > x)
  rounded-right' q = ฮฑ , ฮฒ
   where
    ฮฑ : q > x โ†’ โˆƒ q' ๊ž‰ โ„š , (q' < q) ร— q' > x
    ฮฑ r = โˆฃ ฮด (โ„š-dense x q r) โˆฃ
     where
      ฮด : (ฮฃ q' ๊ž‰ โ„š , (x < q') ร— (q' < q)) โ†’ ฮฃ q' ๊ž‰ โ„š , (q' < q) ร— q' > x
      ฮด (q' , a , b) = q' , b , a

    ฮฒ : โˆƒ q' ๊ž‰ โ„š , (q' < q) ร— q' > x โ†’ q > x
    ฮฒ r = โˆฅโˆฅ-rec (โ„š<-is-prop x q) ฮด r
     where
      ฮด : ฮฃ q' ๊ž‰ โ„š , (q' < q) ร— q' > x โ†’ x < q
      ฮด (q' , a , b) = โ„š<-trans x q' q b a

  disjoint' : (p q : โ„š) โ†’ p < x < q โ†’ p < q
  disjoint' p q (l , r) = โ„š<-trans p x q l r

  located' : (p q : โ„š) โ†’ p < q โ†’ (p < x) โˆจ (x < q)
  located' p q l = โˆฃ located-property p q x l โˆฃ

instance
 canonical-map-โ„š-to-โ„ : Canonical-Map โ„š โ„
 ฮน {{canonical-map-โ„š-to-โ„}} = embedding-โ„š-to-โ„

โ„ค-to-โ„ : โ„ค โ†’ โ„
โ„ค-to-โ„ z = ฮน (ฮน z)

โ„•-to-โ„ : โ„• โ†’ โ„
โ„•-to-โ„ n = ฮน (ฮน {{canonical-map-โ„•-to-โ„š}} n)

instance
 canonical-map-โ„ค-to-โ„ : Canonical-Map โ„ค โ„
 ฮน {{canonical-map-โ„ค-to-โ„}} = โ„ค-to-โ„

 canonical-map-โ„•-to-โ„ : Canonical-Map โ„• โ„
 ฮน {{canonical-map-โ„•-to-โ„}} = โ„•-to-โ„

0โ„ : โ„
0โ„ = ฮน 0โ„š

1โ„ : โ„
1โ„ = ฮน 1โ„š

1/2โ„ : โ„
1/2โ„ = ฮน 1/2

โ„-equality : (((Lx , Rx) , isCutx) ((Ly , Ry) , isCuty) : โ„)
           โ†’ (Lx ๏ผ Ly)
           โ†’ (Rx ๏ผ Ry)
           โ†’ ((Lx , Rx) , isCutx) ๏ผ ((Ly , Ry) , isCuty)

โ„-equality ((Lx , Rx) , isCutx) ((Ly , Ry) , isCuty) eโ‚  eโ‚‚ = to-subtype-๏ผ (ฮป (L , R) โ†’ isCut-is-prop L R) (to-ร—-๏ผ' (eโ‚ , eโ‚‚))

โ„-equality' : (((Lx , Rx) , isCutx) ((Ly , Ry) , isCuty) : โ„)
           โ†’ (Lx โŠ† Ly)
           โ†’ (Ly โŠ† Lx)
           โ†’ (Rx โŠ† Ry)
           โ†’ (Ry โŠ† Rx)
           โ†’ ((Lx , Rx) , isCutx) ๏ผ ((Ly , Ry) , isCuty)
โ„-equality' x y a b c d = โ„-equality x y (subset-extensionality pe fe a b) (subset-extensionality pe fe c d)

โ„-left-cut-equal-gives-right-cut-equal : (((Lx , Rx) , _) ((Ly , Ry) , _) : โ„)
                                       โ†’ Lx ๏ผ Ly
                                       โ†’ Rx ๏ผ Ry
โ„-left-cut-equal-gives-right-cut-equal ((Lx , Rx) , inhabited-left-x , inhabited-right-x , rounded-left-x , rounded-right-x , disjoint-x , located-x) ((Ly , Ry) , inhabited-left-y , inhabited-right-y , rounded-left-y , rounded-right-y , disjoint-y , located-y) left-cut-equal = I left-subsets
 where
  left-subsets : (Lx โŠ† Ly) ร— (Ly โŠ† Lx)
  left-subsets = โŠ†-refl-consequence Lx Ly left-cut-equal
  I : (Lx โŠ† Ly) ร— (Ly โŠ† Lx) โ†’ Rx ๏ผ Ry
  I (LxโŠ†Ly , LyโŠ†Lx) = subset-extensionality pe fe RxโŠ†Ry RyโŠ†Rx
   where
    RxโŠ†Ry : Rx โŠ† Ry
    RxโŠ†Ry q q-Rx = โˆฅโˆฅ-rec q-Ry-is-prop II obtain-q'
     where
      q-Ry-is-prop : is-prop (q โˆˆ Ry)
      q-Ry-is-prop = โˆˆ-is-prop Ry q
      obtain-q' : โˆƒ q' ๊ž‰ โ„š , (q' < q) ร— q' โˆˆ Rx
      obtain-q' = (prโ‚ (rounded-right-x q)) q-Rx
      II : (ฮฃ q' ๊ž‰ โ„š , (q' < q) ร— q' โˆˆ Rx) โ†’ q โˆˆ Ry
      II (q' , (q'<q , q'-Rx)) = โˆฅโˆฅ-rec q-Ry-is-prop III use-located
       where
        use-located : q' โˆˆ Ly โˆจ q โˆˆ Ry
        use-located = located-y q' q q'<q
        III : q' โˆˆ Ly โˆ” q โˆˆ Ry โ†’ q โˆˆ Ry
        III (inl q'-Ly) = ๐Ÿ˜-elim (โ„š<-irrefl q' from-above)
         where
          get-contradiction : q' โˆˆ Lx
          get-contradiction = LyโŠ†Lx q' q'-Ly
          from-above : q' < q'
          from-above = disjoint-x q' q' (get-contradiction , q'-Rx)
        III (inr q'-Ry) = q'-Ry
    RyโŠ†Rx : Ry โŠ† Rx
    RyโŠ†Rx q q-Ry = โˆฅโˆฅ-rec q-Rx-is-prop II obtain-q'
     where
      q-Rx-is-prop : is-prop (q โˆˆ Rx)
      q-Rx-is-prop = โˆˆ-is-prop Rx q
      obtain-q' : โˆƒ q' ๊ž‰ โ„š , (q' < q) ร— q' โˆˆ Ry
      obtain-q' = (prโ‚ (rounded-right-y q)) q-Ry
      II : ฮฃ q' ๊ž‰ โ„š , (q' < q) ร— q' โˆˆ Ry โ†’ q โˆˆ Rx
      II (q' , (q'<q , q'-Ry))  = โˆฅโˆฅ-rec q-Rx-is-prop III use-located
       where
        use-located : q' โˆˆ Lx โˆจ q โˆˆ Rx
        use-located = located-x q' q q'<q
        III : q' โˆˆ Lx โˆ” q โˆˆ Rx โ†’ q โˆˆ Rx
        III (inl q'-Lx) = ๐Ÿ˜-elim (โ„š<-irrefl q' from-above)
         where
          get-contradiction : q' โˆˆ Ly
          get-contradiction = LxโŠ†Ly q' q'-Lx
          from-above : q' < q'
          from-above = disjoint-y q' q' (get-contradiction , q'-Ry)
        III (inr q-Rx) = q-Rx

โ„-equality-from-left-cut : (((Lx , Rx) , isCutx) ((Ly , Ry) , isCuty) : โ„)
                         โ†’ Lx ๏ผ Ly
                         โ†’ ((Lx , Rx) , isCutx) ๏ผ ((Ly , Ry) , isCuty)
โ„-equality-from-left-cut x y left-cut-equal = โ„-equality x y left-cut-equal right-cut-equal
 where
  right-cut-equal : prโ‚‚ (prโ‚ x) ๏ผ prโ‚‚ (prโ‚ y)
  right-cut-equal = โ„-left-cut-equal-gives-right-cut-equal x y left-cut-equal

โ„-equality-from-left-cut' : (((Lx , Rx) , isCutx) ((Ly , Ry) , isCuty) : โ„)
                          โ†’ Lx โŠ† Ly
                          โ†’ Ly โŠ† Lx
                          โ†’ ((Lx , Rx) , isCutx) ๏ผ ((Ly , Ry) , isCuty)
โ„-equality-from-left-cut' x y s t = โ„-equality-from-left-cut x y (subset-extensionality pe fe s t)

rounded-left-d : (x : โ„) โ†’ (p : โ„š) โ†’ p < x โ†’ โˆƒ q ๊ž‰ โ„š , p < q < x
rounded-left-d x@((L , _) , _ , _ , rl , _) = rounded-left-b L rl

use-rounded-real-L : (x : โ„) (p q : โ„š) โ†’ p < q โ†’ q < x โ†’ p < x
use-rounded-real-L x@((L , _) , _ , _ , rl , _) = rounded-left-c L rl

use-rounded-real-L' : (x : โ„) (p q : โ„š) โ†’ p โ‰ค q โ†’ q < x โ†’ p < x
use-rounded-real-L' x@((L , _) , _ , _ , rl , _) = rounded-left-a L rl

use-rounded-real-R : (x : โ„) (p q : โ„š) โ†’ p < q โ†’ x < p โ†’ x < q
use-rounded-real-R x@((_ , R) , _ , _ , _ , rr , _) = rounded-right-c R rr

use-rounded-real-R' : (x : โ„) (p q : โ„š) โ†’ p โ‰ค q โ†’ x < p โ†’ x < q
use-rounded-real-R' x@((_ , R) , _ , _ , _ , rr , _) = rounded-right-a R rr

disjoint-from-real' : (x : โ„) โ†’ (p q : โ„š) โ†’ (p < x) ร— (x < q) โ†’ p โ‰ค q
disjoint-from-real' x p q (lโ‚ , lโ‚‚) = ฮณ
 where
  I : p < q
  I = disjoint-from-real x p q (lโ‚ , lโ‚‚)

  ฮณ : p โ‰ค q
  ฮณ = โ„š<-coarser-than-โ‰ค p q I

type-of-locator-for-reals : ๐“คโ‚ ฬ‡
type-of-locator-for-reals = (x : โ„) โ†’ (p q : โ„š) โ†’ (p < x) โˆ” (x < q)

\end{code}