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

Co-authored-by: Fredrik Bakke <[email protected]>
UniMath · Feb 27, 2024 · 86e09b2 · 86e09b2
1 parent 9e95664
commit 86e09b2
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
@@ -110,8 +110,8 @@ module _
   is-rational-ℝ-Prop : Prop l
   is-rational-ℝ-Prop =
     product-Prop
-      ( neg-Prop ( lower-cut-ℝ x p))
-      ( neg-Prop ( upper-cut-ℝ x p))
+      ( neg-Prop (lower-cut-ℝ x p))
+      ( neg-Prop (upper-cut-ℝ x p))
 
   is-rational-ℝ : UU l
   is-rational-ℝ = type-Prop is-rational-ℝ-Prop