diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md
index 8dfdb41987..8548212757 100644
--- a/src/elementary-number-theory.lagda.md
+++ b/src/elementary-number-theory.lagda.md
@@ -27,6 +27,7 @@ open import elementary-number-theory.collatz-conjecture public
 open import elementary-number-theory.commutative-semiring-of-natural-numbers public
 open import elementary-number-theory.congruence-integers public
 open import elementary-number-theory.congruence-natural-numbers public
+open import elementary-number-theory.cross-multiplication-difference-integer-fractions public
 open import elementary-number-theory.cubes-natural-numbers public
 open import elementary-number-theory.decidable-dependent-function-types public
 open import elementary-number-theory.decidable-total-order-natural-numbers public
@@ -73,6 +74,7 @@ open import elementary-number-theory.legendre-symbol public
 open import elementary-number-theory.lower-bounds-natural-numbers public
 open import elementary-number-theory.maximum-natural-numbers public
 open import elementary-number-theory.maximum-standard-finite-types public
+open import elementary-number-theory.mediant-integer-fractions public
 open import elementary-number-theory.mersenne-primes public
 open import elementary-number-theory.minimum-natural-numbers public
 open import elementary-number-theory.minimum-standard-finite-types public
diff --git a/src/elementary-number-theory/addition-integers.lagda.md b/src/elementary-number-theory/addition-integers.lagda.md
index f8fd31eb59..8b93313e77 100644
--- a/src/elementary-number-theory/addition-integers.lagda.md
+++ b/src/elementary-number-theory/addition-integers.lagda.md
@@ -536,6 +536,20 @@ is-positive-add-ℤ {inr (inr (succ-ℕ x))} {inr (inr y)} H K =
   is-positive-succ-ℤ
     ( is-nonnegative-is-positive-ℤ
       ( is-positive-add-ℤ {inr (inr x)} {inr (inr y)} star star))
