Update src/real-numbers/rational-real-numbers.lagda.md

Co-authored-by: Fredrik Bakke <[email protected]>
UniMath · Feb 27, 2024 · 3a32dae · 3a32dae
1 parent c3336ca
commit 3a32dae
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md
@@ -211,8 +211,8 @@ eq-real-rational-is-rational-ℝ x q H =
             ( is-located-lower-upper-cut-ℝ x r q I))
           ( trichotomy-le-ℚ r q
             ( λ I _ → I)
-            ( λ E H' → ex-falso ( pr1 ( tr ( is-rational-ℝ x) ( inv E) H) H'))
-            ( λ I H' → ex-falso ( pr1 H ( le-lower-cut-ℝ x q r I H'))))))
+            ( λ E H' → ex-falso (pr1 (tr (is-rational-ℝ x) (inv E) H) H'))
+            ( λ I H' → ex-falso (pr1 H (le-lower-cut-ℝ x q r I H'))))))
 ```
 
 ### The cannonical map from rationals to rational reals