cleanup

Author: malarbol

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

@@ -49,7 +49,6 @@ open import foundation.function-types
 open import foundation.identity-types
 open import foundation.logical-equivalences
 open import foundation.negation
-open import foundation.pi-decompositions
 open import foundation.propositional-truncations
 open import foundation.propositions
 open import foundation.sets
@@ -874,26 +873,6 @@ module _
           ( r<s+right))
 ```
 
-```agda
-module _
-  {l1 l2 l3 : Level}
-  (P : ℚ⁺ → UU l1)
-  (Q : ℚ⁺ → UU l2)
-  (R : ℚ⁺ → UU l3)
-  (merge-add-family-ℚ⁺ : (d₁ d₂ : ℚ⁺) → P d₁ → Q d₂ → R (d₁ +ℚ⁺ d₂))
-  where
-
-  Π-merge-family-ℚ⁺ : Π ℚ⁺ P → Π ℚ⁺ Q → Π ℚ⁺ R
-  Π-merge-family-ℚ⁺ H K d =
-    tr R
-      ( eq-add-split-ℚ⁺ d)
-      ( merge-add-family-ℚ⁺
-        ( left-summand-split-ℚ⁺ d)
-        ( right-summand-split-ℚ⁺ d)
-        ( H (left-summand-split-ℚ⁺ d))
-        ( K (right-summand-split-ℚ⁺ d)))
-```
-
 ### Any two positive rational numbers have a positive rational number strictly less than both
 
 ```agda

src/metric-spaces/limits-sequences-pseudometric-spaces.lagda.md

@@ -122,28 +122,37 @@ module _
     modulus-limit-sequence-Pseudometric-Space M u x →
     modulus-limit-sequence-Pseudometric-Space M u y →
     is-indistinguishable-Pseudometric-Space M x y
-  indistinguishable-limit-modulus-limit-sequence-Pseudometric-Space mx my =
-    Π-merge-family-ℚ⁺
-      ( λ d →
-        Σ ( ℕ)
-          ( λ N →
-            (n : ℕ) →
-            leq-ℕ N n →
-            neighborhood-Pseudometric-Space M d (u n) x))
-      ( λ d →
-        Σ ( ℕ)
-          ( λ N →
-            (n : ℕ) →
-            leq-ℕ N n →
-            neighborhood-Pseudometric-Space M d (u n) y))
+  indistinguishable-limit-modulus-limit-sequence-Pseudometric-Space mx my ε =
+    tr
       ( is-upper-bound-dist-Pseudometric-Space M x y)
-      ( tr-modulus-indistinguishable)
-      ( λ d →
-        modulus-modulus-limit-sequence-Pseudometric-Space M u x mx d ,
-        is-modulus-modulus-limit-sequence-Pseudometric-Space M u x mx d)
-      ( λ d →
-        modulus-modulus-limit-sequence-Pseudometric-Space M u y my d ,
-        is-modulus-modulus-limit-sequence-Pseudometric-Space M u y my d)
+      ( eq-add-split-ℚ⁺ ε)
+      ( tr-modulus-indistinguishable
+        ( left-summand-split-ℚ⁺ ε)
+        ( right-summand-split-ℚ⁺ ε)
+        ( ( modulus-modulus-limit-sequence-Pseudometric-Space
+            ( M)
+            ( u)
+            ( x)
+            ( mx)
+            ( left-summand-split-ℚ⁺ ε)) ,
+          ( is-modulus-modulus-limit-sequence-Pseudometric-Space
+            ( M)
+            ( u)
+            ( x)
+            ( mx)
+            ( left-summand-split-ℚ⁺ ε)))
+        ( ( modulus-modulus-limit-sequence-Pseudometric-Space
+            ( M)
+            ( u)
+            ( y)
+            ( my)
+            ( right-summand-split-ℚ⁺ ε)) ,
+          ( is-modulus-modulus-limit-sequence-Pseudometric-Space
+            ( M)
+            ( u)
+            ( y)
+            ( my)
+            ( right-summand-split-ℚ⁺ ε))))
     where
       tr-modulus-indistinguishable :
         (d₁ d₂ : ℚ⁺) →