+
+is-positive-add-nonnegative-positive-ℤ :
+  {x y : ℤ} → is-nonnegative-ℤ x → is-positive-ℤ y → is-positive-ℤ (x +ℤ y)
+is-positive-add-nonnegative-positive-ℤ {inr (inl x)} {y} H H' =
+  is-positive-eq-ℤ refl H'
+is-positive-add-nonnegative-positive-ℤ {inr (inr x)} {y} H H' =
+  is-positive-add-ℤ {inr (inr x)} {y} H H'
+
+is-positive-add-positive-nonnegative-ℤ :
+  {x y : ℤ} → is-positive-ℤ x → is-nonnegative-ℤ y → is-positive-ℤ (x +ℤ y)
+is-positive-add-positive-nonnegative-ℤ {x} {y} H H' =
+  is-positive-eq-ℤ
+    ( commutative-add-ℤ y x)
+    ( is-positive-add-nonnegative-positive-ℤ H' H)
 ```
 
 ### The inclusion of ℕ into ℤ preserves addition
diff --git a/src/elementary-number-theory/cross-multiplication-difference-integer-fractions.lagda.md b/src/elementary-number-theory/cross-multiplication-difference-integer-fractions.lagda.md
new file mode 100644
index 0000000000..8fb4af6bbc
--- /dev/null
+++ b/src/elementary-number-theory/cross-multiplication-difference-integer-fractions.lagda.md
@@ -0,0 +1,219 @@
+# The cross-multiplication difference of two integer fractions
+
+```agda
+module elementary-number-theory.cross-multiplication-difference-integer-fractions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-integers
+open import elementary-number-theory.difference-integers
+open import elementary-number-theory.integer-fractions
+open import elementary-number-theory.integers
+open import elementary-number-theory.multiplication-integers
+
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.negation
+open import foundation.propositions
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "cross-multiplication difference" Agda=cross-mul-diff-fraction-ℤ}} of
+two [integer fractions](elementary-number-theory.integer-fractions.md) `a/b` and
+`c/d` is the [difference](elementary-number-theory.difference-integers.md) of
+the [products](elementary-number-theory.multiplication-integers.md) of the
+numerator of each fraction with the denominator of the other: `c * b - a * d`.
+
+## Definitions
+
+### The cross-multiplication difference of two fractions
+
+```agda
+cross-mul-diff-fraction-ℤ : fraction-ℤ → fraction-ℤ → ℤ
+cross-mul-diff-fraction-ℤ x y =
+  diff-ℤ
+    ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x)
+    ( numerator-fraction-ℤ x *ℤ denominator-fraction-ℤ y)
+```
+
+## Properties
+
+### Swapping the fractions changes the sign of the cross-multiplication difference
+
+```agda
+skew-commutative-cross-mul-diff-fraction-ℤ :
+  (x y : fraction-ℤ) →
+  Id
+    ( neg-ℤ (cross-mul-diff-fraction-ℤ x y))
+    ( cross-mul-diff-fraction-ℤ y x)
+skew-commutative-cross-mul-diff-fraction-ℤ x y =
+  distributive-neg-diff-ℤ
+    ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x)
+    ( numerator-fraction-ℤ x *ℤ denominator-fraction-ℤ y)
+```
+
+### Two fractions are similar when their cross-multiplication difference is zero
+
+```agda
+module _
+  (x y : fraction-ℤ)
+  where
+
+  is-zero-cross-mul-diff-sim-fraction-ℤ :
+    sim-fraction-ℤ x y →
+    is-zero-ℤ (cross-mul-diff-fraction-ℤ x y)
+  is-zero-cross-mul-diff-sim-fraction-ℤ H =
+    is-zero-diff-ℤ (inv H)
+
+  sim-is-zero-coss-mul-diff-fraction-ℤ :
+    is-zero-ℤ (cross-mul-diff-fraction-ℤ x y) →
+    sim-fraction-ℤ x y
+  sim-is-zero-coss-mul-diff-fraction-ℤ H = inv (eq-diff-ℤ H)
+```
+
+## The transitive-additive property for the cross-multiplication difference
+
+Given three fractions `a/b`, `x/y` and `m/n`, the pairwise cross-multiplication
+differences satisfy a transitive-additive property:
+
+```text
+  y * (m * b - a * n) = b * (m * y - x * n) + n * (x * b - a * y)
+```
+
+```agda
+lemma-add-cross-mul-diff-fraction-ℤ :
+  (p q r : fraction-ℤ) →
+  Id
+    ( add-ℤ
+      ( denominator-fraction-ℤ p *ℤ cross-mul-diff-fraction-ℤ q r)
+      ( denominator-fraction-ℤ r *ℤ cross-mul-diff-fraction-ℤ p q))
+    ( denominator-fraction-ℤ q *ℤ cross-mul-diff-fraction-ℤ p r)
+lemma-add-cross-mul-diff-fraction-ℤ
+  (np , dp , hp)
+  (nq , dq , hq)
+  (nr , dr , hr) =
+  equational-reasoning
+  add-ℤ
+    (dp *ℤ (nr *ℤ dq -ℤ nq *ℤ dr))
+    (dr *ℤ (nq *ℤ dp -ℤ np *ℤ dq))
+  ＝ add-ℤ
+      (dp *ℤ (nr *ℤ dq) -ℤ dp *ℤ (nq *ℤ dr))
+      (dr *ℤ (nq *ℤ dp) -ℤ dr *ℤ (np *ℤ dq))
+    by
+      ap-add-ℤ
+        ( inv (linear-diff-left-mul-ℤ dp (nr *ℤ dq) (nq *ℤ dr)))
+        ( inv (linear-diff-left-mul-ℤ dr (nq *ℤ dp) (np *ℤ dq)))
+  ＝ diff-ℤ
+      (dp *ℤ (nr *ℤ dq) +ℤ dr *ℤ (nq *ℤ dp))
+      (dp *ℤ (nq *ℤ dr) +ℤ dr *ℤ (np *ℤ dq))
+    by
+      interchange-law-add-diff-ℤ
+        ( mul-ℤ dp ( mul-ℤ nr dq))
+        ( mul-ℤ dp ( mul-ℤ nq dr))
+        ( mul-ℤ dr ( mul-ℤ nq dp))
+        ( mul-ℤ dr ( mul-ℤ np dq))
+  ＝ diff-ℤ
+      (dq *ℤ (nr *ℤ dp) +ℤ dr *ℤ (nq *ℤ dp))
+      (dr *ℤ (nq *ℤ dp) +ℤ dq *ℤ (np *ℤ dr))
+    by
+      ap-diff-ℤ
+        ( ap-add-ℤ
+          ( lemma-interchange-mul-ℤ dp nr dq)
+          ( refl))
+        ( ap-add-ℤ
+          ( lemma-interchange-mul-ℤ dp nq dr)
+          ( lemma-interchange-mul-ℤ dr np dq))
+  ＝ diff-ℤ
+      (dq *ℤ (nr *ℤ dp) +ℤ dr *ℤ (nq *ℤ dp))
+      ((dq *ℤ (np *ℤ dr)) +ℤ (dr *ℤ (nq *ℤ dp)))
+    by
+      ap
+        ( diff-ℤ (dq *ℤ (nr *ℤ dp) +ℤ dr *ℤ (nq *ℤ dp)))
+        ( commutative-add-ℤ (dr *ℤ (nq *ℤ dp)) (dq *ℤ (np *ℤ dr)))
+  ＝ (dq *ℤ (nr *ℤ dp)) -ℤ (dq *ℤ (np *ℤ dr))
+    by
+      right-translation-diff-ℤ
+        (dq *ℤ (nr *ℤ dp))
+        (dq *ℤ (np *ℤ dr))
+        (dr *ℤ (nq *ℤ dp))
+  ＝ dq *ℤ (nr *ℤ dp -ℤ np *ℤ dr)
+    by linear-diff-left-mul-ℤ dq (nr *ℤ dp) (np *ℤ dr)
+  where
+  lemma-interchange-mul-ℤ : (a b c : ℤ) → (a *ℤ (b *ℤ c)) ＝ (c *ℤ (b *ℤ a))
+  lemma-interchange-mul-ℤ a b c =
+    inv (associative-mul-ℤ a b c) ∙
+    ap (mul-ℤ' c) (commutative-mul-ℤ a b) ∙
+    commutative-mul-ℤ (b *ℤ a) c
+
+lemma-left-sim-cross-mul-diff-fraction-ℤ :
+  (a a' b : fraction-ℤ) →
+  sim-fraction-ℤ a a' →
+  Id
+    ( denominator-fraction-ℤ a *ℤ cross-mul-diff-fraction-ℤ a' b)
+    ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b)
+lemma-left-sim-cross-mul-diff-fraction-ℤ a a' b H =
+  equational-reasoning
+  ( denominator-fraction-ℤ a *ℤ cross-mul-diff-fraction-ℤ a' b)
+  ＝ ( add-ℤ
+        ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b)
+        ( denominator-fraction-ℤ b *ℤ cross-mul-diff-fraction-ℤ a' a))
+    by inv (lemma-add-cross-mul-diff-fraction-ℤ a' a b)
+  ＝ ( add-ℤ
+      ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b)
+      ( zero-ℤ))
+    by
+      ap
+        ( add-ℤ
+          ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b))
+          ( ( ap
+              ( mul-ℤ (denominator-fraction-ℤ b))
+              ( is-zero-cross-mul-diff-sim-fraction-ℤ a' a H')) ∙
+            ( right-zero-law-mul-ℤ (denominator-fraction-ℤ b)))
+  ＝ denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b
+    by
+      right-unit-law-add-ℤ
+        ( denominator-fraction-ℤ a' *ℤ cross-mul-diff-fraction-ℤ a b)
+  where
+  H' : sim-fraction-ℤ a' a
+  H' = symmetric-sim-fraction-ℤ a a' H
+
+lemma-right-sim-cross-mul-diff-fraction-ℤ :
+  (a b b' : fraction-ℤ) →
+  sim-fraction-ℤ b b' →
+  Id
+    ( denominator-fraction-ℤ b *ℤ cross-mul-diff-fraction-ℤ a b')
+    ( denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b)
+lemma-right-sim-cross-mul-diff-fraction-ℤ a b b' H =
+  equational-reasoning
+  ( denominator-fraction-ℤ b *ℤ cross-mul-diff-fraction-ℤ a b')
+  ＝ ( add-ℤ
+      ( denominator-fraction-ℤ a *ℤ cross-mul-diff-fraction-ℤ b b')
+      ( denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b))
+    by inv (lemma-add-cross-mul-diff-fraction-ℤ a b b')
+  ＝ ( add-ℤ
+      ( zero-ℤ)
+      ( denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b))
+    by
+      ap
+        ( add-ℤ' (denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b))
+        ( ( ap
+          ( mul-ℤ (denominator-fraction-ℤ a))
+          ( is-zero-cross-mul-diff-sim-fraction-ℤ b b' H)) ∙
+          ( right-zero-law-mul-ℤ (denominator-fraction-ℤ a)))
+  ＝ denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b
+    by
+      left-unit-law-add-ℤ
+        ( denominator-fraction-ℤ b' *ℤ cross-mul-diff-fraction-ℤ a b)
+```
+
+## External links
+
+- [Cross-multiplication](https://en.wikipedia.org/wiki/Cross-multiplication) at
+  Wikipedia
diff --git a/src/elementary-number-theory/inequality-integer-fractions.lagda.md b/src/elementary-number-theory/inequality-integer-fractions.lagda.md
index 9515686192..72408db7b4 100644
--- a/src/elementary-number-theory/inequality-integer-fractions.lagda.md
+++ b/src/elementary-number-theory/inequality-integer-fractions.lagda.md
@@ -7,12 +7,24 @@ module elementary-number-theory.inequality-integer-fractions where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.addition-integers
+open import elementary-number-theory.cross-multiplication-difference-integer-fractions
+open import elementary-number-theory.difference-integers
 open import elementary-number-theory.inequality-integers
 open import elementary-number-theory.integer-fractions
+open import elementary-number-theory.integers
+open import elementary-number-theory.mediant-integer-fractions
 open import elementary-number-theory.multiplication-integers
 
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.coproduct-types
 open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.negation
 open import foundation.propositions
+open import foundation.transport-along-identifications
 open import foundation.universe-levels
 ```
 
@@ -52,3 +64,212 @@ le-fraction-ℤ x y = type-Prop (le-fraction-ℤ-Prop x y)
 is-prop-le-fraction-ℤ : (x y : fraction-ℤ) → is-prop (le-fraction-ℤ x y)
 is-prop-le-fraction-ℤ x y = is-prop-type-Prop (le-fraction-ℤ-Prop x y)
 ```
+
+## Properties
+
+### Inequality on integer fractions is antisymmetric with respect to the similarity relation
+
+```agda
+module _
+  (x y : fraction-ℤ)
+  where
+
+  is-sim-antisymmetric-leq-fraction-ℤ :
+    leq-fraction-ℤ x y →
+    leq-fraction-ℤ y x →
+    sim-fraction-ℤ x y
+  is-sim-antisymmetric-leq-fraction-ℤ H H' =
+    sim-is-zero-coss-mul-diff-fraction-ℤ x y
+      ( is-zero-is-nonnegative-ℤ
+        ( H)
+        ( is-nonnegative-eq-ℤ
+            ( inv ( skew-commutative-cross-mul-diff-fraction-ℤ x y))
+            ( H')))
+```
+
+### Strict inequality on integer fractions is asymmetric
+
+```agda
+module _
+  (x y : fraction-ℤ)
+  where
+
+  asymmetric-le-fraction-ℤ :
+    le-fraction-ℤ x y → ¬ (le-fraction-ℤ y x)
+  asymmetric-le-fraction-ℤ =
+    asymmetric-le-ℤ
+      ( mul-ℤ
+        ( numerator-fraction-ℤ x)
+        ( denominator-fraction-ℤ y))
+      ( mul-ℤ
+        ( numerator-fraction-ℤ y)
+        ( denominator-fraction-ℤ x))
+```
+
+### Inequality on integer fractions is transitive
+
+```agda
+transitive-leq-fraction-ℤ :
+  (p q r : fraction-ℤ) →
+  leq-fraction-ℤ p q →
+  leq-fraction-ℤ q r →
+  leq-fraction-ℤ p r
+transitive-leq-fraction-ℤ p q r H H' =
+  is-nonnegative-right-factor-mul-ℤ
+    ( is-nonnegative-eq-ℤ
+      ( lemma-add-cross-mul-diff-fraction-ℤ p q r)
+        (is-nonnegative-add-ℤ
+          ( denominator-fraction-ℤ p *ℤ cross-mul-diff-fraction-ℤ q r)
+          ( denominator-fraction-ℤ r *ℤ cross-mul-diff-fraction-ℤ p q)
+          ( is-nonnegative-mul-ℤ
+            ( is-nonnegative-is-positive-ℤ
+              ( is-positive-denominator-fraction-ℤ p))
+            ( H'))
+          ( is-nonnegative-mul-ℤ
+            ( is-nonnegative-is-positive-ℤ
+              ( is-positive-denominator-fraction-ℤ r))
+            ( H))))
+    ( is-positive-denominator-fraction-ℤ q)
+```
+
+### Strict inequality on integer fractions is transitive
+
+```agda
+transitive-le-fraction-ℤ :
+  (p q r : fraction-ℤ) →
+  le-fraction-ℤ p q →
+  le-fraction-ℤ q r →
+  le-fraction-ℤ p r
+transitive-le-fraction-ℤ p q r H H' =
+  is-positive-right-factor-mul-ℤ
+    ( is-positive-eq-ℤ
+      ( lemma-add-cross-mul-diff-fraction-ℤ p q r)
+      ( is-positive-add-ℤ
+        ( is-positive-mul-ℤ
+          ( is-positive-denominator-fraction-ℤ p)
+          ( H'))
+        ( is-positive-mul-ℤ
+          ( is-positive-denominator-fraction-ℤ r)
+          ( H))))
+      ( is-positive-denominator-fraction-ℤ q)
+```
+
+### Chaining rules for inequality and strict inequality on integer fractions
+
+```agda
+module _
+  (p q r : fraction-ℤ)
+  where
+
+  concatenate-le-leq-fraction-ℤ :
+    le-fraction-ℤ p q →
+    leq-fraction-ℤ q r →
+    le-fraction-ℤ p r
+  concatenate-le-leq-fraction-ℤ H H' =
+    is-positive-right-factor-mul-ℤ
+      ( is-positive-eq-ℤ
+        ( lemma-add-cross-mul-diff-fraction-ℤ p q r)
+        ( is-positive-add-nonnegative-positive-ℤ
+          ( is-nonnegative-mul-ℤ
+            ( is-nonnegative-is-positive-ℤ
+              ( is-positive-denominator-fraction-ℤ p))
+            ( H'))
+          ( is-positive-mul-ℤ
+            ( is-positive-denominator-fraction-ℤ r)
+            ( H))))
+      ( is-positive-denominator-fraction-ℤ q)
+
+  concatenate-leq-le-fraction-ℤ :
+    leq-fraction-ℤ p q →
+    le-fraction-ℤ q r →
+    le-fraction-ℤ p r
+  concatenate-leq-le-fraction-ℤ H H' =
+    is-positive-right-factor-mul-ℤ
+      ( is-positive-eq-ℤ
+        ( lemma-add-cross-mul-diff-fraction-ℤ p q r)
+        ( is-positive-add-positive-nonnegative-ℤ
+          ( is-positive-mul-ℤ
+            ( is-positive-denominator-fraction-ℤ p)
+            ( H'))
+          ( is-nonnegative-mul-ℤ
+            ( is-nonnegative-is-positive-ℤ
+              ( is-positive-denominator-fraction-ℤ r))
+            ( H))))
+      ( is-positive-denominator-fraction-ℤ q)
+```
+
+### Chaining rules for similarity and strict inequality on integer fractions
+
+```agda
+module _
+  (p q r : fraction-ℤ)
+  where
+
+  concatenate-sim-le-fraction-ℤ :
+    sim-fraction-ℤ p q →
+    le-fraction-ℤ q r →
+    le-fraction-ℤ p r
+  concatenate-sim-le-fraction-ℤ H H' =
+    is-positive-right-factor-mul-ℤ
+      ( is-positive-eq-ℤ
+        ( lemma-left-sim-cross-mul-diff-fraction-ℤ p q r H)
+        ( is-positive-mul-ℤ
+          ( is-positive-denominator-fraction-ℤ p) H'))
+      ( is-positive-denominator-fraction-ℤ q)
+
+  concatenate-le-sim-fraction-ℤ :
+    le-fraction-ℤ p q →
+    sim-fraction-ℤ q r →
+    le-fraction-ℤ p r
+  concatenate-le-sim-fraction-ℤ H H' =
+    is-positive-right-factor-mul-ℤ
+      ( is-positive-eq-ℤ
+        ( inv ( lemma-right-sim-cross-mul-diff-fraction-ℤ p q r H'))
+        ( is-positive-mul-ℤ (is-positive-denominator-fraction-ℤ r) H))
+      ( is-positive-denominator-fraction-ℤ q)
+```
+
+### Fractions with equal denominator compare the same as their numerators
+
+```agda
+module _
+  (x y : fraction-ℤ) (H : denominator-fraction-ℤ x ＝ denominator-fraction-ℤ y)
+  where
+
+  le-fraction-le-numerator-fraction-ℤ :
+    le-ℤ (numerator-fraction-ℤ x) (numerator-fraction-ℤ y) →
+    le-fraction-ℤ x y
+  le-fraction-le-numerator-fraction-ℤ H' =
+    tr
+      ( λ (k : ℤ) →
+        le-ℤ
+          ( numerator-fraction-ℤ x *ℤ k)
+          ( numerator-fraction-ℤ y *ℤ denominator-fraction-ℤ x))
+      ( H)
+      ( preserves-strict-order-mul-positive-ℤ'
+        { numerator-fraction-ℤ x}
+        { numerator-fraction-ℤ y}
+        ( denominator-fraction-ℤ x)
+        ( is-positive-denominator-fraction-ℤ x)
+        ( H'))
+```
+
+### The mediant of two fractions is between them
+
+```agda
+module _
+  (x y : fraction-ℤ)
+  where
+
+  le-left-mediant-fraction-ℤ :
+    le-fraction-ℤ x y →
+    le-fraction-ℤ x (mediant-fraction-ℤ x y)
+  le-left-mediant-fraction-ℤ =
+    is-positive-eq-ℤ (cross-mul-diff-left-mediant-fraction-ℤ x y)
+
+  le-right-mediant-fraction-ℤ :
+    le-fraction-ℤ x y →
+    le-fraction-ℤ (mediant-fraction-ℤ x y) y
+  le-right-mediant-fraction-ℤ =
+    is-positive-eq-ℤ (cross-mul-diff-right-mediant-fraction-ℤ x y)
+```
diff --git a/src/elementary-number-theory/inequality-integers.lagda.md b/src/elementary-number-theory/inequality-integers.lagda.md
index 84668302c9..3eb990d983 100644
--- a/src/elementary-number-theory/inequality-integers.lagda.md
+++ b/src/elementary-number-theory/inequality-integers.lagda.md
@@ -18,6 +18,8 @@ open import foundation.coproduct-types
 open import foundation.function-types
 open import foundation.functoriality-coproduct-types
 open import foundation.identity-types
+open import foundation.negated-equality
+open import foundation.negation
 open import foundation.propositions
 open import foundation.transport-along-identifications
 open import foundation.unit-type
@@ -100,7 +102,7 @@ concatenate-eq-leq-ℤ y refl H = H
 
 ```agda
 le-ℤ-Prop : ℤ → ℤ → Prop lzero
-le-ℤ-Prop x y = is-positive-ℤ-Prop (x -ℤ y)
+le-ℤ-Prop x y = is-positive-ℤ-Prop (y -ℤ x)
 
 le-ℤ : ℤ → ℤ → UU lzero
 le-ℤ x y = type-Prop (le-ℤ-Prop x y)
@@ -109,6 +111,47 @@ is-prop-le-ℤ : (x y : ℤ) → is-prop (le-ℤ x y)
 is-prop-le-ℤ x y = is-prop-type-Prop (le-ℤ-Prop x y)
 ```
 
+## Properties
+
+```agda
+transitive-le-ℤ : (k l m : ℤ) → le-ℤ k l → le-ℤ l m → le-ℤ k m
+transitive-le-ℤ k l m p q =
+  tr is-positive-ℤ
+    ( triangle-diff-ℤ m l k)
+    ( is-positive-add-ℤ q p)
+
+asymmetric-le-ℤ : (x y : ℤ) → le-ℤ x y → ¬ (le-ℤ y x)
+asymmetric-le-ℤ x y p q =
+  not-is-nonpositive-is-positive-ℤ
+    ( y -ℤ x)
+    ( p)
+    ( is-nonnegative-is-positive-ℤ
+      ( is-positive-eq-ℤ
+        ( inv ( distributive-neg-diff-ℤ y x))
+        ( q)))
+
+connected-le-ℤ : (x y : ℤ) → x ≠ y → le-ℤ x y + le-ℤ y x
+connected-le-ℤ x y H =
+  map-coproduct
+    ( id)
+    ( is-positive-eq-ℤ ( distributive-neg-diff-ℤ y x))
+    ( decide-is-positive-is-nonzero-ℤ (y -ℤ x) (H ∘ inv ∘ eq-diff-ℤ))
+
+le-pred-ℤ : (x : ℤ) → le-ℤ (pred-ℤ x) x
+le-pred-ℤ x =
+  is-positive-eq-ℤ
+    ( inv
+      ( right-predecessor-law-diff-ℤ x x ∙ ap succ-ℤ (is-zero-diff-ℤ' x)))
+    ( is-positive-one-ℤ)
+
+le-succ-ℤ : (x : ℤ) → le-ℤ x (succ-ℤ x)
+le-succ-ℤ x =
+  is-positive-eq-ℤ
+    ( inv
+      ( left-successor-law-diff-ℤ x x ∙ ap succ-ℤ (is-zero-diff-ℤ' x)))
+    ( is-positive-one-ℤ)
+```
+
 ### ℤ is an ordered ring
 
 ```agda
@@ -143,6 +186,40 @@ reflects-order-add-ℤ {x} {y} {z} =
   is-nonnegative-eq-ℤ (left-translation-diff-ℤ y x z)
 ```
 
+### Addition on the integers preserves and reflects the strict ordering
+
+```agda
+preserves-strict-order-add-ℤ' :
+  {x y : ℤ} (z : ℤ) → le-ℤ x y → le-ℤ (x +ℤ z) (y +ℤ z)
+preserves-strict-order-add-ℤ' {x} {y} z =
+  is-positive-eq-ℤ (inv (right-translation-diff-ℤ y x z))
+
+preserves-strict-order-add-ℤ :
+  {x y : ℤ} (z : ℤ) → le-ℤ x y → le-ℤ (z +ℤ x) (z +ℤ y)
+preserves-strict-order-add-ℤ {x} {y} z =
+  is-positive-eq-ℤ (inv (left-translation-diff-ℤ y x z))
+
+preserves-le-add-ℤ :
+  {a b c d : ℤ} → le-ℤ a b → le-ℤ c d → le-ℤ (a +ℤ c) (b +ℤ d)
+preserves-le-add-ℤ {a} {b} {c} {d} H K =
+  transitive-le-ℤ
+    ( a +ℤ c)
+    ( b +ℤ c)
+    ( b +ℤ d)
+    ( preserves-strict-order-add-ℤ' {a} {b} c H)
+    ( preserves-strict-order-add-ℤ b K)
+
+reflects-strict-order-add-ℤ' :
+  {x y z : ℤ} → le-ℤ (x +ℤ z) (y +ℤ z) → le-ℤ x y
+reflects-strict-order-add-ℤ' {x} {y} {z} =
+  is-positive-eq-ℤ (right-translation-diff-ℤ y x z)
+
+reflects-strict-order-add-ℤ :
+  {x y z : ℤ} → le-ℤ (z +ℤ x) (z +ℤ y) → le-ℤ x y
+reflects-strict-order-add-ℤ {x} {y} {z} =
+  is-positive-eq-ℤ (left-translation-diff-ℤ y x z)
+```
+
 ### Inclusion of ℕ into ℤ preserves order
 
 ```agda
diff --git a/src/elementary-number-theory/inequality-rational-numbers.lagda.md b/src/elementary-number-theory/inequality-rational-numbers.lagda.md
index aa52e54c68..12c55dad2c 100644
--- a/src/elementary-number-theory/inequality-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/inequality-rational-numbers.lagda.md
@@ -7,10 +7,27 @@ module elementary-number-theory.inequality-rational-numbers where
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.cross-multiplication-difference-integer-fractions
 open import elementary-number-theory.inequality-integer-fractions
+open import elementary-number-theory.inequality-integers
+open import elementary-number-theory.integer-fractions
+open import elementary-number-theory.integers
+open import elementary-number-theory.mediant-integer-fractions
+open import elementary-number-theory.multiplication-integers
 open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.reduced-integer-fractions
 
+open import foundation.binary-relations
+open import foundation.cartesian-product-types
+open import foundation.coproduct-types
 open import foundation.dependent-pair-types
+open import foundation.disjunction
+open import foundation.existential-quantification
+open import foundation.function-types
+open import foundation.functoriality-coproduct-types
+open import foundation.identity-types
+open import foundation.negation
+open import foundation.propositional-truncations
 open import foundation.propositions
 open import foundation.universe-levels
 ```
@@ -53,3 +70,226 @@ le-ℚ x y = type-Prop (le-ℚ-Prop x y)
 is-prop-le-ℚ : (x y : ℚ) → is-prop (le-ℚ x y)
 is-prop-le-ℚ x y = is-prop-type-Prop (le-ℚ-Prop x y)
 ```
+
+## Properties
+
+### Inequality on rational numbers is reflexive
+
+```agda
+refl-leq-ℚ : (x : ℚ) → leq-ℚ x x
+refl-leq-ℚ x =
+  refl-leq-ℤ (numerator-ℚ x *ℤ denominator-ℚ x)
+```
+
+### Inequality on rational numbers is antisymmetric
+
+```agda
+antisymmetric-leq-ℚ : (x y : ℚ) → leq-ℚ x y → leq-ℚ y x → x ＝ y
+antisymmetric-leq-ℚ x y H H' =
+  ( inv (in-fraction-fraction-ℚ x)) ∙
+  ( eq-ℚ-sim-fractions-ℤ
+    ( fraction-ℚ x)
+    ( fraction-ℚ y)
+    ( is-sim-antisymmetric-leq-fraction-ℤ
+      ( fraction-ℚ x)
+      ( fraction-ℚ y)
+      ( H)
+      ( H'))) ∙
+  ( in-fraction-fraction-ℚ y)
+```
+
+### Strict inequality on rationals is asymmetric
+
+```agda
+asymmetric-le-ℚ : (x y : ℚ) → le-ℚ x y → ¬ (le-ℚ y x)
+asymmetric-le-ℚ x y =
+  asymmetric-le-fraction-ℤ
+    ( fraction-ℚ x)
+    ( fraction-ℚ y)
+
+irreflexive-le-ℚ : (x : ℚ) → ¬ (le-ℚ x x)
+irreflexive-le-ℚ =
+  is-irreflexive-is-asymmetric le-ℚ asymmetric-le-ℚ
+```
+
+### Transitivity properties
+
+```agda
+module _
+  (x y z : ℚ)
+  where
+
+  transitive-leq-ℚ : leq-ℚ x y → leq-ℚ y z → leq-ℚ x z
+  transitive-leq-ℚ =
+    transitive-leq-fraction-ℤ
+      ( fraction-ℚ x)
+      ( fraction-ℚ y)
+      ( fraction-ℚ z)
+
+  transitive-le-ℚ : le-ℚ x y → le-ℚ y z → le-ℚ x z
+  transitive-le-ℚ =
+    transitive-le-fraction-ℤ
+      ( fraction-ℚ x)
+      ( fraction-ℚ y)
+      ( fraction-ℚ z)
+
+  concatenate-le-leq-ℚ : le-ℚ x y → leq-ℚ y z → le-ℚ x z
+  concatenate-le-leq-ℚ =
+    concatenate-le-leq-fraction-ℤ
+      ( fraction-ℚ x)
+      ( fraction-ℚ y)
+      ( fraction-ℚ z)
+
+  concatenate-leq-le-ℚ : leq-ℚ x y → le-ℚ y z → le-ℚ x z
+  concatenate-leq-le-ℚ =
+    concatenate-leq-le-fraction-ℤ
+      ( fraction-ℚ x)
+      ( fraction-ℚ y)
+      ( fraction-ℚ z)
+```
+
+### Strict inequality on the rational numbers reflects strict inequality on the underlying fractions
+
+```agda
+module _
+  (x : ℚ) (p : fraction-ℤ)
+  where
+
+  right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ :
+    le-fraction-ℤ (fraction-ℚ x) p →
+    le-ℚ x (in-fraction-ℤ p)
+  right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ H =
+    concatenate-le-sim-fraction-ℤ
+      ( fraction-ℚ x)
+      ( p)
+      ( fraction-ℚ ( in-fraction-ℤ p))
+      ( H)
+      ( sim-reduced-fraction-ℤ p)
+
+  left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ :
+    le-fraction-ℤ p (fraction-ℚ x) →
+    le-ℚ (in-fraction-ℤ p) x
+  left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ =
+    concatenate-sim-le-fraction-ℤ
+      ( fraction-ℚ ( in-fraction-ℤ p))
+      ( p)
+      ( fraction-ℚ x)
+      ( symmetric-sim-fraction-ℤ
+        ( p)
+        ( fraction-ℚ ( in-fraction-ℤ p))
+        ( sim-reduced-fraction-ℤ p))
+```
+
+### The rational numbers have no lower or upper bound
+
+```agda
+module _
+  (x : ℚ)
+  where
+
+  left-∃-le-ℚ : ∃ ℚ (λ q → le-ℚ q x)
+  left-∃-le-ℚ = intro-∃
+    ( in-fraction-ℤ frac)
+    ( left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x frac
+      ( le-fraction-le-numerator-fraction-ℤ
+        ( frac)
+        ( fraction-ℚ x)
+        ( refl)
+        ( le-pred-ℤ (numerator-ℚ x))))
+    where
+    frac : fraction-ℤ
+    frac = pred-ℤ (numerator-ℚ x) , positive-denominator-ℚ x
+
+  right-∃-le-ℚ : ∃ ℚ (λ r → le-ℚ x r)
+  right-∃-le-ℚ = intro-∃
+    ( in-fraction-ℤ frac)
+    ( right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x frac
+      ( le-fraction-le-numerator-fraction-ℤ
+        ( fraction-ℚ x)
+        ( frac)
+        ( refl)
+        ( le-succ-ℤ (numerator-ℚ x))))
+    where
+    frac : fraction-ℤ
+    frac = succ-ℤ (numerator-ℚ x) , positive-denominator-ℚ x
+```
+
+### Decidability of strict inequality on the rationals
+
+```agda
+decide-le-leq-ℚ : (x y : ℚ) → le-ℚ x y + leq-ℚ y x
+decide-le-leq-ℚ x y =
+  map-coproduct
+    ( id)
+    ( is-nonnegative-eq-ℤ
+      ( skew-commutative-cross-mul-diff-fraction-ℤ
+        ( fraction-ℚ x)
+        ( fraction-ℚ y)))
+    ( decide-is-positive-ℤ
+      { cross-mul-diff-fraction-ℤ
+        ( fraction-ℚ x)
+        ( fraction-ℚ y)})
+```
+
+It remains to fully formalize that strict inequality is decidable.
+
+### Trichotomy on the rationals
+
+```agda
+trichotomy-le-ℚ :
+  {l : Level} {A : UU l} (x y : ℚ) →
+  ( le-ℚ x y → A) →
+  ( Id x y → A) →
+  ( le-ℚ y x → A) →
+  A
+trichotomy-le-ℚ x y left eq right with decide-le-leq-ℚ x y | decide-le-leq-ℚ y x
+... | inl I | _ = left I
+... | inr I | inl I' = right I'
+... | inr I | inr I' = eq (antisymmetric-leq-ℚ x y I' I)
+```
+
+### The mediant of two rationals is between them
+
+```agda
+module _
+  (x y : ℚ) (H : le-ℚ x y)
+  where
+
+  le-left-mediant-ℚ : le-ℚ x (mediant-ℚ x y)
+  le-left-mediant-ℚ =
+    right-le-ℚ-in-fraction-ℤ-le-fraction-ℤ x
+      ( mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y))
+      ( le-left-mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H)
+
+  le-right-mediant-ℚ : le-ℚ (mediant-ℚ x y) y
+  le-right-mediant-ℚ =
+    left-le-ℚ-in-fraction-ℤ-le-fraction-ℤ y
+      ( mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y))
+      ( le-right-mediant-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y) H)
+```
+
+### Strict inequality on the rationals is dense
+
+```agda
+module _
+  (x y : ℚ) (H : le-ℚ x y)
+  where
+
+  dense-le-ℚ : ∃ ℚ (λ r → le-ℚ x r × le-ℚ r y)
+  dense-le-ℚ =
+    intro-∃
+      ( mediant-ℚ x y)
+      ( le-left-mediant-ℚ x y H , le-right-mediant-ℚ x y H)
+```
+
+### The strict order on the rationals is located
+
+```agda
+located-le-ℚ : (x y z : ℚ) → le-ℚ y z → (le-ℚ-Prop y x) ∨ (le-ℚ-Prop x z)
+located-le-ℚ x y z H =
+  unit-trunc-Prop
+    ( map-coproduct
+      ( id)
+      ( λ p → concatenate-leq-le-ℚ x y z p H)
+      ( decide-le-leq-ℚ y x))
+```
diff --git a/src/elementary-number-theory/integers.lagda.md b/src/elementary-number-theory/integers.lagda.md
index 853f8a3981..9c8b2a6150 100644
--- a/src/elementary-number-theory/integers.lagda.md
+++ b/src/elementary-number-theory/integers.lagda.md
@@ -22,6 +22,7 @@ open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.injective-maps
 open import foundation.negated-equality
+open import foundation.negation
 open import foundation.propositions
 open import foundation.retractions
 open import foundation.sections
@@ -426,16 +427,71 @@ is-zero-is-nonnegative-neg-is-nonnegative-ℤ (inr (inl star)) nonneg nonpos =
   refl
 ```
 
