Cleanups in real numbers (#1675)

I started out wanting to make some parameters implicit, now that with
`opaque` definitions they can reliably be inferred from the context.

Then things snowballed from there to include a bunch of #1545, use of
`abstract opaque`, and elimination of redundant imports.

Author: lowasser

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