Double negation stability of equality on Dedekind real numbers (#1703)

Author: fredrik-bakke

references.bib

@@ -149,6 +149,15 @@ @online{BdJR24
   keywords      = {Computer Science - Logic in Computer Science,Mathematics - Algebraic Topology,Mathematics - Category Theory},
 }
 
+@misc{BH25,
+  title         = {The Countable Reals},
+  author        = {Andrej Bauer and James E. Hanson},
+  year          = 2025,
+  eprint        = {2404.01256},
+  archiveprefix = {arXiv},
+  primaryclass  = {math.LO},
+}
+
 @phdthesis{Booij20PhD,
   title         = {Analysis in univalent type theory},
   author        = {Booij, Auke Bart},

src/real-numbers.lagda.md

@@ -23,6 +23,7 @@ open import real-numbers.dedekind-real-numbers public
 open import real-numbers.difference-real-numbers public
 open import real-numbers.distance-real-numbers public
 open import real-numbers.enclosing-closed-rational-intervals-real-numbers public
+open import real-numbers.equality-real-numbers public
 open import real-numbers.finitely-enumerable-subsets-real-numbers public
 open import real-numbers.geometric-sequences-real-numbers public
 open import real-numbers.inequalities-addition-and-subtraction-real-numbers public

src/real-numbers/equality-real-numbers.lagda.md

@@ -0,0 +1,69 @@
+# Equality of real numbers
+
+```agda
+module real-numbers.equality-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.double-negation
+open import foundation.double-negation-stable-equality
+open import foundation.identity-types
+open import foundation.sets
+open import foundation.universe-levels
+
+open import real-numbers.dedekind-real-numbers
+open import real-numbers.inequality-real-numbers
+open import real-numbers.similarity-real-numbers
+```
+
+</details>
+
+## Idea
+
+We record that [equality](foundation-core.identity-types.md) and
+[similarity](real-numbers.similarity-real-numbers.md) of
+[Dedekind real numbers](real-numbers.dedekind-real-numbers.md) and
+[double negation stable](foundation.double-negation-stable-equality.md).
+
+## Properties
+
+### Similarity of Dedekind real numbers is double negation stable
+
+```agda
+module _
+  {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2}
+  where abstract
+
+  double-negation-elim-sim-ℝ : ¬¬ (x ~ℝ y) → x ~ℝ y
+  double-negation-elim-sim-ℝ H =
+    sim-antisymmetric-leq-ℝ x y
+      ( double-negation-elim-leq-ℝ x y (map-double-negation leq-sim-ℝ H))
+      ( double-negation-elim-leq-ℝ y x (map-double-negation leq-sim-ℝ' H))
+```
+
+### Equality of Dedekind real numbers is double negation stable
+
+```agda
+module _
+  {l : Level} {x y : ℝ l}
+  where abstract
+
+  double-negation-elim-eq-ℝ : ¬¬ (x ＝ y) → x ＝ y
+  double-negation-elim-eq-ℝ H =
+    eq-sim-ℝ (double-negation-elim-sim-ℝ (map-double-negation sim-eq-ℝ H))
+```
+
+### The Dedekind real numbers form a set
+
+This fact is already demonstrated in
+[`real-numbers.dedekind-real-numbers`](real-numbers.dedekind-real-numbers.md),
+but we give a second proof using the fact that equality satisfies double
+negation elimination.
+
+```agda
+is-set-ℝ' : {l : Level} → is-set (ℝ l)
+is-set-ℝ' =
+  is-set-has-double-negation-stable-equality (λ x y → double-negation-elim-eq-ℝ)
+```

src/real-numbers/inequality-real-numbers.lagda.md

@@ -16,6 +16,8 @@ open import elementary-number-theory.strict-inequality-rational-numbers
 open import foundation.cartesian-product-types
 open import foundation.complements-subtypes
 open import foundation.dependent-pair-types
+open import foundation.disjunction
+open import foundation.double-negation
 open import foundation.empty-types
 open import foundation.existential-quantification
 open import foundation.function-types
@@ -189,6 +191,9 @@ abstract opaque
 
   leq-sim-ℝ : {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → sim-ℝ x y → leq-ℝ x y
   leq-sim-ℝ = pr1
+
+  leq-sim-ℝ' : {l1 l2 : Level} {x : ℝ l1} {y : ℝ l2} → sim-ℝ x y → leq-ℝ y x
+  leq-sim-ℝ' = pr2
 ```
 
 ### Inequality on the real numbers is antisymmetric
@@ -413,6 +418,39 @@ module _
           leq-leq-rational-ℝ y x (λ q → forward-implication (H q)))
 ```
 
+### Double negation elimination of inequality
+
+Given two Dedekind real numbers `x` and `y` such that `¬¬(x ≤ y)`, then `x ≤ y`.
+
+We follow the proof of Proposition 5.2 in {{#cite BH25}}.
+
+**Proof.** Assume `¬¬(x ≤ y)`, and let `q : ℚ` such that `q ∈ Lx`. Then by
+roundedness of `Lx` there exists an `r : ℚ` such that `q < r` and `r ∈ Lx`.
+Because `y` is located, we have that `q ∈ Ly` or `r ∈ Uy`. In the first case we
+are already done, so assume `r ∈ Uy`. By `¬¬(x ≤ y)` we also know that
+`¬¬ (r ∈ Ly)`, but the lower and upper cuts of `y` are disjoint, so we have
+reached a contradiction. ∎
+
+```agda
+module _
+  {l1 l2 : Level} (x : ℝ l1) (y : ℝ l2)
+  where abstract opaque
+
+  unfolding leq-ℝ
+
+  double-negation-elim-leq-ℝ : ¬¬ (leq-ℝ x y) → leq-ℝ x y
+  double-negation-elim-leq-ℝ H q Q =
+    rec-trunc-Prop
+      ( lower-cut-ℝ y q)
+      ( λ (r , q<r , R) →
+        elim-disjunction
+          ( lower-cut-ℝ y q)
+          ( id)
+          ( λ r∈Uy → ex-falso (H (λ L → is-disjoint-cut-ℝ y r (L r R , r∈Uy))))
+          ( is-located-lower-upper-cut-ℝ y q<r))
+      ( forward-implication (is-rounded-lower-cut-ℝ x q) Q)
+```
+
 ## References
 
 {{#bibliography}}

src/real-numbers/similarity-real-numbers.lagda.md

@@ -190,3 +190,9 @@ abstract opaque
 
   syntax step-similarity-reasoning-ℝ p u q = p ~ℝ u by q
 ```
+
+## See also
+
+- In
+  [`real-numbers.equality-real-numbers`](real-numbers.equality-real-numbers.md)
+  it is demonstrated that similarity is double negation stable.