+### Properties of positive integers
+
+#### The positivity predicate on integers is decidable
+
+```agda
+decide-is-positive-ℤ : {x : ℤ} → (is-positive-ℤ x) + is-nonnegative-ℤ (neg-ℤ x)
+decide-is-positive-ℤ {inl x} = inr star
+decide-is-positive-ℤ {inr (inl x)} = inr star
+decide-is-positive-ℤ {inr (inr x)} = inl star
+
+decide-is-positive-is-nonzero-ℤ :
+  (x : ℤ) → (x ≠ zero-ℤ) →
+  (is-positive-ℤ x) + is-positive-ℤ (neg-ℤ x)
+decide-is-positive-is-nonzero-ℤ (inl x) H = inr star
+decide-is-positive-is-nonzero-ℤ (inr (inl x)) H = ex-falso (H refl)
+decide-is-positive-is-nonzero-ℤ (inr (inr x)) H = inl star
+```
+
+This remains to be fully formalized.
+
+### The nonpositive integers
+
+```agda
+is-nonpositive-ℤ : ℤ → UU lzero
+is-nonpositive-ℤ x = is-nonnegative-ℤ (neg-ℤ x)
+```
+
+#### Positive integers are not nonpositive
+
+```agda
+not-is-nonpositive-is-positive-ℤ :
+  (x : ℤ) → is-positive-ℤ x → ¬ (is-nonpositive-ℤ x)
+not-is-nonpositive-is-positive-ℤ (inr (inl x)) x-is-pos _ = x-is-pos
+not-is-nonpositive-is-positive-ℤ (inr (inr x)) x-is-pos neg-x-is-nonneg =
+  neg-x-is-nonneg
+```
+
+#### An integer that is not positive is nonpositive
+
+```agda
+is-nonpositive-not-is-positive-ℤ :
+  (x : ℤ) → ¬ (is-positive-ℤ x) → is-nonpositive-ℤ x
+is-nonpositive-not-is-positive-ℤ x H with decide-is-positive-ℤ {x}
+... | inl K = ex-falso (H K)
+... | inr K = K
+```
+
+#### Relation between successors of natural numbers and integers
+
 ```agda
 succ-int-ℕ : (x : ℕ) → succ-ℤ (int-ℕ x) ＝ int-ℕ (succ-ℕ x)
 succ-int-ℕ zero-ℕ = refl
 succ-int-ℕ (succ-ℕ x) = refl
 ```
 
