Cleanups in real numbers

src/elementary-number-theory/absolute-value-rational-numbers.lagda.md

@@ -177,7 +177,7 @@ abstract
         ( q)
         ( rational-abs-ℚ q)
         ( zero-ℚ)
-        ( leq-eq-ℚ _ _ (ap rational-ℚ⁰⁺ abs=0))
+        ( leq-eq-ℚ (ap rational-ℚ⁰⁺ abs=0))
         ( leq-abs-ℚ q))
       ( binary-tr
         ( leq-ℚ)

src/elementary-number-theory/addition-positive-rational-numbers.lagda.md

@@ -169,7 +169,7 @@ module _
   where
 
   le-diff-ℚ⁺ : ℚ⁺
-  le-diff-ℚ⁺ = positive-diff-le-ℚ (rational-ℚ⁺ x) (rational-ℚ⁺ y) H
+  le-diff-ℚ⁺ = positive-diff-le-ℚ H
 
   left-diff-law-add-ℚ⁺ : le-diff-ℚ⁺ +ℚ⁺ x ＝ y
   left-diff-law-add-ℚ⁺ =
@@ -334,23 +334,16 @@ module _
     ((d : ℚ⁺) → leq-ℚ x (y +ℚ (rational-ℚ⁺ d))) → leq-ℚ x y
   leq-leq-add-positive-ℚ H =
     rec-coproduct
-      ( λ I →
+      ( λ y<x →
         ex-falso
           ( not-leq-le-ℚ
             ( mediant-ℚ y x)
             ( x)
-            ( le-right-mediant-ℚ y x I)
+            ( le-right-mediant-ℚ y<x)
             ( tr
               ( leq-ℚ x)
-              ( right-law-positive-diff-le-ℚ
-                ( y)
-                ( mediant-ℚ y x)
-                ( le-left-mediant-ℚ y x I))
-              ( H
-                ( positive-diff-le-ℚ
-                  ( y)
-                  ( mediant-ℚ y x)
-                  ( le-left-mediant-ℚ y x I))))))
+              ( right-law-positive-diff-le-ℚ (le-left-mediant-ℚ y<x))
+              ( H (positive-diff-le-ℚ (le-left-mediant-ℚ y<x))))))
       ( id)
       ( decide-le-leq-ℚ y x)
 

src/elementary-number-theory/addition-rational-numbers.lagda.md

@@ -23,7 +23,6 @@ open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
 open import foundation.equivalences
 open import foundation.identity-types
-open import foundation.injective-maps
 open import foundation.interchange-law
 open import foundation.retractions
 open import foundation.sections

src/elementary-number-theory/difference-rational-numbers.lagda.md

@@ -17,7 +17,6 @@ open import elementary-number-theory.rational-numbers
 open import foundation.action-on-identifications-binary-functions
 open import foundation.action-on-identifications-functions
 open import foundation.identity-types
-open import foundation.interchange-law
 ```
 
 </details>

src/elementary-number-theory/distance-rational-numbers.lagda.md

@@ -21,13 +21,11 @@ open import elementary-number-theory.minimum-rational-numbers
 open import elementary-number-theory.multiplication-nonnegative-rational-numbers
 open import elementary-number-theory.multiplication-rational-numbers
 open import elementary-number-theory.nonnegative-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-binary-functions
 open import foundation.action-on-identifications-functions
-open import foundation.binary-transport
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.function-types
@@ -191,10 +189,7 @@ abstract
       ( rational-dist-ℚ p q)
       ( (rational-abs-ℚ p) +ℚ (rational-abs-ℚ (neg-ℚ q)))
       ( rational-abs-ℚ p +ℚ rational-abs-ℚ q)
-      ( leq-eq-ℚ
-        ( (rational-abs-ℚ p) +ℚ (rational-abs-ℚ (neg-ℚ q)))
-        ( rational-abs-ℚ p +ℚ rational-abs-ℚ q)
-        ( ap (add-ℚ (rational-abs-ℚ p) ∘ rational-ℚ⁰⁺) (abs-neg-ℚ q)))
+      ( leq-eq-ℚ (ap (add-ℚ (rational-abs-ℚ p) ∘ rational-ℚ⁰⁺) (abs-neg-ℚ q)))
       ( triangle-inequality-abs-ℚ p (neg-ℚ q))
 ```
 

