diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md
index 815543ad14..8d04d1a4f3 100644
--- a/src/elementary-number-theory.lagda.md
+++ b/src/elementary-number-theory.lagda.md
@@ -10,6 +10,7 @@
 module elementary-number-theory where
 
 open import elementary-number-theory.absolute-value-integers public
+open import elementary-number-theory.absolute-value-rational-numbers public
 open import elementary-number-theory.ackermann-function public
 open import elementary-number-theory.addition-integer-fractions public
 open import elementary-number-theory.addition-integers public
@@ -127,7 +128,9 @@ open import elementary-number-theory.natural-numbers public
 open import elementary-number-theory.negative-integer-fractions public
 open import elementary-number-theory.negative-integers public
 open import elementary-number-theory.negative-rational-numbers public
+open import elementary-number-theory.nonnegative-integer-fractions public
 open import elementary-number-theory.nonnegative-integers public
+open import elementary-number-theory.nonnegative-rational-numbers public
 open import elementary-number-theory.nonpositive-integers public
 open import elementary-number-theory.nonzero-integers public
 open import elementary-number-theory.nonzero-natural-numbers public
diff --git a/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md b/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md
new file mode 100644
index 0000000000..7c69ea4eac
--- /dev/null
+++ b/src/elementary-number-theory/absolute-value-rational-numbers.lagda.md
@@ -0,0 +1,266 @@
+# The absolute value function on the rational numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module elementary-number-theory.absolute-value-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-rational-numbers
+open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.maximum-rational-numbers
+open import elementary-number-theory.multiplication-rational-numbers
+open import elementary-number-theory.nonnegative-rational-numbers
+open import elementary-number-theory.rational-numbers
+
+open import foundation.action-on-identifications-binary-functions
+open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
+open import foundation.coproduct-types
+open import foundation.dependent-pair-types
+open import foundation.function-types
+open import foundation.identity-types
+open import foundation.transport-along-identifications
+```
+
+</details>
+
+## Idea
+
+The
+{{#concept "absolute value" Disambiguation="of a rational number" Agda=abs-ℚ WD="absolute value" WDID=Q120812}}
+of a [rational number](elementary-number-theory.rational-numbers.md) is the
+[greater](elementary-number-theory.maximum-rational-numbers.md) of itself and
+its negation.
+
+## Definition
+
+```agda
+rational-abs-ℚ : ℚ → ℚ
+rational-abs-ℚ q = max-ℚ q (neg-ℚ q)
+
+abstract
+  is-nonnegative-rational-abs-ℚ : (q : ℚ) → is-nonnegative-ℚ (rational-abs-ℚ q)
+  is-nonnegative-rational-abs-ℚ q =
+    rec-coproduct
+      ( λ 0≤q →
+        inv-tr
+          ( is-nonnegative-ℚ)
+          ( right-leq-left-max-ℚ
+            ( q)
+            ( neg-ℚ q)
+            ( transitive-leq-ℚ (neg-ℚ q) zero-ℚ q 0≤q (neg-leq-ℚ zero-ℚ q 0≤q)))
+          ( is-nonnegative-leq-zero-ℚ q 0≤q))
+      ( λ q≤0 →
+        inv-tr
+          ( is-nonnegative-ℚ)
+          ( left-leq-right-max-ℚ
+            ( q)
+            ( neg-ℚ q)
+            ( transitive-leq-ℚ q zero-ℚ (neg-ℚ q) (neg-leq-ℚ q zero-ℚ q≤0) q≤0))
+          ( is-nonnegative-leq-zero-ℚ (neg-ℚ q) (neg-leq-ℚ q zero-ℚ q≤0)))
+      ( linear-leq-ℚ zero-ℚ q)
+
+abs-ℚ : ℚ → ℚ⁰⁺
+pr1 (abs-ℚ q) = rational-abs-ℚ q
+pr2 (abs-ℚ q) = is-nonnegative-rational-abs-ℚ q
+```
+
+## Properties
+
+### The absolute value of a nonnegative rational number is the number itself
+
+```agda
+abstract
+  abs-rational-ℚ⁰⁺ : (q : ℚ⁰⁺) → abs-ℚ (rational-ℚ⁰⁺ q) ＝ q
+  abs-rational-ℚ⁰⁺ (q , nonneg-q) =
+    eq-ℚ⁰⁺
+      ( right-leq-left-max-ℚ
+        ( q)
+        ( neg-ℚ q)
+        ( transitive-leq-ℚ
+          ( neg-ℚ q)
+          ( zero-ℚ)
+          ( q)
+          ( leq-zero-is-nonnegative-ℚ q nonneg-q)
+          ( neg-leq-ℚ zero-ℚ q (leq-zero-is-nonnegative-ℚ q nonneg-q))))
+
+  rational-abs-zero-leq-ℚ : (q : ℚ) → leq-ℚ zero-ℚ q → rational-abs-ℚ q ＝ q
+  rational-abs-zero-leq-ℚ q 0≤q =
+    ap rational-ℚ⁰⁺ (abs-rational-ℚ⁰⁺ (q , is-nonnegative-leq-zero-ℚ q 0≤q))
+
+  rational-abs-leq-zero-ℚ :
+    (q : ℚ) → leq-ℚ q zero-ℚ → rational-abs-ℚ q ＝ neg-ℚ q
+  rational-abs-leq-zero-ℚ q q≤0 =
+    left-leq-right-max-ℚ
+      ( q)
+      ( neg-ℚ q)
+      ( transitive-leq-ℚ
+        ( q)
+        ( zero-ℚ)
+        ( neg-ℚ q)
+        ( neg-leq-ℚ q zero-ℚ q≤0)
+        ( q≤0))
+```
+
+### The absolute value of the negation of `q` is the absolute value of `q`
+
+```agda
+abstract
+  abs-neg-ℚ : (q : ℚ) → abs-ℚ (neg-ℚ q) ＝ abs-ℚ q
+  abs-neg-ℚ q =
+    eq-ℚ⁰⁺
+      ( ap (max-ℚ (neg-ℚ q)) (neg-neg-ℚ q) ∙ commutative-max-ℚ _ _)
+```
+
+### `q` is less than or equal to `abs-ℚ q`
+
+```agda
+abstract
+  leq-abs-ℚ : (q : ℚ) → leq-ℚ q (rational-abs-ℚ q)
+  leq-abs-ℚ q = leq-left-max-ℚ q (neg-ℚ q)
+
+  neg-leq-abs-ℚ : (q : ℚ) → leq-ℚ (neg-ℚ q) (rational-abs-ℚ q)
+  neg-leq-abs-ℚ q = leq-right-max-ℚ q (neg-ℚ q)
+```
+
+### The absolute value of `q` is zero iff `q` is zero
+
+```agda
+abstract
+  eq-zero-eq-abs-zero-ℚ : (q : ℚ) → abs-ℚ q ＝ zero-ℚ⁰⁺ → q ＝ zero-ℚ
+  eq-zero-eq-abs-zero-ℚ q abs=0 =
+    rec-coproduct
+      ( λ 0≤q →
+        antisymmetric-leq-ℚ
+          ( q)
+          ( zero-ℚ)
+          ( tr (leq-ℚ q) (ap rational-ℚ⁰⁺ abs=0) (leq-abs-ℚ q)) 0≤q)
+      ( λ q≤0 →
+        antisymmetric-leq-ℚ
+          ( q)
+          ( zero-ℚ)
+          ( q≤0)
+          ( tr
+            ( leq-ℚ zero-ℚ)
+            ( neg-neg-ℚ q)
+            ( neg-leq-ℚ
+              ( neg-ℚ q)
+              ( zero-ℚ)
+              ( tr
+                ( leq-ℚ (neg-ℚ q))
+                ( ap rational-ℚ⁰⁺ abs=0)
+                ( neg-leq-abs-ℚ q)))))
+      ( linear-leq-ℚ zero-ℚ q)
+
+  abs-zero-ℚ : abs-ℚ zero-ℚ ＝ zero-ℚ⁰⁺
+  abs-zero-ℚ = eq-ℚ⁰⁺ (left-leq-right-max-ℚ _ _ (refl-leq-ℚ zero-ℚ))
+```
+
+### The triangle inequality
+
+```agda
+abstract
+  triangle-inequality-abs-ℚ :
+    (p q : ℚ) → leq-ℚ⁰⁺ (abs-ℚ (p +ℚ q)) (abs-ℚ p +ℚ⁰⁺ abs-ℚ q)
+  triangle-inequality-abs-ℚ p q =
+    leq-max-leq-both-ℚ
+      ( rational-abs-ℚ p +ℚ rational-abs-ℚ q)
+      ( _)
+      ( _)
+      ( preserves-leq-add-ℚ
+        { p}
+        { rational-abs-ℚ p}
+        { q}
+        { rational-abs-ℚ q}
+        ( leq-abs-ℚ p)
+        ( leq-abs-ℚ q))
+      ( inv-tr
+        ( λ r → leq-ℚ r (rational-abs-ℚ p +ℚ rational-abs-ℚ q))
+        ( distributive-neg-add-ℚ p q)
+        ( preserves-leq-add-ℚ
+          { neg-ℚ p}
+          { rational-abs-ℚ p}
+          { neg-ℚ q}
+          { rational-abs-ℚ q}
+          ( neg-leq-abs-ℚ p)
+          ( neg-leq-abs-ℚ q)))
+```
+
+### `|ab| = |a||b|`
+
+```agda
+abstract
+  abs-left-mul-nonnegative-ℚ :
+    (q : ℚ) (p : ℚ⁰⁺) → abs-ℚ (rational-ℚ⁰⁺ p *ℚ q) ＝ p *ℚ⁰⁺ abs-ℚ q
+  abs-left-mul-nonnegative-ℚ q p⁰⁺@(p , nonneg-p) with linear-leq-ℚ zero-ℚ q
+  ... | inl 0≤q =
+    eq-ℚ⁰⁺
+      ( equational-reasoning
+        rational-abs-ℚ (p *ℚ q)
+        ＝ p *ℚ q
+          by
+            ap
+              ( rational-ℚ⁰⁺)
+              ( abs-rational-ℚ⁰⁺
+                ( p⁰⁺ *ℚ⁰⁺ (q , is-nonnegative-leq-zero-ℚ q 0≤q)))
+        ＝ p *ℚ rational-abs-ℚ q
+          by ap (p *ℚ_) (inv (rational-abs-zero-leq-ℚ q 0≤q)))
+  ... | inr q≤0 =
+    eq-ℚ⁰⁺
+      ( equational-reasoning
+        rational-abs-ℚ (p *ℚ q)
+        ＝ rational-abs-ℚ (neg-ℚ (p *ℚ q))
+          by ap rational-ℚ⁰⁺ (inv (abs-neg-ℚ (p *ℚ q)))
+        ＝ rational-abs-ℚ (p *ℚ neg-ℚ q)
+          by ap rational-abs-ℚ (inv (right-negative-law-mul-ℚ p q))
+        ＝ p *ℚ neg-ℚ q
+          by
+            ap
+              ( rational-ℚ⁰⁺)
+              ( abs-rational-ℚ⁰⁺
+                ( p⁰⁺ *ℚ⁰⁺
+                  ( neg-ℚ q ,
+                    is-nonnegative-leq-zero-ℚ
+                      ( neg-ℚ q)
+                      ( neg-leq-ℚ q zero-ℚ q≤0))))
+        ＝ p *ℚ rational-abs-ℚ q
+          by ap (p *ℚ_) (inv (rational-abs-leq-zero-ℚ q q≤0)))
+
+  abs-mul-ℚ : (p q : ℚ) → abs-ℚ (p *ℚ q) ＝ abs-ℚ p *ℚ⁰⁺ abs-ℚ q
+  abs-mul-ℚ p q with linear-leq-ℚ zero-ℚ p
+  ... | inl 0≤p =
+    eq-ℚ⁰⁺
+      ( equational-reasoning
+        rational-abs-ℚ (p *ℚ q)
+        ＝ p *ℚ rational-abs-ℚ q
+          by
+            ap
+              ( rational-ℚ⁰⁺)
+              ( abs-left-mul-nonnegative-ℚ
+                ( q)
+                ( p , is-nonnegative-leq-zero-ℚ p 0≤p))
+        ＝ rational-abs-ℚ p *ℚ rational-abs-ℚ q
+          by ap (_*ℚ rational-abs-ℚ q) (inv (rational-abs-zero-leq-ℚ p 0≤p)))
+  ... | inr p≤0 =
+    eq-ℚ⁰⁺
+      ( equational-reasoning
+        rational-abs-ℚ (p *ℚ q)
+        ＝ rational-abs-ℚ (neg-ℚ (p *ℚ q))
+          by ap rational-ℚ⁰⁺ (inv (abs-neg-ℚ (p *ℚ q)))
+        ＝ rational-abs-ℚ (neg-ℚ p *ℚ q)
+          by ap rational-abs-ℚ (inv (left-negative-law-mul-ℚ p q))
+        ＝ neg-ℚ p *ℚ rational-abs-ℚ q
+          by
+            ap
+              ( rational-ℚ⁰⁺)
+              ( abs-left-mul-nonnegative-ℚ
+                ( q)
+                ( neg-ℚ p ,
+                  is-nonnegative-leq-zero-ℚ (neg-ℚ p) (neg-leq-ℚ p zero-ℚ p≤0)))
+        ＝ rational-abs-ℚ p *ℚ rational-abs-ℚ q
+          by ap (_*ℚ rational-abs-ℚ q) (inv (rational-abs-leq-zero-ℚ p p≤0)))
+```
diff --git a/src/elementary-number-theory/inequality-rational-numbers.lagda.md b/src/elementary-number-theory/inequality-rational-numbers.lagda.md
index 4d2603dade..690b806b34 100644
--- a/src/elementary-number-theory/inequality-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/inequality-rational-numbers.lagda.md
@@ -355,6 +355,13 @@ preserves-leq-add-ℚ {a} {b} {c} {d} H K =
     ( preserves-leq-left-add-ℚ c a b H)
 ```
 