+#### The negative function is injective
+
 ```agda
 is-injective-neg-ℤ : is-injective neg-ℤ
 is-injective-neg-ℤ {x} {y} p = inv (neg-neg-ℤ x) ∙ ap neg-ℤ p ∙ neg-neg-ℤ y
+```
 
+#### An integer is zero if its negative is zero
+
+```agda
 is-zero-is-zero-neg-ℤ : (x : ℤ) → is-zero-ℤ (neg-ℤ x) → is-zero-ℤ x
 is-zero-is-zero-neg-ℤ (inr (inl star)) H = refl
 ```
diff --git a/src/elementary-number-theory/mediant-integer-fractions.lagda.md b/src/elementary-number-theory/mediant-integer-fractions.lagda.md
new file mode 100644
index 0000000000..56ee67d080
--- /dev/null
+++ b/src/elementary-number-theory/mediant-integer-fractions.lagda.md
@@ -0,0 +1,86 @@
+# The mediant fraction of two integer fractions
+
+```agda
+module elementary-number-theory.mediant-integer-fractions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-integers
+open import elementary-number-theory.cross-multiplication-difference-integer-fractions
+open import elementary-number-theory.difference-integers
+open import elementary-number-theory.integer-fractions
+open import elementary-number-theory.multiplication-integers
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "mediant" Disambiguation="integer fractions" Agda=mediant-fraction-ℤ}}
+of two fractions is the quotient of the sum of the numerators by the sum of the
+denominators.
+
+## Definitions
+
+### The mediant of two fractions
+
+```agda
+mediant-fraction-ℤ : fraction-ℤ → fraction-ℤ → fraction-ℤ
+mediant-fraction-ℤ (a , b , p) (c , d , q) =
+  (a +ℤ c , b +ℤ d , is-positive-add-ℤ p q)
+```
+
+## Properties
+
+### The mediant preserves the cross-multiplication difference
+
+```agda
+cross-mul-diff-left-mediant-fraction-ℤ :
+  (x y : fraction-ℤ) →
+  Id
+    ( cross-mul-diff-fraction-ℤ x y)
+    ( cross-mul-diff-fraction-ℤ x ( mediant-fraction-ℤ x y))
+cross-mul-diff-left-mediant-fraction-ℤ (nx , dx , px) (ny , dy , py) =
+  equational-reasoning
+  (ny *ℤ dx -ℤ nx *ℤ dy)
+  ＝ (nx *ℤ dx +ℤ ny *ℤ dx) -ℤ (nx *ℤ dx +ℤ nx *ℤ dy)
+    by inv
+      ( left-translation-diff-ℤ
+        ( mul-ℤ ny dx)
+        ( mul-ℤ nx dy)
+        ( mul-ℤ nx dx))
+  ＝ (nx +ℤ ny) *ℤ dx -ℤ nx *ℤ (dx +ℤ dy)
+    by ap-diff-ℤ
+      ( inv (right-distributive-mul-add-ℤ nx ny dx))
+      ( inv (left-distributive-mul-add-ℤ nx dx dy))
+
+cross-mul-diff-right-mediant-fraction-ℤ :
+  (x y : fraction-ℤ) →
+  Id
+    ( cross-mul-diff-fraction-ℤ x y)
+    ( cross-mul-diff-fraction-ℤ (mediant-fraction-ℤ x y) y)
+cross-mul-diff-right-mediant-fraction-ℤ (nx , dx , px) (ny , dy , py) =
+  equational-reasoning
+  (ny *ℤ dx -ℤ nx *ℤ dy)
+  ＝ (ny *ℤ dx +ℤ ny *ℤ dy) -ℤ (nx *ℤ dy +ℤ ny *ℤ dy)
+    by inv
+      ( right-translation-diff-ℤ
+        ( mul-ℤ ny dx)
+        ( mul-ℤ nx dy)
+        ( mul-ℤ ny dy))
+  ＝ ny *ℤ (dx +ℤ dy) -ℤ (nx +ℤ ny) *ℤ dy
+    by ap-diff-ℤ
+      ( inv (left-distributive-mul-add-ℤ ny dx dy))
+      ( inv (right-distributive-mul-add-ℤ nx ny dy))
+```
+
+## External links
+
+- [Mediant fraction](<https://en.wikipedia.org/wiki/Mediant_(mathematics)>) at
+  Wikipedia
diff --git a/src/elementary-number-theory/multiplication-integers.lagda.md b/src/elementary-number-theory/multiplication-integers.lagda.md
index b0b1f81d70..e9b7690aa8 100644
--- a/src/elementary-number-theory/multiplication-integers.lagda.md
+++ b/src/elementary-number-theory/multiplication-integers.lagda.md
@@ -536,4 +536,18 @@ preserves-leq-right-mul-ℤ x y z H K =
     ( commutative-mul-ℤ x z)
     ( preserves-leq-left-mul-ℤ x y z H K)
     ( commutative-mul-ℤ z y)
+
+preserves-strict-order-mul-positive-ℤ' :
+  {x y : ℤ} (z : ℤ) → is-positive-ℤ z → le-ℤ x y → le-ℤ (x *ℤ z) (y *ℤ z)
+preserves-strict-order-mul-positive-ℤ' {x} {y} z H p =
+  is-positive-eq-ℤ
+    ( inv ( linear-diff-right-mul-ℤ y x z))
+    ( is-positive-mul-ℤ p H)
+
+preserves-strict-order-mul-positive-ℤ :
+  {x y : ℤ} (z : ℤ) → is-positive-ℤ z → le-ℤ x y → le-ℤ (z *ℤ x) (z *ℤ y)
+preserves-strict-order-mul-positive-ℤ {x} {y} z H p =
+  is-positive-eq-ℤ
+    ( inv ( linear-diff-left-mul-ℤ z y x))
+    ( is-positive-mul-ℤ H p)
 ```
