Dedekind real numbers

Content created by Egbert Rijke, Elif Uskuplu and Fredrik Bakke.

Created on 2023-04-08.
Last modified on 2023-04-28.

module real-numbers.dedekind-real-numbers where
open import elementary-number-theory.inequality-rational-numbers
open import elementary-number-theory.rational-numbers

open import foundation.dependent-pair-types
open import foundation.disjunction
open import foundation.existential-quantification
open import foundation.logical-equivalences
open import foundation.negation
open import foundation.propositions
open import foundation.sets
open import foundation.truncated-types
open import foundation.universe-levels

open import foundation-core.truncation-levels


A Dedekind cut consists a pair (L , U) of subtypes of , satisfying the following four conditions

  1. Inhabitedness. Both L and U are inhabited subtypes of .
  2. Roundedness. A rational number q is in L if and only if there exists q < r such that r ∈ L, and a rational number r is in U if and only if there exists q < r such that q ∈ U.
  3. Disjointness. L and U are disjoint subsets of .
  4. Locatedness. If q < r then q ∈ L or r ∈ U.

The type of Dedekind real numbers is the type of all dedekind cuts. The Dedekind real numbers will be taken as the standard definition of the real numbers in the agda-unimath library.


Dedekind cuts

is-dedekind-cut-Prop :
  {l : Level}  (  Prop l)  (  Prop l)  Prop l
is-dedekind-cut-Prop L U =
    ( prod-Prop (exists-Prop  L) (exists-Prop  U))
    ( prod-Prop
      ( prod-Prop
        ( Π-Prop 
          ( λ q 
              ( L q)
              ( exists-Prop   r  prod-Prop (le-ℚ-Prop q r) (L r)))))
        ( Π-Prop 
          ( λ r 
              ( U r)
              ( exists-Prop   q  prod-Prop (le-ℚ-Prop q r) (U q))))))
      ( prod-Prop
        ( Π-Prop   q  neg-Prop (prod-Prop (L q) (U q))))
        ( Π-Prop 
          ( λ q 
              ( λ r 
                  ( le-ℚ-Prop q r)
                  ( disj-Prop (L q) (U r)))))))

is-dedekind-cut :
  {l : Level}  (  Prop l)  (  Prop l)  UU l
is-dedekind-cut L U = type-Prop (is-dedekind-cut-Prop L U)

The Dedekind real numbers

 : (l : Level)  UU (lsuc l)
 l = Σ (  Prop l)  L  Σ (  Prop l) (is-dedekind-cut L))

ℝ is a set


  is-set-ℝ : (l : Level)  is-set ( l)
  is-set-ℝ l =
      ( is-set-function-type (is-trunc-Truncated-Type neg-one-𝕋))
      ( λ x 
        ( is-set-Σ
          ( is-set-function-type (is-trunc-Truncated-Type neg-one-𝕋))
          ( λ y 
            ( is-set-is-prop
              ( is-prop-type-Prop
                ( is-dedekind-cut-Prop x y))))))

ℝ-Set : (l : Level)  Set (lsuc l)
pr1 (ℝ-Set l) =  l
pr2 (ℝ-Set l) = is-set-ℝ l

Recent changes