+### Negation of rational numbers reverses inequality
+
+```agda
+neg-leq-ℚ : (x y : ℚ) → leq-ℚ x y → leq-ℚ (neg-ℚ y) (neg-ℚ x)
+neg-leq-ℚ x y = neg-leq-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)
+```
+
 ### Transposing additions on inequalities of rational numbers
 
 ```agda
@@ -415,13 +422,6 @@ pr1 (leq-iff-transpose-left-diff-ℚ x y z) = leq-transpose-left-diff-ℚ x y z
 pr2 (leq-iff-transpose-left-diff-ℚ x y z) = leq-transpose-right-add-ℚ x z y
 ```
 
-### Negation of rational numbers reverses inequality
-
-```agda
-neg-leq-ℚ : (x y : ℚ) → leq-ℚ x y → leq-ℚ (neg-ℚ y) (neg-ℚ x)
-neg-leq-ℚ x y = neg-leq-fraction-ℤ (fraction-ℚ x) (fraction-ℚ y)
-```
-
 ## See also
 
 - The decidable total order on the rational numbers is defined in
diff --git a/src/elementary-number-theory/maximum-rational-numbers.lagda.md b/src/elementary-number-theory/maximum-rational-numbers.lagda.md
index 9bb3eab066..80cde98f19 100644
--- a/src/elementary-number-theory/maximum-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/maximum-rational-numbers.lagda.md
@@ -13,7 +13,9 @@ open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.strict-inequality-rational-numbers
 
 open import foundation.coproduct-types
