Progress

src/real-numbers/arithmetically-located-dedekind-cuts.lagda.md

@@ -42,18 +42,19 @@ open import real-numbers.upper-dedekind-real-numbers
 
 ## Definition
 
-A pair of a [lower Dedekind real](real-numbers.lower-dedekind-real-numbers.md)
-`L` and an [upper Dedekind real](real-numbers.upper-dedekind-real-numbers.md)
+A pair of a [lower Dedekind cut](real-numbers.lower-dedekind-real-numbers.md)
+`L` and an [upper Dedekind cut](real-numbers.upper-dedekind-real-numbers.md)
 `U` is {{#concept "arithmetically located" Disambiguation="Dedekind cut" Agda=arithmetically-located-lower-upper-ℝ}} if
-for any positive [rational number](elementary-number-theory.rational-numbers.md)
-`ε : ℚ`, there exists `p, q : ℚ` where `p ∈ L` and `q ∈ U`, such that
+for any [positive](elementary-number-theory.positive-rational-numbers.md)
+[rational number](elementary-number-theory.rational-numbers.md)
+`ε : ℚ⁺`, there exists `p, q : ℚ` where `p ∈ L` and `q ∈ U`, such that
 `0 < q - p < ε`. Intuitively, when `L , U` represent the cuts of a real number
 `x`, `p` and `q` are rational approximations of `x` to within `ε`. This follows
 parts of Section 11 in {{#cite BauerTaylor2009}}.
 
 ## Definitions
 
-### The predicate of being arithmetically located on pairs of subtypes of rational numbers
+### The predicate of being arithmetically located on pairs of lower and upper Dedekind real numbers
 
 ```agda
 module _
@@ -74,8 +75,7 @@ module _
 
 ### Arithmetically located cuts are located
 
-If a cut is arithmetically located and closed under strict inequality on the
-rational numbers, it is also located.
+If a pair of lower and upper Dedekind cuts is arithmetically located, it is also located.
 
 ```agda
 module _