diff --git a/src/elementary-number-theory/rational-numbers.lagda.md b/src/elementary-number-theory/rational-numbers.lagda.md
index 00c52582bc..b04a7d7592 100644
--- a/src/elementary-number-theory/rational-numbers.lagda.md
+++ b/src/elementary-number-theory/rational-numbers.lagda.md
@@ -11,6 +11,7 @@ open import elementary-number-theory.divisibility-integers
 open import elementary-number-theory.greatest-common-divisor-integers
 open import elementary-number-theory.integer-fractions
 open import elementary-number-theory.integers
+open import elementary-number-theory.mediant-integer-fractions
 open import elementary-number-theory.reduced-integer-fractions
 
 open import foundation.dependent-pair-types
@@ -39,11 +40,27 @@ equivalence relation given by `(n/m) ~ (n'/m') := Id (n *ℤ m') (n' *ℤ m)`.
 ℚ : UU lzero
 ℚ = Σ fraction-ℤ is-reduced-fraction-ℤ
 
-fraction-ℚ : ℚ → fraction-ℤ
-fraction-ℚ x = pr1 x
+module _
+  (x : ℚ)
+  where
 
-is-reduced-fraction-ℚ : (x : ℚ) → is-reduced-fraction-ℤ (fraction-ℚ x)
-is-reduced-fraction-ℚ x = pr2 x
+  fraction-ℚ : fraction-ℤ
+  fraction-ℚ = pr1 x
+
+  is-reduced-fraction-ℚ : is-reduced-fraction-ℤ fraction-ℚ
+  is-reduced-fraction-ℚ = pr2 x
+
+  numerator-ℚ : ℤ
+  numerator-ℚ = numerator-fraction-ℤ fraction-ℚ
+
+  positive-denominator-ℚ : positive-ℤ
+  positive-denominator-ℚ = positive-denominator-fraction-ℤ fraction-ℚ
+
+  denominator-ℚ : ℤ
+  denominator-ℚ = denominator-fraction-ℤ fraction-ℚ
+
+  is-positive-denominator-ℚ : is-positive-ℤ denominator-ℚ
+  is-positive-denominator-ℚ = is-positive-denominator-fraction-ℤ fraction-ℚ
 ```
 
 ### Inclusion of fractions
@@ -86,6 +103,17 @@ is-one-ℚ : ℚ → UU lzero
 is-one-ℚ x = (x ＝ one-ℚ)
 ```
 