src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md

@@ -29,9 +29,7 @@ open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.ring-of-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.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.identity-types
 open import foundation.negated-equality
@@ -45,8 +43,6 @@ open import lists.sequences
 open import metric-spaces.limits-of-sequences-metric-spaces
 open import metric-spaces.metric-space-of-rational-numbers
 open import metric-spaces.uniformly-continuous-functions-metric-spaces
-
-open import order-theory.strictly-increasing-sequences-strictly-preordered-sets
 ```
 
 </details>

src/elementary-number-theory/inequalities-positive-and-negative-rational-numbers.lagda.md

@@ -101,8 +101,8 @@ abstract
 ```agda
 abstract
   is-positive-le-ℚ⁰⁺ :
-    (p : ℚ⁰⁺) (q : ℚ) → le-ℚ (rational-ℚ⁰⁺ p) q → is-positive-ℚ q
-  is-positive-le-ℚ⁰⁺ (p , nonneg-p) q p<q =
+    (p : ℚ⁰⁺) {q : ℚ} → le-ℚ (rational-ℚ⁰⁺ p) q → is-positive-ℚ q
+  is-positive-le-ℚ⁰⁺ (p , nonneg-p) p<q =
     is-positive-le-zero-ℚ
       ( concatenate-leq-le-ℚ _ _ _ (leq-zero-is-nonnegative-ℚ nonneg-p) p<q)
 ```
@@ -112,8 +112,8 @@ abstract
 ```agda
 abstract
   is-negative-le-ℚ⁰⁻ :
