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

Co-authored-by: Fredrik Bakke <[email protected]>
UniMath · Feb 27, 2024 · c3336ca · c3336ca
1 parent 39a8b54
commit c3336ca
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md
@@ -46,7 +46,7 @@ the [image](foundation.images.md) of this embedding
 
 ## Definitions
 
-### Strict inequality on rational gives Dedekind cuts
+### Strict inequality on rationals gives Dedekind cuts
 
 ```agda
 is-dedekind-cut-le-ℚ :