+### The mediant of two rationals
+
+```agda
+mediant-ℚ : ℚ → ℚ → ℚ
+mediant-ℚ x y =
+  in-fraction-ℤ
+    ( mediant-fraction-ℤ
+      ( fraction-ℚ x)
+      ( fraction-ℚ y))
+```
+
 ## Properties
 
 ### If two fractions are related by `sim-fraction-ℤ`, then their embeddings into `ℚ` are equal
diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md
index 06965bfcf1..ce0ae91405 100644
--- a/src/real-numbers.lagda.md
+++ b/src/real-numbers.lagda.md
@@ -6,4 +6,5 @@
 module real-numbers where
 
 open import real-numbers.dedekind-real-numbers public
+open import real-numbers.rational-real-numbers public
 ```
diff --git a/src/real-numbers/dedekind-real-numbers.lagda.md b/src/real-numbers/dedekind-real-numbers.lagda.md
index 262eaed319..f50b97b7c0 100644
--- a/src/real-numbers/dedekind-real-numbers.lagda.md
+++ b/src/real-numbers/dedekind-real-numbers.lagda.md
@@ -10,14 +10,27 @@ module real-numbers.dedekind-real-numbers where
 open import elementary-number-theory.inequality-rational-numbers
 open import elementary-number-theory.rational-numbers
 
+open import foundation.binary-transport
+open import foundation.cartesian-product-types
+open import foundation.complements-subtypes
+open import foundation.conjunction
+open import foundation.coproduct-types
 open import foundation.dependent-pair-types
 open import foundation.disjunction
+open import foundation.embeddings
+open import foundation.empty-types
 open import foundation.existential-quantification
+open import foundation.function-types
+open import foundation.functoriality-cartesian-product-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.identity-types
 open import foundation.logical-equivalences
 open import foundation.negation
+open import foundation.propositional-truncations
 open import foundation.propositions
 open import foundation.sets
 open import foundation.subtypes
+open import foundation.transport-along-identifications
 open import foundation.truncated-types
 open import foundation.universe-levels
 
@@ -96,6 +109,65 @@ module _
 ```agda
 ℝ : (l : Level) → UU (lsuc l)
 ℝ l = Σ (subtype l ℚ) (λ L → Σ (subtype l ℚ) (is-dedekind-cut L))
+
+real-dedekind-cut : {l : Level} (L U : subtype l ℚ) → is-dedekind-cut L U → ℝ l
+real-dedekind-cut L U H = L , U , H
+
+module _
+  {l : Level} (x : ℝ l)
+  where
+
+  lower-cut-ℝ : subtype l ℚ
+  lower-cut-ℝ = pr1 x
+
+  upper-cut-ℝ : subtype l ℚ
+  upper-cut-ℝ = pr1 (pr2 x)
+
+  is-in-lower-cut-ℝ : ℚ → UU l
+  is-in-lower-cut-ℝ = is-in-subtype lower-cut-ℝ
+
+  is-in-upper-cut-ℝ : ℚ → UU l
+  is-in-upper-cut-ℝ = is-in-subtype upper-cut-ℝ
+
+  is-dedekind-cut-cut-ℝ : is-dedekind-cut lower-cut-ℝ upper-cut-ℝ
+  is-dedekind-cut-cut-ℝ = pr2 (pr2 x)
+
+  is-inhabited-lower-cut-ℝ : exists ℚ lower-cut-ℝ
+  is-inhabited-lower-cut-ℝ = pr1 (pr1 is-dedekind-cut-cut-ℝ)
+
+  is-inhabited-upper-cut-ℝ : exists ℚ upper-cut-ℝ
+  is-inhabited-upper-cut-ℝ = pr2 (pr1 is-dedekind-cut-cut-ℝ)
+
+  is-rounded-lower-cut-ℝ :
+    (q : ℚ) →
+    is-in-lower-cut-ℝ q ↔ ∃ ℚ (λ r → (le-ℚ q r) × (is-in-lower-cut-ℝ r))
+  is-rounded-lower-cut-ℝ =
+    pr1 (pr1 (pr2 is-dedekind-cut-cut-ℝ))
+
+  is-rounded-upper-cut-ℝ :
+    (r : ℚ) →
+    is-in-upper-cut-ℝ r ↔ ∃ ℚ (λ q → (le-ℚ q r) × (is-in-upper-cut-ℝ q))
+  is-rounded-upper-cut-ℝ =
+    pr2 (pr1 (pr2 is-dedekind-cut-cut-ℝ))
+
+  is-disjoint-cut-ℝ : (q : ℚ) → ¬ (is-in-lower-cut-ℝ q × is-in-upper-cut-ℝ q)
+  is-disjoint-cut-ℝ =
+    pr1 (pr2 (pr2 is-dedekind-cut-cut-ℝ))
+
+  is-located-lower-upper-cut-ℝ :
+    (q r : ℚ) → le-ℚ q r → (lower-cut-ℝ q) ∨ (upper-cut-ℝ r)
+  is-located-lower-upper-cut-ℝ =
+    pr2 (pr2 (pr2 is-dedekind-cut-cut-ℝ))
+
+  cut-ℝ : subtype l ℚ
+  cut-ℝ q =
+    coproduct-Prop
+      ( lower-cut-ℝ q)
+      ( upper-cut-ℝ q)
+      ( ev-pair ( is-disjoint-cut-ℝ q))
+
+  is-in-cut-ℝ : ℚ → UU l
+  is-in-cut-ℝ = is-in-subtype cut-ℝ
 ```
 
 ## Properties
@@ -121,6 +193,325 @@ pr1 (ℝ-Set l) = ℝ l
 pr2 (ℝ-Set l) = is-set-ℝ l
 ```
 