+open import foundation.dependent-pair-types
 open import foundation.identity-types
+open import foundation.logical-equivalences
 open import foundation.transport-along-identifications
 
 open import order-theory.decidable-total-orders
@@ -114,6 +116,16 @@ abstract
         ( y)
         ( y≤x))
       ( x<z)
+
+  leq-max-leq-both-ℚ : (z x y : ℚ) → leq-ℚ x z → leq-ℚ y z → leq-ℚ (max-ℚ x y) z
+  leq-max-leq-both-ℚ z x y x≤z y≤z =
+    forward-implication
+      ( max-is-least-binary-upper-bound-Decidable-Total-Order
+        ( ℚ-Decidable-Total-Order)
+        ( x)
+        ( y)
+        ( z))
+      ( x≤z , y≤z)
 ```
 
 ### If `a ≤ b` and `c ≤ d`, then `max a c ≤ max b d`
diff --git a/src/elementary-number-theory/nonnegative-integer-fractions.lagda.md b/src/elementary-number-theory/nonnegative-integer-fractions.lagda.md
new file mode 100644
index 0000000000..76b8630dfa
--- /dev/null
+++ b/src/elementary-number-theory/nonnegative-integer-fractions.lagda.md
@@ -0,0 +1,120 @@
+# Nonnegative integer fractions
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module elementary-number-theory.nonnegative-integer-fractions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-integer-fractions
+open import elementary-number-theory.addition-positive-and-negative-integers
+open import elementary-number-theory.integer-fractions
+open import elementary-number-theory.integers
+open import elementary-number-theory.multiplication-integer-fractions
+open import elementary-number-theory.multiplication-integers
+open import elementary-number-theory.multiplication-positive-and-negative-integers
+open import elementary-number-theory.nonnegative-integers
+open import elementary-number-theory.positive-and-negative-integers
+open import elementary-number-theory.positive-integer-fractions
+open import elementary-number-theory.positive-integers
+open import elementary-number-theory.reduced-integer-fractions
+
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.propositions
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+An [integer fraction](elementary-number-theory.integer-fractions.md) `x` is said
+to be
+{{#concept "nonnegative" Disambiguation="integer fraction" Agda=is-nonnegative-fraction-ℤ}}
+if its numerator is a
+[nonnegative integer](elementary-number-theory.nonnegative-integers.md).
+
+## Definitions
+
+### The property of being a nonnegative integer fraction
+
+```agda
+module _
+  (x : fraction-ℤ)
+  where
+
+  is-nonnegative-fraction-ℤ : UU lzero
+  is-nonnegative-fraction-ℤ = is-nonnegative-ℤ (numerator-fraction-ℤ x)
+
+  is-prop-is-nonnegative-fraction-ℤ : is-prop is-nonnegative-fraction-ℤ
+  is-prop-is-nonnegative-fraction-ℤ =
+    is-prop-is-nonnegative-ℤ (numerator-fraction-ℤ x)
+```
+
+## Properties
+
+### An integer fraction similar to a nonnegative integer fraction is nonnegative
+
+```agda
+is-nonnegative-sim-fraction-ℤ :
+  (x y : fraction-ℤ) (S : sim-fraction-ℤ x y) →
+  is-nonnegative-fraction-ℤ x →
+  is-nonnegative-fraction-ℤ y
+is-nonnegative-sim-fraction-ℤ x y S N =
+  is-nonnegative-left-factor-mul-ℤ
+    ( tr
+      ( is-nonnegative-ℤ)
+      ( S)
+      ( is-nonnegative-mul-nonnegative-positive-ℤ
+        ( N)
+        ( is-positive-denominator-fraction-ℤ y)))
+    ( is-positive-denominator-fraction-ℤ x)
+```
+
+### The reduced fraction of a nonnegative integer fraction is nonnegative
+
+```agda
+is-nonnegative-reduce-fraction-ℤ :
+  {x : fraction-ℤ} (P : is-nonnegative-fraction-ℤ x) →
+  is-nonnegative-fraction-ℤ (reduce-fraction-ℤ x)
+is-nonnegative-reduce-fraction-ℤ {x} =
+  is-nonnegative-sim-fraction-ℤ
+    ( x)
+    ( reduce-fraction-ℤ x)
+    ( sim-reduced-fraction-ℤ x)
+```
+
+### The sum of two nonnegative integer fractions is nonnegative
+
+```agda
+is-nonnegative-add-fraction-ℤ :
+  {x y : fraction-ℤ} →
+  is-nonnegative-fraction-ℤ x →
+  is-nonnegative-fraction-ℤ y →
+  is-nonnegative-fraction-ℤ (add-fraction-ℤ x y)
+is-nonnegative-add-fraction-ℤ {x} {y} P Q =
+  is-nonnegative-add-ℤ
+    ( is-nonnegative-mul-nonnegative-positive-ℤ
+      ( P)
+      ( is-positive-denominator-fraction-ℤ y))
+    ( is-nonnegative-mul-nonnegative-positive-ℤ
+      ( Q)
+      ( is-positive-denominator-fraction-ℤ x))
+```
+
+### The product of two nonnegative integer fractions is nonnegative
+
+```agda
+is-nonnegative-mul-nonnegative-fraction-ℤ :
+  {x y : fraction-ℤ} →
+  is-nonnegative-fraction-ℤ x →
+  is-nonnegative-fraction-ℤ y →
+  is-nonnegative-fraction-ℤ (mul-fraction-ℤ x y)
+is-nonnegative-mul-nonnegative-fraction-ℤ = is-nonnegative-mul-ℤ
+```
diff --git a/src/elementary-number-theory/nonnegative-rational-numbers.lagda.md b/src/elementary-number-theory/nonnegative-rational-numbers.lagda.md
new file mode 100644
index 0000000000..808366d930
--- /dev/null
+++ b/src/elementary-number-theory/nonnegative-rational-numbers.lagda.md
@@ -0,0 +1,336 @@
+# Nonnegative rational numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module elementary-number-theory.nonnegative-rational-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-rational-numbers
+open import elementary-number-theory.cross-multiplication-difference-integer-fractions
+open import elementary-number-theory.decidable-total-order-rational-numbers
+open import elementary-number-theory.difference-rational-numbers
+open import elementary-number-theory.inequality-integers
+open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.integer-fractions
+open import elementary-number-theory.integers
+open import elementary-number-theory.multiplication-integer-fractions
+open import elementary-number-theory.multiplication-integers
+open import elementary-number-theory.multiplication-positive-and-negative-integers
+open import elementary-number-theory.multiplication-rational-numbers
+open import elementary-number-theory.nonnegative-integer-fractions
+open import elementary-number-theory.nonnegative-integers
+open import elementary-number-theory.nonzero-rational-numbers
+open import elementary-number-theory.positive-and-negative-integers
+open import elementary-number-theory.positive-integer-fractions
+open import elementary-number-theory.positive-integers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.reduced-integer-fractions
+open import elementary-number-theory.strict-inequality-rational-numbers
+
+open import foundation.binary-transport
+open import foundation.dependent-pair-types
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import order-theory.inflationary-maps-posets
+```
+
+</details>
+
+## Idea
+
+A [rational number](elementary-number-theory.rational-numbers.md) `x` is said to
+be
+{{#concept "nonnegative" Disambiguation="rational number" Agda=is-nonnegative-ℚ}}
+if its numerator is a
+[nonnegative integer](elementary-number-theory.nonnegative-integers.md).
+
+Nonnegative rational numbers are a [subsemigroup](group-theory.subsemigroups.md)
+of the
+[additive monoid of rational numbers](elementary-number-theory.additive-group-of-rational-numbers.md).
+
+## Definitions
+
+### The property of being a nonnegative rational number
+
+```agda
+module _
+  (q : ℚ)
+  where
+
+  is-nonnegative-ℚ : UU lzero
+  is-nonnegative-ℚ = is-nonnegative-fraction-ℤ (fraction-ℚ q)
+
+  is-prop-is-nonnegative-ℚ : is-prop is-nonnegative-ℚ
+  is-prop-is-nonnegative-ℚ = is-prop-is-nonnegative-fraction-ℤ (fraction-ℚ q)
+
+  is-nonnegative-prop-ℚ : Prop lzero
+  pr1 is-nonnegative-prop-ℚ = is-nonnegative-ℚ
+  pr2 is-nonnegative-prop-ℚ = is-prop-is-nonnegative-ℚ
+```
+
+### The type of nonnegative rational numbers
+
+```agda
+nonnegative-ℚ : UU lzero
+nonnegative-ℚ = type-subtype is-nonnegative-prop-ℚ
+
+ℚ⁰⁺ : UU lzero
+ℚ⁰⁺ = nonnegative-ℚ
+
+module _
+  (x : nonnegative-ℚ)
+  where
+
+  rational-ℚ⁰⁺ : ℚ
+  rational-ℚ⁰⁺ = pr1 x
+
+  fraction-ℚ⁰⁺ : fraction-ℤ
+  fraction-ℚ⁰⁺ = fraction-ℚ rational-ℚ⁰⁺
+
+  numerator-ℚ⁰⁺ : ℤ
+  numerator-ℚ⁰⁺ = numerator-ℚ rational-ℚ⁰⁺
+
+  denominator-ℚ⁰⁺ : ℤ
+  denominator-ℚ⁰⁺ = denominator-ℚ rational-ℚ⁰⁺
+
+  is-nonnegative-rational-ℚ⁰⁺ : is-nonnegative-ℚ rational-ℚ⁰⁺
+  is-nonnegative-rational-ℚ⁰⁺ = pr2 x
+
+  is-nonnegative-fraction-ℚ⁰⁺ : is-nonnegative-fraction-ℤ fraction-ℚ⁰⁺
+  is-nonnegative-fraction-ℚ⁰⁺ = pr2 x
+
+  is-nonnegative-numerator-ℚ⁰⁺ : is-nonnegative-ℤ numerator-ℚ⁰⁺
+  is-nonnegative-numerator-ℚ⁰⁺ = is-nonnegative-fraction-ℚ⁰⁺
+
+  is-positive-denominator-ℚ⁰⁺ : is-positive-ℤ denominator-ℚ⁰⁺
+  is-positive-denominator-ℚ⁰⁺ = is-positive-denominator-ℚ rational-ℚ⁰⁺
+
+abstract
+  eq-ℚ⁰⁺ : {x y : ℚ⁰⁺} → rational-ℚ⁰⁺ x ＝ rational-ℚ⁰⁺ y → x ＝ y
+  eq-ℚ⁰⁺ {x} {y} = eq-type-subtype is-nonnegative-prop-ℚ
+
+zero-ℚ⁰⁺ : ℚ⁰⁺
+zero-ℚ⁰⁺ = zero-ℚ , _
+```
+
+## Properties
+
+### The nonnegative rational numbers form a set
+
+```agda
+is-set-ℚ⁰⁺ : is-set ℚ⁰⁺
+is-set-ℚ⁰⁺ = is-set-type-subtype is-nonnegative-prop-ℚ is-set-ℚ
+```
+
+### The rational image of a nonnegative integer is nonnegative
+
+```agda
+abstract
+  is-nonnegative-rational-ℤ :
+    (x : ℤ) → is-nonnegative-ℤ x → is-nonnegative-ℚ (rational-ℤ x)
+  is-nonnegative-rational-ℤ _ H = H
+
+nonnegative-rational-nonnegative-ℤ : nonnegative-ℤ → ℚ⁰⁺
+nonnegative-rational-nonnegative-ℤ (x , x-is-neg) =
+  ( rational-ℤ x , is-nonnegative-rational-ℤ x x-is-neg)
+```
+
+### The rational image of a nonnegative integer fraction is nonnegative
+
+```agda
+abstract
+  is-nonnegative-rational-fraction-ℤ :
+    {x : fraction-ℤ} (P : is-nonnegative-fraction-ℤ x) →
+    is-nonnegative-ℚ (rational-fraction-ℤ x)
+  is-nonnegative-rational-fraction-ℤ {x} =
+    is-nonnegative-sim-fraction-ℤ
+      ( x)
+      ( reduce-fraction-ℤ x)
+      ( sim-reduced-fraction-ℤ x)
+```
+
+### A rational number `x` is nonnegative if and only if `0 ≤ x`
+
+```agda
+module _
+  (x : ℚ)
+  where
+
+  abstract
+    leq-zero-is-nonnegative-ℚ : is-nonnegative-ℚ x → leq-ℚ zero-ℚ x
+    leq-zero-is-nonnegative-ℚ =
+      is-nonnegative-eq-ℤ (inv (cross-mul-diff-zero-fraction-ℤ (fraction-ℚ x)))
+
+    is-nonnegative-leq-zero-ℚ : leq-ℚ zero-ℚ x → is-nonnegative-ℚ x
+    is-nonnegative-leq-zero-ℚ =
+      is-nonnegative-eq-ℤ (cross-mul-diff-zero-fraction-ℤ (fraction-ℚ x))
+
+    is-nonnegative-iff-leq-zero-ℚ : is-nonnegative-ℚ x ↔ leq-ℚ zero-ℚ x
+    is-nonnegative-iff-leq-zero-ℚ =
+      ( leq-zero-is-nonnegative-ℚ ,
+        is-nonnegative-leq-zero-ℚ)
+```
+
+### The difference of a rational number with a rational number less than or equal to the first is nonnegative
+
+```agda
+module _
+  (x y : ℚ) (H : leq-ℚ x y)
+  where
+
+  abstract
+    is-nonnegative-diff-leq-ℚ : is-nonnegative-ℚ (y -ℚ x)
+    is-nonnegative-diff-leq-ℚ =
+      is-nonnegative-leq-zero-ℚ
+        ( y -ℚ x)
+        ( backward-implication (iff-translate-diff-leq-zero-ℚ x y) H)
+
+  nonnegative-diff-le-ℚ : ℚ⁰⁺
+  nonnegative-diff-le-ℚ = (y -ℚ x , is-nonnegative-diff-leq-ℚ)
+```
+
+### The product of two nonnegative rational numbers is nonnegative
+
+```agda
+  is-nonnegative-mul-nonnegative-ℚ :
+    {x y : ℚ} → is-nonnegative-ℚ x → is-nonnegative-ℚ y →
+    is-nonnegative-ℚ (x *ℚ y)
+  is-nonnegative-mul-nonnegative-ℚ {x} {y} P Q =
+    is-nonnegative-rational-fraction-ℤ
+      ( is-nonnegative-mul-nonnegative-fraction-ℤ
+        { fraction-ℚ x}
+        { fraction-ℚ y}
+        ( P)
+        ( Q))
+```
+
+### Multiplication by a nonnegative rational number preserves inequality
+
+```agda
+abstract
+  preserves-leq-right-mul-ℚ⁰⁺ :
+    (p : ℚ⁰⁺) (q r : ℚ) → leq-ℚ q r →
+    leq-ℚ (q *ℚ rational-ℚ⁰⁺ p) (r *ℚ rational-ℚ⁰⁺ p)
+  preserves-leq-right-mul-ℚ⁰⁺
+    p⁺@((p@(np , dp , pos-dp) , _) , nonneg-np)
+    (q@(nq , dq , _) , _)
+    (r@(nr , dr , _) , _)
+    q≤r =
+      preserves-leq-rational-fraction-ℤ
+        ( mul-fraction-ℤ q p)
+        ( mul-fraction-ℤ r p)
+        ( binary-tr
+          ( leq-ℤ)
+          ( interchange-law-mul-mul-ℤ _ _ _ _)
+          ( interchange-law-mul-mul-ℤ _ _ _ _)
+          ( preserves-leq-left-mul-nonnegative-ℤ
+            ( np *ℤ dp ,
+              is-nonnegative-mul-nonnegative-positive-ℤ nonneg-np pos-dp)
+            ( nq *ℤ dr)
+            ( nr *ℤ dq)
+            ( q≤r)))
+
+  preserves-leq-left-mul-ℚ⁰⁺ :
+    (p : ℚ⁰⁺) (q r : ℚ) → leq-ℚ q r →
+    leq-ℚ (rational-ℚ⁰⁺ p *ℚ q) (rational-ℚ⁰⁺ p *ℚ r)
+  preserves-leq-left-mul-ℚ⁰⁺ p q r q≤r =
+    binary-tr
+      ( leq-ℚ)
+      ( commutative-mul-ℚ q (rational-ℚ⁰⁺ p))
+      ( commutative-mul-ℚ r (rational-ℚ⁰⁺ p))
+      ( preserves-leq-right-mul-ℚ⁰⁺ p q r q≤r)
+```
+
+### Addition on nonnegative rational numbers
+
+```agda
+abstract
+  is-nonnegative-add-ℚ :
+    (p q : ℚ) → is-nonnegative-ℚ p → is-nonnegative-ℚ q →
+    is-nonnegative-ℚ (p +ℚ q)
+  is-nonnegative-add-ℚ p q nonneg-p nonneg-q =
+    is-nonnegative-rational-fraction-ℤ
+      ( is-nonnegative-add-fraction-ℤ
+        { fraction-ℚ p}
+        { fraction-ℚ q}
+        ( nonneg-p)
+        ( nonneg-q))
+
+add-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺
+add-ℚ⁰⁺ (p , nonneg-p) (q , nonneg-q) =
+  ( p +ℚ q , is-nonnegative-add-ℚ p q nonneg-p nonneg-q)
+
+infixl 35 _+ℚ⁰⁺_
+_+ℚ⁰⁺_ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺
+_+ℚ⁰⁺_ = add-ℚ⁰⁺
+```
+
+### Multiplication on nonnegative rational numbers
+
+```agda
+abstract
+  is-nonnegative-mul-ℚ :
+    (p q : ℚ) → is-nonnegative-ℚ p → is-nonnegative-ℚ q →
+    is-nonnegative-ℚ (p *ℚ q)
+  is-nonnegative-mul-ℚ p q nonneg-p nonneg-q =
+    is-nonnegative-rational-fraction-ℤ
+      ( is-nonnegative-mul-nonnegative-fraction-ℤ
+        { fraction-ℚ p}
+        { fraction-ℚ q}
+        ( nonneg-p)
+        ( nonneg-q))
+
+mul-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺
+mul-ℚ⁰⁺ (p , nonneg-p) (q , nonneg-q) =
+  ( p *ℚ q , is-nonnegative-mul-ℚ p q nonneg-p nonneg-q)
+
+infixl 35 _*ℚ⁰⁺_
+_*ℚ⁰⁺_ : ℚ⁰⁺ → ℚ⁰⁺ → ℚ⁰⁺
+_*ℚ⁰⁺_ = mul-ℚ⁰⁺
+```
+
+### Inequality on nonnegative rational numbers
+
+```agda
+leq-ℚ⁰⁺-Prop : ℚ⁰⁺ → ℚ⁰⁺ → Prop lzero
+leq-ℚ⁰⁺-Prop (p , _) (q , _) = leq-ℚ-Prop p q
+
+leq-ℚ⁰⁺ : ℚ⁰⁺ → ℚ⁰⁺ → UU lzero
+leq-ℚ⁰⁺ (p , _) (q , _) = leq-ℚ p q
+```
+
+### Addition of a nonnegative rational number is an increasing map
+
+```agda
+abstract
+  is-inflationary-map-left-add-rational-ℚ⁰⁺ :
+    (p : ℚ⁰⁺) → is-inflationary-map-Poset ℚ-Poset (rational-ℚ⁰⁺ p +ℚ_)
+  is-inflationary-map-left-add-rational-ℚ⁰⁺ (p , nonneg-p) q =
+    tr
+      ( λ r → leq-ℚ r (p +ℚ q))
+      ( left-unit-law-add-ℚ q)
+      ( preserves-leq-left-add-ℚ
+        ( q)
+        ( zero-ℚ)
+        ( p)
+        ( leq-zero-is-nonnegative-ℚ p nonneg-p))
+
+  is-inflationary-map-right-add-rational-ℚ⁰⁺ :
+    (p : ℚ⁰⁺) → is-inflationary-map-Poset ℚ-Poset (_+ℚ rational-ℚ⁰⁺ p)
+  is-inflationary-map-right-add-rational-ℚ⁰⁺ p q =
+    tr
+      ( leq-ℚ q)
+      ( commutative-add-ℚ (rational-ℚ⁰⁺ p) q)
+      ( is-inflationary-map-left-add-rational-ℚ⁰⁺ p q)
+```