-    (q : ℚ⁰⁻) (p : ℚ) → le-ℚ p (rational-ℚ⁰⁻ q) → is-negative-ℚ p
-  is-negative-le-ℚ⁰⁻ (q , nonpos-q) p p<q =
+    (q : ℚ⁰⁻) {p : ℚ} → le-ℚ p (rational-ℚ⁰⁻ q) → is-negative-ℚ p
+  is-negative-le-ℚ⁰⁻ (q , nonpos-q) {p} p<q =
     is-negative-le-zero-ℚ
       ( concatenate-le-leq-ℚ p q zero-ℚ
         ( p<q)

src/elementary-number-theory/inequality-positive-rational-numbers.lagda.md

@@ -13,7 +13,6 @@ open import elementary-number-theory.positive-rational-numbers
 
 open import foundation.action-on-identifications-functions
 open import foundation.binary-relations
-open import foundation.dependent-pair-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.universe-levels
@@ -97,5 +96,5 @@ antisymmetric-leq-ℚ⁺ = antisymmetric-leq-Poset poset-ℚ⁺
 
 ```agda
 leq-eq-ℚ⁺ : {x y : ℚ⁺} → x ＝ y → leq-ℚ⁺ x y
-leq-eq-ℚ⁺ x=y = leq-eq-ℚ _ _ (ap rational-ℚ⁺ x=y)
+leq-eq-ℚ⁺ x=y = leq-eq-ℚ (ap rational-ℚ⁺ x=y)
 ```

src/elementary-number-theory/inequality-rational-numbers.lagda.md

@@ -126,8 +126,8 @@ opaque
     refl-leq-ℤ (numerator-ℚ x *ℤ denominator-ℚ x)
 
 abstract
-  leq-eq-ℚ : (x y : ℚ) → x ＝ y → leq-ℚ x y
-  leq-eq-ℚ x y x=y = tr (leq-ℚ x) x=y (refl-leq-ℚ x)
+  leq-eq-ℚ : {x y : ℚ} → x ＝ y → leq-ℚ x y
+  leq-eq-ℚ {x} refl = refl-leq-ℚ x
 ```
 
 ### Inequality on the rational numbers is antisymmetric
@@ -294,8 +294,8 @@ opaque
   unfolding leq-ℚ-Prop
 
   preserves-leq-rational-ℤ :
-    (x y : ℤ) → leq-ℤ x y → leq-ℚ (rational-ℤ x) (rational-ℤ y)
-  preserves-leq-rational-ℤ x y =
+    {x y : ℤ} → leq-ℤ x y → leq-ℚ (rational-ℤ x) (rational-ℤ y)
+  preserves-leq-rational-ℤ {x} {y} =
     binary-tr leq-ℤ
       ( inv (right-unit-law-mul-ℤ x))
       ( inv (right-unit-law-mul-ℤ y))
@@ -309,7 +309,7 @@ opaque
 
   iff-leq-rational-ℤ :
     (x y : ℤ) → leq-ℤ x y ↔ leq-ℚ (rational-ℤ x) (rational-ℤ y)
-  pr1 (iff-leq-rational-ℤ x y) = preserves-leq-rational-ℤ x y
+  pr1 (iff-leq-rational-ℤ x y) = preserves-leq-rational-ℤ
   pr2 (iff-leq-rational-ℤ x y) = reflects-leq-rational-ℤ x y
 ```
 
@@ -324,8 +324,9 @@ abstract
     iff-leq-int-ℕ x y
 
   preserves-leq-rational-ℕ :
-    (x y : ℕ) → leq-ℕ x y → leq-ℚ (rational-ℕ x) (rational-ℕ y)
-  preserves-leq-rational-ℕ x y = forward-implication (iff-leq-rational-ℕ x y)
+    {x y : ℕ} → leq-ℕ x y → leq-ℚ (rational-ℕ x) (rational-ℕ y)
+  preserves-leq-rational-ℕ {x} {y} =
+    forward-implication (iff-leq-rational-ℕ x y)
 
   reflects-leq-rational-ℕ :
     (x y : ℕ) → leq-ℚ (rational-ℕ x) (rational-ℕ y) → leq-ℕ x y

src/elementary-number-theory/metric-additive-group-of-rational-numbers.lagda.md

@@ -9,9 +9,7 @@ module elementary-number-theory.metric-additive-group-of-rational-numbers where
 ```agda
 open import analysis.metric-abelian-groups
 
-open import elementary-number-theory.addition-rational-numbers
 open import elementary-number-theory.additive-group-of-rational-numbers
-open import elementary-number-theory.rational-numbers
 
 open import foundation.dependent-pair-types
 open import foundation.universe-levels

src/elementary-number-theory/multiplication-closed-intervals-rational-numbers.lagda.md

@@ -924,7 +924,7 @@ abstract
           rational-dist-ℚ (a *ℚ q) (b *ℚ q)
           ≤ rational-dist-ℚ a b *ℚ rational-abs-ℚ q
             by
-              leq-eq-ℚ _ _
+              leq-eq-ℚ
                 ( ( ap
                     ( rational-abs-ℚ)
                     ( inv (right-distributive-mul-diff-ℚ _ _ _))) ∙
@@ -939,7 +939,7 @@ abstract
           ≤ width-closed-interval-ℚ [a,b] *ℚ
             rational-max-abs-closed-interval-ℚ [c,d]
             by
-              leq-eq-ℚ _ _
+              leq-eq-ℚ
                 ( ap-mul-ℚ
                   ( eq-width-dist-lower-upper-bounds-closed-interval-ℚ [a,b])
                   ( refl))
@@ -951,7 +951,7 @@ abstract
           rational-dist-ℚ (p *ℚ c) (p *ℚ d)
           ≤ rational-dist-ℚ c d *ℚ rational-abs-ℚ p
             by
-              leq-eq-ℚ _ _
+              leq-eq-ℚ
                 ( ( ap
                     ( rational-abs-ℚ)
                     ( inv (left-distributive-mul-diff-ℚ _ _ _))) ∙
@@ -966,7 +966,7 @@ abstract
                 ( leq-max-abs-is-in-closed-interval-ℚ [a,b] p p∈[a,b])
           ≤ _
             by
-              leq-eq-ℚ _ _
+              leq-eq-ℚ
                 ( ap-mul-ℚ
                   ( eq-width-dist-lower-upper-bounds-closed-interval-ℚ [c,d])
                   ( refl))
@@ -983,7 +983,7 @@ abstract
           rational-dist-ℚ (a *ℚ c) (b *ℚ d)
           ≤ rational-abs-ℚ ((a *ℚ c -ℚ b *ℚ c) +ℚ (b *ℚ c -ℚ b *ℚ d))
             by
-              leq-eq-ℚ _ _
+              leq-eq-ℚ
                 ( ap
                   ( rational-abs-ℚ)
                   ( inv ( mul-right-div-Group group-add-ℚ _ _ _)))
@@ -996,7 +996,7 @@ abstract
           rational-dist-ℚ (a *ℚ d) (b *ℚ c)
           ≤ rational-abs-ℚ ((a *ℚ d -ℚ b *ℚ d) +ℚ (b *ℚ d -ℚ b *ℚ c))
             by
-              leq-eq-ℚ _ _
+              leq-eq-ℚ
                 ( ap
                   ( rational-abs-ℚ)
                   ( inv ( mul-right-div-Group group-add-ℚ _ _ _)))
@@ -1006,7 +1006,7 @@ abstract
           ≤ rational-dist-ℚ (a *ℚ d) (b *ℚ d) +ℚ
             rational-dist-ℚ (b *ℚ c) (b *ℚ d)
             by
-              leq-eq-ℚ _ _
+              leq-eq-ℚ
                 ( ap-add-ℚ refl (ap rational-ℚ⁰⁺ (commutative-dist-ℚ _ _)))
           ≤ <b-a><max|c||d|> +ℚ <d-c><max|a||b|>
             by preserves-leq-add-ℚ |ad-bd|≤<b-a>max|c||d| |bc-bd|≤<d-c>max|a||b|
@@ -1042,7 +1042,7 @@ abstract
         chain-of-inequalities
           rational-dist-ℚ q q
           ≤ zero-ℚ
-            by leq-eq-ℚ _ _ (rational-dist-self-ℚ q)
+            by leq-eq-ℚ (rational-dist-self-ℚ q)
           ≤ <b-a><max|c||d|> +ℚ <d-c><max|a||b|>
             by
               leq-zero-rational-ℚ⁰⁺ (<b-a><max|c||d|>⁰⁺ +ℚ⁰⁺ <d-c><max|a||b|>⁰⁺)

src/elementary-number-theory/multiplication-interior-closed-intervals-rational-numbers.lagda.md

@@ -1,6 +1,8 @@
 # Multiplication of interior intervals of closed intervals of rational numbers
 
 ```agda
+{-# OPTIONS --lossy-unification #-}
+
 module elementary-number-theory.multiplication-interior-closed-intervals-rational-numbers where
 ```
 
@@ -325,12 +327,10 @@ abstract
                 ( a'<b')
                 ( c'<d')
                 ( min'=a'c')
-            is-pos-b' =
-              is-positive-le-ℚ⁰⁺ (a' , is-nonneg-a') b' a'<b'
-            is-pos-b = is-positive-le-ℚ⁺ (b' , is-pos-b') b b'<b
-            is-pos-d' =
-              is-positive-le-ℚ⁰⁺ (c' , is-nonneg-c') d' c'<d'
-            is-pos-d = is-positive-le-ℚ⁺ (d' , is-pos-d') d d'<d
+            is-pos-b' = is-positive-le-ℚ⁰⁺ (a' , is-nonneg-a') a'<b'
+            is-pos-b = is-positive-le-ℚ⁺ (b' , is-pos-b') b'<b
+            is-pos-d' = is-positive-le-ℚ⁰⁺ (c' , is-nonneg-c') c'<d'
+            is-pos-d = is-positive-le-ℚ⁺ (d' , is-pos-d') d'<d
             is-nonneg-min' =
               inv-tr
                 ( is-nonnegative-ℚ)
@@ -377,11 +377,7 @@ abstract
                         ( le-ℚ (a *ℚ c'))
                         ( min'=a'c')
                         ( preserves-le-right-mul-ℚ⁺
-                          ( c' ,
-                            is-positive-le-ℚ⁰⁺
-                              ( c , is-nonneg-c)
-                              ( c')
-                              ( c<c'))
+                          ( c' , is-positive-le-ℚ⁰⁺ (c , is-nonneg-c) c<c')
                           ( a)
                           ( a')
                           ( a<a'))))
@@ -403,10 +399,8 @@ abstract
                 ( a'<b')
                 ( c'<d')
                 ( min'=a'd')
-            is-neg-a =
-              is-negative-le-ℚ⁰⁻ (a' , is-nonpos-a') a a<a'
-            is-pos-d =
-              is-positive-le-ℚ⁰⁺ (d' , is-nonneg-d') d d'<d
+            is-neg-a = is-negative-le-ℚ⁰⁻ (a' , is-nonpos-a') a<a'
+            is-pos-d = is-positive-le-ℚ⁰⁺ (d' , is-nonneg-d') d'<d
           in
             concatenate-leq-le-ℚ
               ( min)
@@ -444,8 +438,8 @@ abstract
                 ( a'<b')
                 ( c'<d')
                 ( min'=b'c')
-            is-pos-b = is-positive-le-ℚ⁰⁺ (b' , is-nonneg-b') b b'<b
-            is-neg-c = is-negative-le-ℚ⁰⁻ (c' , is-nonpos-c') c c<c'
+            is-pos-b = is-positive-le-ℚ⁰⁺ (b' , is-nonneg-b') b'<b
+            is-neg-c = is-negative-le-ℚ⁰⁻ (c' , is-nonpos-c') c<c'
           in
             concatenate-le-leq-ℚ
               ( min)
@@ -481,12 +475,10 @@ abstract
                 ( a'<b')
                 ( c'<d')
                 ( min'=b'd')
-            is-neg-a' =
-              is-negative-le-ℚ⁰⁻ (b' , is-nonpos-b') a' a'<b'
-            is-neg-a = is-negative-le-ℚ⁻ (a' , is-neg-a') a a<a'
-            is-neg-c' =
-              is-negative-le-ℚ⁰⁻ (d' , is-nonpos-d') c' c'<d'
-            is-neg-c = is-negative-le-ℚ⁻ (c' , is-neg-c') c c<c'
+            is-neg-a' = is-negative-le-ℚ⁰⁻ (b' , is-nonpos-b') a'<b'
+            is-neg-a = is-negative-le-ℚ⁻ (a' , is-neg-a') a<a'
+            is-neg-c' = is-negative-le-ℚ⁰⁻ (d' , is-nonpos-d') c'<d'
+            is-neg-c = is-negative-le-ℚ⁻ (c' , is-neg-c') c<c'
             is-nonneg-min' =
               inv-tr
                 ( is-nonnegative-ℚ)
@@ -533,11 +525,7 @@ abstract
                           ( le-ℚ (b' *ℚ d))
                           ( min'=b'd')
                           ( reverses-le-left-mul-ℚ⁻
-                            ( b' ,
-                              is-negative-le-ℚ⁰⁻
-                                ( b , is-nonpos-b)
-                                ( b')
-                                ( b'<b))
+                            ( b' , is-negative-le-ℚ⁰⁻ (b , is-nonpos-b) b'<b)
                             ( d')
                             ( d)
                             ( d'<d)))))

src/elementary-number-theory/multiplication-positive-rational-numbers.lagda.md

@@ -357,6 +357,6 @@ abstract
   leq-left-mul-leq-one-ℚ⁺ p⁺@(p , _) p≤1 q⁺@(q , _) =
     trichotomy-le-ℚ p one-ℚ
       ( λ p<1 → leq-le-ℚ (le-left-mul-less-than-one-ℚ⁺ p⁺ p<1 q⁺))
-      ( λ p=1 → leq-eq-ℚ _ _ (ap-mul-ℚ p=1 refl ∙ left-unit-law-mul-ℚ q))
+      ( λ p=1 → leq-eq-ℚ (ap-mul-ℚ p=1 refl ∙ left-unit-law-mul-ℚ q))
       ( λ 1<p → ex-falso (not-leq-le-ℚ one-ℚ p 1<p p≤1))
 ```

src/elementary-number-theory/multiplicative-group-of-rational-numbers.lagda.md

@@ -16,7 +16,6 @@ open import elementary-number-theory.multiplication-positive-rational-numbers
 open import elementary-number-theory.multiplication-rational-numbers
 open import elementary-number-theory.multiplicative-monoid-of-rational-numbers
 open import elementary-number-theory.negative-rational-numbers
-open import elementary-number-theory.nonnegative-rational-numbers
 open import elementary-number-theory.nonzero-rational-numbers
 open import elementary-number-theory.positive-and-negative-rational-numbers
 open import elementary-number-theory.positive-rational-numbers
@@ -27,7 +26,6 @@ open import elementary-number-theory.strict-inequality-rational-numbers
 open import foundation.action-on-identifications-functions
 open import foundation.coproduct-types
 open import foundation.dependent-pair-types
-open import foundation.empty-types
 open import foundation.function-types
 open import foundation.identity-types
 open import foundation.negated-equality