+## Properties of lower/upper Dedekind cuts
+
+### Lower and upper Dedekind cuts are closed under the standard ordering on the rationals
+
+```agda
+module _
+  {l : Level} (x : ℝ l) (p q : ℚ)
+  where
+
+  le-lower-cut-ℝ :
+    le-ℚ p q →
+    is-in-lower-cut-ℝ x q →
+    is-in-lower-cut-ℝ x p
+  le-lower-cut-ℝ H H' =
+    ind-trunc-Prop
+      ( λ s → lower-cut-ℝ x p)
+      ( rec-coproduct
+          ( id)
+          ( λ I → ex-falso (is-disjoint-cut-ℝ x q (H' , I))))
+      ( is-located-lower-upper-cut-ℝ x p q H)
+
+  leq-lower-cut-ℝ :
+    leq-ℚ p q →
+    is-in-lower-cut-ℝ x q →
+    is-in-lower-cut-ℝ x p
+  leq-lower-cut-ℝ H H' =
+    rec-coproduct
+      ( λ s → le-lower-cut-ℝ s H')
+      ( λ I →
+        tr
+          ( is-in-lower-cut-ℝ x)
+          ( antisymmetric-leq-ℚ q p I H)
+          ( H'))
+      ( decide-le-leq-ℚ p q)
+
+  le-upper-cut-ℝ :
+    le-ℚ p q →
+    is-in-upper-cut-ℝ x p →
+    is-in-upper-cut-ℝ x q
+  le-upper-cut-ℝ H H' =
+    ind-trunc-Prop
+      ( λ s → upper-cut-ℝ x q)
+      ( rec-coproduct
+        ( λ I → ex-falso (is-disjoint-cut-ℝ x p ( I , H')))
+        ( id))
+      ( is-located-lower-upper-cut-ℝ x p q H)
+
+  leq-upper-cut-ℝ :
+    leq-ℚ p q →
+    is-in-upper-cut-ℝ x p →
+    is-in-upper-cut-ℝ x q
+  leq-upper-cut-ℝ H H' =
+    rec-coproduct
+      ( λ s → le-upper-cut-ℝ s H')
+      ( λ I →
+        tr
+          ( is-in-upper-cut-ℝ x)
+          ( antisymmetric-leq-ℚ p q H I)
+          ( H'))
+      ( decide-le-leq-ℚ p q)
+```
+
+### Elements of the lower cut are lower bounds of the upper cut
+
+```agda
+module _
+  {l : Level} (x : ℝ l) (p q : ℚ)
+  where
+
+  le-lower-upper-cut-ℝ :
+    is-in-lower-cut-ℝ x p →
+    is-in-upper-cut-ℝ x q →
+    le-ℚ p q
+  le-lower-upper-cut-ℝ H H' =
+    rec-coproduct
+      ( id)
+      ( λ I →
+        ex-falso
+          ( is-disjoint-cut-ℝ x p
+              ( H , leq-upper-cut-ℝ x q p I H')))
+      ( decide-le-leq-ℚ p q)
+```
+
+### Characterisation of each cut by the other
+
+#### The lower cut is the subtype of rationals bounded above by some element of the complement of the upper cut
+
+```agda
+module _
+  {l : Level} (x : ℝ l)
+  where
+
+  is-lower-complement-upper-cut-ℝ-Prop : (p q : ℚ) → Prop l
+  is-lower-complement-upper-cut-ℝ-Prop p q =
+    product-Prop
+      ( le-ℚ-Prop p q)
+      ( neg-Prop ( upper-cut-ℝ x q))
+
+  lower-complement-upper-cut-ℝ : subtype l ℚ
+  lower-complement-upper-cut-ℝ p =
+    exists-Prop ℚ (is-lower-complement-upper-cut-ℝ-Prop p)
+```
+
+```agda
+module _
+  {l : Level} (x : ℝ l)
+  where
+
+  subset-lower-cut-lower-complement-upper-cut-ℝ :
+    lower-complement-upper-cut-ℝ x ⊆ lower-cut-ℝ x
+  subset-lower-cut-lower-complement-upper-cut-ℝ p =
+    elim-exists-Prop
+      ( is-lower-complement-upper-cut-ℝ-Prop x p)
+      ( lower-cut-ℝ x p)
+      ( λ q I →
+        map-right-unit-law-disjunction-is-empty-Prop
+          ( lower-cut-ℝ x p)
+          ( upper-cut-ℝ x q)
+          ( pr2 I)
+          ( is-located-lower-upper-cut-ℝ x p q ( pr1 I)))
+
+  subset-lower-complement-upper-cut-lower-cut-ℝ :
+    lower-cut-ℝ x ⊆ lower-complement-upper-cut-ℝ x
+  subset-lower-complement-upper-cut-lower-cut-ℝ p H =
+    elim-exists-Prop
+      ( λ q → product-Prop (le-ℚ-Prop p q) (lower-cut-ℝ x q))
+      ( lower-complement-upper-cut-ℝ x p)
+      ( λ q I →
+        intro-exists
+          ( is-lower-complement-upper-cut-ℝ-Prop x p)
+          ( q)
+          ( map-product
+            ( id)
+            ( λ L U → is-disjoint-cut-ℝ x q (L , U))
+            ( I)))
+      ( pr1 (is-rounded-lower-cut-ℝ x p) H)
+
+  eq-lower-cut-lower-complement-upper-cut-ℝ :
+    lower-complement-upper-cut-ℝ x ＝ lower-cut-ℝ x
+  eq-lower-cut-lower-complement-upper-cut-ℝ =
+    antisymmetric-leq-subtype
+      ( lower-complement-upper-cut-ℝ x)
+      ( lower-cut-ℝ x)
+      ( subset-lower-cut-lower-complement-upper-cut-ℝ)
+      ( subset-lower-complement-upper-cut-lower-cut-ℝ)
+```
+
+#### The upper cut is the subtype of rationals bounded below by some element of the complement of the lower cut
+
+```agda
+module _
+  {l : Level} (x : ℝ l)
+  where
+
+  is-upper-complement-lower-cut-ℝ-Prop : (q p : ℚ) → Prop l
+  is-upper-complement-lower-cut-ℝ-Prop q p =
+    product-Prop
+      ( le-ℚ-Prop p q)
+      ( neg-Prop ( lower-cut-ℝ x p))
+
+  upper-complement-lower-cut-ℝ : subtype l ℚ
+  upper-complement-lower-cut-ℝ q =
+    exists-Prop ℚ (is-upper-complement-lower-cut-ℝ-Prop q)
+```
+
+```agda
+module _
+  {l : Level} (x : ℝ l)
+  where
+
+  subset-upper-cut-upper-complement-lower-cut-ℝ :
+    upper-complement-lower-cut-ℝ x ⊆ upper-cut-ℝ x
+  subset-upper-cut-upper-complement-lower-cut-ℝ q =
+    elim-exists-Prop
+      ( is-upper-complement-lower-cut-ℝ-Prop x q)
+      ( upper-cut-ℝ x q)
+      ( λ p I →
+        map-left-unit-law-disjunction-is-empty-Prop
+          ( lower-cut-ℝ x p)
+          ( upper-cut-ℝ x q)
+          ( pr2 I)
+          ( is-located-lower-upper-cut-ℝ x p q ( pr1 I)))
+
+  subset-upper-complement-lower-cut-upper-cut-ℝ :
+    upper-cut-ℝ x ⊆ upper-complement-lower-cut-ℝ x
+  subset-upper-complement-lower-cut-upper-cut-ℝ q H =
+    elim-exists-Prop
+      ( λ p → product-Prop (le-ℚ-Prop p q) (upper-cut-ℝ x p))
+      ( upper-complement-lower-cut-ℝ x q)
+      ( λ p I →
+        intro-exists
+          ( is-upper-complement-lower-cut-ℝ-Prop x q)
+          ( p)
+          ( map-product
+            ( id)
+            ( λ U L → is-disjoint-cut-ℝ x p (L , U))
+            ( I)))
+      ( pr1 (is-rounded-upper-cut-ℝ x q) H)
+
+  eq-upper-cut-upper-complement-lower-cut-ℝ :
+    upper-complement-lower-cut-ℝ x ＝ upper-cut-ℝ x
+  eq-upper-cut-upper-complement-lower-cut-ℝ =
+    antisymmetric-leq-subtype
+      ( upper-complement-lower-cut-ℝ x)
+      ( upper-cut-ℝ x)
+      ( subset-upper-cut-upper-complement-lower-cut-ℝ)
+      ( subset-upper-complement-lower-cut-upper-cut-ℝ)
+```
+
+### The lower/upper cut of a real determines the other
+
+```agda
+module _
+  {l : Level} (x y : ℝ l)
+  where
+
+  subset-lower-cut-upper-cut-ℝ :
+    upper-cut-ℝ y ⊆ upper-cut-ℝ x → lower-cut-ℝ x ⊆ lower-cut-ℝ y
+  subset-lower-cut-upper-cut-ℝ H =
+    binary-tr
+      ( _⊆_)
+      ( eq-lower-cut-lower-complement-upper-cut-ℝ x)
+      ( eq-lower-cut-lower-complement-upper-cut-ℝ y)
+      ( λ p →
+        elim-exists-Prop
+          ( is-lower-complement-upper-cut-ℝ-Prop x p)
+          ( lower-complement-upper-cut-ℝ y p)
+          ( λ q → intro-∃ q ∘ tot (λ _ K → K ∘ H q)))
+
+  subset-upper-cut-lower-cut-ℝ :
+    lower-cut-ℝ x ⊆ lower-cut-ℝ y → upper-cut-ℝ y ⊆ upper-cut-ℝ x
+  subset-upper-cut-lower-cut-ℝ H =
+    binary-tr
+      ( _⊆_)
+      ( eq-upper-cut-upper-complement-lower-cut-ℝ y)
+      ( eq-upper-cut-upper-complement-lower-cut-ℝ x)
+      ( λ q →
+        elim-exists-Prop
+          ( is-upper-complement-lower-cut-ℝ-Prop y q)
+          ( upper-complement-lower-cut-ℝ x q)
+          ( λ p → intro-∃ p ∘ tot (λ _ K → K ∘ H p)))
+
+module _
+  {l : Level} (x y : ℝ l)
+  where
+
+  eq-lower-cut-eq-upper-cut-ℝ :
+    upper-cut-ℝ x ＝ upper-cut-ℝ y → lower-cut-ℝ x ＝ lower-cut-ℝ y
+  eq-lower-cut-eq-upper-cut-ℝ H =
+    antisymmetric-leq-subtype
+      ( lower-cut-ℝ x)
+      ( lower-cut-ℝ y)
+      ( subset-lower-cut-upper-cut-ℝ x y
+        ( pr2 ∘ has-same-elements-eq-subtype
+          ( upper-cut-ℝ x)
+          ( upper-cut-ℝ y)
+          ( H)))
+      ( subset-lower-cut-upper-cut-ℝ y x
+        ( pr1 ∘ has-same-elements-eq-subtype
+          ( upper-cut-ℝ x)
+          ( upper-cut-ℝ y)
+          ( H)))
+
+  eq-upper-cut-eq-lower-cut-ℝ :
+    lower-cut-ℝ x ＝ lower-cut-ℝ y → upper-cut-ℝ x ＝ upper-cut-ℝ y
+  eq-upper-cut-eq-lower-cut-ℝ H =
+    antisymmetric-leq-subtype
+      ( upper-cut-ℝ x)
+      ( upper-cut-ℝ y)
+      ( subset-upper-cut-lower-cut-ℝ y x
+        ( pr2 ∘ has-same-elements-eq-subtype
+          ( lower-cut-ℝ x)
+          ( lower-cut-ℝ y)
+          ( H)))
+      ( subset-upper-cut-lower-cut-ℝ x y
+        ( pr1 ∘ has-same-elements-eq-subtype
+          ( lower-cut-ℝ x)
+          ( lower-cut-ℝ y)
+          ( H)))
+```
+
+### The map from a real number to its lower cut is an embedding
+
+```agda
+module _
+  {l : Level} (L : subtype l ℚ)
+  where
+
+  has-upper-cut-Prop : Prop (lsuc l)
+  has-upper-cut-Prop =
+    pair
+      ( Σ (subtype l ℚ) (is-dedekind-cut L))
+      ( is-prop-all-elements-equal
+        ( λ U U' →
+          eq-type-subtype
+            ( is-dedekind-cut-Prop L)
+            ( eq-upper-cut-eq-lower-cut-ℝ
+              ( pair L U)
+              ( pair L U')
+              ( refl))))
+
+is-emb-lower-cut : {l : Level} → is-emb (lower-cut-ℝ {l})
+is-emb-lower-cut = is-emb-inclusion-subtype has-upper-cut-Prop
+```
+
+### Two real numbers with the same lower/upper cut are equal
+
+```agda
+module _
+  {l : Level} (x y : ℝ l)
+  where
+
+  eq-eq-lower-cut-ℝ : lower-cut-ℝ x ＝ lower-cut-ℝ y → x ＝ y
+  eq-eq-lower-cut-ℝ = eq-type-subtype has-upper-cut-Prop
+
+  eq-eq-upper-cut-ℝ : upper-cut-ℝ x ＝ upper-cut-ℝ y → x ＝ y
+  eq-eq-upper-cut-ℝ = eq-eq-lower-cut-ℝ ∘ (eq-lower-cut-eq-upper-cut-ℝ x y)
+```
+
 ## References
 
 1. Section 11.2 of Univalent Foundations Project, _Homotopy Type Theory –
diff --git a/src/real-numbers/rational-real-numbers.lagda.md b/src/real-numbers/rational-real-numbers.lagda.md
new file mode 100644
index 0000000000..878b9e33fc
--- /dev/null
+++ b/src/real-numbers/rational-real-numbers.lagda.md
@@ -0,0 +1,256 @@
+# Rational real numbers
+
+```agda
+module real-numbers.rational-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.disjunction
+open import foundation.embeddings
+open import foundation.empty-types
+open import foundation.equivalences
+open import foundation.existential-quantification
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.negation
+open import foundation.propositional-truncations
+open import foundation.propositions
+open import foundation.retractions
+open import foundation.sections
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import real-numbers.dedekind-real-numbers
+```
+
+</details>
+
+## Idea
+
+The type of [rationals](elementary-number-theory.rational-numbers.md) `ℚ`
+[embeds](foundation-core.embeddings.md) into the type of
+[Dedekind reals](real-numbers.dedekind-real-numbers.md) `ℝ`. We call numbers in
+the [image](foundation.images.md) of this embedding
+{{#concept "rational real numbers" Agda=Rational-ℝ}}.
+
+## Definitions
+
+### Strict inequality on rationals gives Dedekind cuts
+
+```agda
+is-dedekind-cut-le-ℚ :
+  (x : ℚ) →
+  is-dedekind-cut
+    (λ (q : ℚ) → le-ℚ-Prop q x)
+    (λ (r : ℚ) → le-ℚ-Prop x r)
+is-dedekind-cut-le-ℚ x =
+  ( left-∃-le-ℚ x , right-∃-le-ℚ x) ,
+  ( ( λ (q : ℚ) →
+      dense-le-ℚ q x ,
+      elim-exists-Prop
+        ( λ r → product-Prop ( le-ℚ-Prop q r) ( le-ℚ-Prop r x))
+        ( le-ℚ-Prop q x)
+        ( λ r (H , H') → transitive-le-ℚ q r x H H')) ,
+    ( λ (r : ℚ) →
+      α x r ∘ dense-le-ℚ x r ,
+      elim-exists-Prop
+        ( λ q → product-Prop ( le-ℚ-Prop q r) ( le-ℚ-Prop x q))
+        ( le-ℚ-Prop x r)
+        ( λ q (H , H') → transitive-le-ℚ x q r H' H))) ,
+  ( λ (q : ℚ) (H , H') → asymmetric-le-ℚ q x H H') ,
+  ( located-le-ℚ x)
+  where
+    α :
+      (a b : ℚ) →
+      ∃ ℚ (λ r → le-ℚ a r × le-ℚ r b) →
+      ∃ ℚ (λ r → le-ℚ r b × le-ℚ a r)
+    α a b =
+      elim-exists-Prop
+        ( ( λ r →
+            product-Prop
+              ( le-ℚ-Prop a r)
+              ( le-ℚ-Prop r b)))
+        ( exists-Prop ℚ
+          ( λ r →
+            product-Prop
+              ( le-ℚ-Prop r b)
+              ( le-ℚ-Prop a r)))
+        ( λ r ( p , q) → intro-∃ r ( q , p))
+```
+
+### The canonical map from `ℚ` to `ℝ`
+
+```agda
+real-rational : ℚ → ℝ lzero
+real-rational x =
+  real-dedekind-cut
+    ( λ (q : ℚ) → le-ℚ-Prop q x)
+    ( λ (r : ℚ) → le-ℚ-Prop x r)
+    ( is-dedekind-cut-le-ℚ x)
+```
+
+### The property of being a rational real number
+
+```agda
+module _
+  {l : Level} (x : ℝ l) (p : ℚ)
+  where
+
+  is-rational-ℝ-Prop : Prop l
+  is-rational-ℝ-Prop =
+    product-Prop
+      ( neg-Prop (lower-cut-ℝ x p))
+      ( neg-Prop (upper-cut-ℝ x p))
+
+  is-rational-ℝ : UU l
+  is-rational-ℝ = type-Prop is-rational-ℝ-Prop
+```
+
+```agda
+all-eq-is-rational-ℝ :
+  {l : Level} (x : ℝ l) (p q : ℚ) →
+  is-rational-ℝ x p →
+  is-rational-ℝ x q →
+  p ＝ q
+all-eq-is-rational-ℝ x p q H H' =
+  trichotomy-le-ℚ p q left-case id right-case
+  where
+  left-case : le-ℚ p q → p ＝ q
+  left-case I =
+    ex-falso
+      ( elim-disjunction-Prop
+        ( lower-cut-ℝ x p)
+        ( upper-cut-ℝ x q)
+        ( empty-Prop)
+        ( pr1 H , pr2 H')
+        ( is-located-lower-upper-cut-ℝ x p q I))
+
+  right-case : le-ℚ q p → p ＝ q
+  right-case I =
+    ex-falso
+      ( elim-disjunction-Prop
+        ( lower-cut-ℝ x q)
+        ( upper-cut-ℝ x p)
+        ( empty-Prop)
+        ( pr1 H' , pr2 H)
+        ( is-located-lower-upper-cut-ℝ x q p I))
+
+is-prop-rational-real : {l : Level} (x : ℝ l) → is-prop (Σ ℚ (is-rational-ℝ x))
+is-prop-rational-real x =
+  is-prop-all-elements-equal
+    ( λ p q →
+      eq-type-subtype
+        ( is-rational-ℝ-Prop x)
+        ( all-eq-is-rational-ℝ x (pr1 p) (pr1 q) (pr2 p) (pr2 q)))
+```
+
+### The subtype of rational reals
+
+```agda
+subtype-rational-real : {l : Level} → ℝ l → Prop l
+subtype-rational-real x =
+  Σ ℚ (is-rational-ℝ x) , is-prop-rational-real x
+
+Rational-ℝ : (l : Level) → UU (lsuc l)
+Rational-ℝ l =
+  type-subtype subtype-rational-real
+
+module _
+  {l : Level} (x : Rational-ℝ l)
+  where
+
+  real-rational-ℝ : ℝ l
+  real-rational-ℝ = pr1 x
+
+  rational-rational-ℝ : ℚ
+  rational-rational-ℝ = pr1 (pr2 x)
+
+  is-rational-rational-ℝ : is-rational-ℝ real-rational-ℝ rational-rational-ℝ
+  is-rational-rational-ℝ = pr2 (pr2 x)
+```
+
+## Properties
+
+### The real embedding of a rational number is rational
+
+```agda
+is-rational-real-rational : (p : ℚ) → is-rational-ℝ (real-rational p) p
+is-rational-real-rational p = irreflexive-le-ℚ p , irreflexive-le-ℚ p
+```
+
+### Rational real numbers are embedded rationals
+
+```agda
+eq-real-rational-is-rational-ℝ :
+  (x : ℝ lzero) (q : ℚ) (H : is-rational-ℝ x q) → real-rational q ＝ x
+eq-real-rational-is-rational-ℝ x q H =
+  eq-eq-lower-cut-ℝ
+    ( real-rational q)
+    ( x)
+    ( eq-has-same-elements-subtype
+      ( λ p → le-ℚ-Prop p q)
+      ( lower-cut-ℝ x)
+      ( λ r →
+        pair
+          ( λ I → elim-disjunction-Prop
+            ( lower-cut-ℝ x r)
+            ( upper-cut-ℝ x q)
+            ( lower-cut-ℝ x r)
+            ( id , λ H' → ex-falso (pr2 H 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'))))))
+```
+
+### The cannonical map from rationals to rational reals
+
+```agda
+rational-ℝ-rational : ℚ → Rational-ℝ lzero
+rational-ℝ-rational q = real-rational q , q , is-rational-real-rational q
+```
+
+### The rationals and rational reals are equivalent
+
+```agda
+is-section-rational-ℝ-rational :
+  (q : ℚ) →
+  rational-rational-ℝ (rational-ℝ-rational q) ＝ q
+is-section-rational-ℝ-rational q = refl
+
+is-retraction-rational-ℝ-rational :
+  (x : Rational-ℝ lzero) →
+  rational-ℝ-rational (rational-rational-ℝ x) ＝ x
+is-retraction-rational-ℝ-rational (x , q , H) =
+  eq-type-subtype
+    subtype-rational-real
+    ( ap real-rational α ∙ eq-real-rational-is-rational-ℝ x q H)
+  where
+    α : rational-rational-ℝ (x , q , H) ＝ q
+    α = refl
+
+equiv-rational-real : Rational-ℝ lzero ≃ ℚ
+pr1 equiv-rational-real = rational-rational-ℝ
+pr2 equiv-rational-real =
+  section-rational-rational-ℝ , retraction-rational-rational-ℝ
+  where
+  section-rational-rational-ℝ : section rational-rational-ℝ
+  section-rational-rational-ℝ =
+    rational-ℝ-rational , is-section-rational-ℝ-rational
+
+  retraction-rational-rational-ℝ : retraction rational-rational-ℝ
+  retraction-rational-rational-ℝ =
+    rational-ℝ-rational , is-retraction-rational-ℝ-rational
+```