diff --git a/src/elementary-number-theory/additive-group-of-rational-numbers.lagda.md b/src/elementary-number-theory/additive-group-of-rational-numbers.lagda.md
index 60aeaf1fb9..e0e8513c49 100644
--- a/src/elementary-number-theory/additive-group-of-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/additive-group-of-rational-numbers.lagda.md
@@ -17,6 +17,7 @@ open import foundation.unital-binary-operations
 open import foundation.universe-levels
 
 open import group-theory.abelian-groups
+open import group-theory.commutative-monoids
 open import group-theory.groups
 open import group-theory.monoids
 open import group-theory.semigroups
@@ -60,9 +61,13 @@ pr2 (pr2 (pr2 (pr2 group-add-ℚ))) = right-inverse-law-add-ℚ
 
 ## Properties
 
-### Tha additive group of rational numbers is commutative
+### The additive group of rational numbers is commutative
 
 ```agda
+commutative-monoid-add-ℚ : Commutative-Monoid lzero
+pr1 commutative-monoid-add-ℚ = monoid-add-ℚ
+pr2 commutative-monoid-add-ℚ = commutative-add-ℚ
+
 abelian-group-add-ℚ : Ab lzero
 pr1 abelian-group-add-ℚ = group-add-ℚ
 pr2 abelian-group-add-ℚ = commutative-add-ℚ
diff --git a/src/elementary-number-theory/positive-rational-numbers.lagda.md b/src/elementary-number-theory/positive-rational-numbers.lagda.md
index 63ae446cfa..88b15da00e 100644
--- a/src/elementary-number-theory/positive-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/positive-rational-numbers.lagda.md
@@ -190,13 +190,14 @@ module _
   (x y : ℚ) (H : le-ℚ x y)
   where
 
-  is-positive-diff-le-ℚ : is-positive-ℚ (y -ℚ x)
-  is-positive-diff-le-ℚ =
-    is-positive-le-zero-ℚ
-      ( y -ℚ x)
-      ( backward-implication
-        ( iff-translate-diff-le-zero-ℚ x y)
-        ( H))
+  abstract
+    is-positive-diff-le-ℚ : is-positive-ℚ (y -ℚ x)
+    is-positive-diff-le-ℚ =
+      is-positive-le-zero-ℚ
+        ( y -ℚ x)
+        ( backward-implication
+          ( iff-translate-diff-le-zero-ℚ x y)
+          ( H))
 
   positive-diff-le-ℚ : ℚ⁺
   positive-diff-le-ℚ = y -ℚ x , is-positive-diff-le-ℚ
@@ -539,12 +540,13 @@ mediant-zero-ℚ⁺ x =
         ( rational-ℚ⁺ x)
         ( le-zero-is-positive-ℚ (rational-ℚ⁺ x) (is-positive-rational-ℚ⁺ x))))
 
-le-mediant-zero-ℚ⁺ : (x : ℚ⁺) → le-ℚ⁺ (mediant-zero-ℚ⁺ x) x
-le-mediant-zero-ℚ⁺ x =
-  le-right-mediant-ℚ
-    ( zero-ℚ)
-    ( rational-ℚ⁺ x)
-    ( le-zero-is-positive-ℚ (rational-ℚ⁺ x) (is-positive-rational-ℚ⁺ x))
+abstract
+  le-mediant-zero-ℚ⁺ : (x : ℚ⁺) → le-ℚ⁺ (mediant-zero-ℚ⁺ x) x
+  le-mediant-zero-ℚ⁺ x =
+    le-right-mediant-ℚ
+      ( zero-ℚ)
+      ( rational-ℚ⁺ x)
+      ( le-zero-is-positive-ℚ (rational-ℚ⁺ x) (is-positive-rational-ℚ⁺ x))
 ```
 
 ### Any positive rational number is the sum of two positive rational numbers
diff --git a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md
index 99d4619055..53e20051b7 100644
--- a/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md
+++ b/src/elementary-number-theory/strict-inequality-rational-numbers.lagda.md
@@ -122,12 +122,13 @@ module _
   (x y z : ℚ)
   where
 
-  transitive-le-ℚ : le-ℚ y z → le-ℚ x y → le-ℚ x z
-  transitive-le-ℚ =
-    transitive-le-fraction-ℤ
-      ( fraction-ℚ x)
-      ( fraction-ℚ y)
-      ( fraction-ℚ z)
+  abstract
+    transitive-le-ℚ : le-ℚ y z → le-ℚ x y → le-ℚ x z
+    transitive-le-ℚ =
+      transitive-le-fraction-ℤ
+        ( fraction-ℚ x)
+        ( fraction-ℚ y)
+        ( fraction-ℚ z)
 ```
 
 ### Concatenation rules for inequality and strict inequality on the rational numbers
@@ -315,15 +316,16 @@ module _
 ### Addition on the rational numbers preserves strict inequality
 
 ```agda
-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-le-right-add-ℚ b c d K)
-    ( preserves-le-left-add-ℚ c a b H)
+abstract
+  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-le-right-add-ℚ b c d K)
+      ( preserves-le-left-add-ℚ c a b H)
 ```
 
 ### The rational numbers have no lower or upper bound
diff --git a/src/foundation/existential-quantification.lagda.md b/src/foundation/existential-quantification.lagda.md
index a15d2258a9..07e29f4bb7 100644
--- a/src/foundation/existential-quantification.lagda.md
+++ b/src/foundation/existential-quantification.lagda.md
@@ -202,6 +202,11 @@ module _
         ( elim-exists Q)
 ```
 
+Note that since existential quantification is implemented using propositional
+truncation, the associated
+[do syntax](foundation.propositional-truncations.md#do-syntax) can be used to
+simplify deeply nested chains of `elim-exists`.
+
 ### The existential quantification satisfies the universal property of existential quantification
 
 ```agda
diff --git a/src/foundation/propositional-truncations.lagda.md b/src/foundation/propositional-truncations.lagda.md
index 1181cc2572..8580a7744a 100644
--- a/src/foundation/propositional-truncations.lagda.md
+++ b/src/foundation/propositional-truncations.lagda.md
@@ -446,6 +446,83 @@ module _
     is-equiv-map-inv-trunc-Prop-diagonal-coproduct
 ```
 
+## `do` syntax for propositional truncation { #do-syntax }
+
+[Agda's `do` syntax](https://agda.readthedocs.io/en/v2.7.0/language/syntactic-sugar.html#do-notation)
+is a handy tool to avoid deeply nesting calls to the same lambda-based function.
+For example, consider a case where you are trying to prove a proposition,
+`motive : Prop l`, from witnesses of propositional truncations of types `P` and
+`Q`:
+
+```text
+rec-trunc-Prop
+  ( motive)
+  ( λ (p : P) →
+    rec-trunc-Prop
+      ( motive)
+      ( λ (q : Q) → witness-motive-P-Q p q)
+      ( witness-truncated-prop-Q p))
+  ( witness-truncated-prop-P)
+```
+
+The tower of indentation, with many layers of indentation in the innermost
+derivation, is a little awkward even at two levels, let alone more. In
+particular, we have the many duplicated lines of `rec-trunc-Prop motive`, and
+the increasing distance between the `rec-trunc-Prop` and the `trunc-Prop` being
+recursed on. Agda's `do` syntax offers us an alternative.
+
+```agda
+module do-syntax-trunc-Prop {l : Level} (motive : Prop l) where
+  _>>=_ :
+    {l : Level} {A : UU l} →
+    type-trunc-Prop A → (A → type-Prop motive) →
+    type-Prop motive
+  trunc-prop-a >>= k = rec-trunc-Prop motive k trunc-prop-a
+```
+
+This allows us to rewrite the nested chain above as
+
+```text
+do
+  p ← witness-truncated-prop-P
+  q ← witness-truncated-prop-Q p
+  witness-motive-P-Q p q
+where open do-syntax-trunc-Prop motive
+```
+
+Since Agda's `do` syntax desugars to calls to `>>=`, this is syntactic sugar for
+
+```text
+witness-truncated-prop-P >>=
+  ( λ p → witness-truncated-prop-Q p >>=
+    ( λ q → witness-motive-P-Q p q))
+```
+
+which, inlining the definition of `>>=`, becomes exactly the chain of
+`rec-trunc-Prop` used above.
+
+To read the `do` syntax, it may help to go through each line:
+
+1. `do` indicates that we will be using Agda's syntactic sugar for the `>>=`
+   function defined in the `do-syntax-trunc-Prop` module.
+1. You can read the `p ← witness-truncated-prop-P` as an _instruction_ saying,
+   "Get the value `p` out of the witness of `trunc-Prop P`." We cannot extract
+   elements out of witnesses of propositionally truncated types, but since we're
+   eliminating into a proposition, the universal property of the truncation
+   allows us to lift a map from the untruncated type to a map from its
+   truncation.
+1. `q ← witness-truncated-prop-Q p` says, "Get the value `q` out of the witness
+   for the truncation `witness-truncated-prop-Q p`" --- noticing that we can
+   make use of `p : P` in that line.
+1. `witness-motive-P-Q p q` must give us a witness of `motive` --- that is, a
+   value of type `type-Prop motive` --- from `p` and `q`.
+1. `where open do-syntax-trunc-Prop motive` is required to allow us to use the
+   `do` syntax.
+
+The result of the entire `do` block is the value of type `type-Prop motive`,
+which is internally constructed with an appropriate chain of `rec-trunc-Prop`
+from the intermediate steps.
+
 ## Table of files about propositional logic
 
 The following table gives an overview of basic constructions in propositional
diff --git a/src/group-theory/abelian-groups.lagda.md b/src/group-theory/abelian-groups.lagda.md
index 6023e6276d..7033d0b8db 100644
--- a/src/group-theory/abelian-groups.lagda.md
+++ b/src/group-theory/abelian-groups.lagda.md
@@ -612,17 +612,18 @@ module _
   {l : Level} (A : Ab l)
   where
 
-  is-identity-left-conjugation-Ab :
-    (x : type-Ab A) → left-conjugation-Ab A x ~ id
-  is-identity-left-conjugation-Ab x y =
-    ( ap (add-Ab' A (neg-Ab A x)) (commutative-add-Ab A x y)) ∙
-    ( is-retraction-right-subtraction-Ab A x y)
-
-  is-identity-right-conjugation-Ab :
-    (x : type-Ab A) → right-conjugation-Ab A x ~ id
-  is-identity-right-conjugation-Ab x =
-    inv-htpy (left-right-conjugation-Ab A x) ∙h
-    is-identity-left-conjugation-Ab x
+  abstract
+    is-identity-left-conjugation-Ab :
+      (x : type-Ab A) → left-conjugation-Ab A x ~ id
+    is-identity-left-conjugation-Ab x y =
+      ( ap (add-Ab' A (neg-Ab A x)) (commutative-add-Ab A x y)) ∙
+      ( is-retraction-right-subtraction-Ab A x y)
+
+    is-identity-right-conjugation-Ab :
+      (x : type-Ab A) → right-conjugation-Ab A x ~ id
+    is-identity-right-conjugation-Ab x =
+      inv-htpy (left-right-conjugation-Ab A x) ∙h
+      is-identity-left-conjugation-Ab x
 
   is-identity-conjugation-Ab :
     (x : type-Ab A) → conjugation-Ab A x ~ id
diff --git a/src/real-numbers.lagda.md b/src/real-numbers.lagda.md
index 9f3700a10d..24d0f66b34 100644
--- a/src/real-numbers.lagda.md
+++ b/src/real-numbers.lagda.md
@@ -5,6 +5,8 @@
 ```agda
 module real-numbers where
 
+open import real-numbers.addition-lower-dedekind-real-numbers public
+open import real-numbers.addition-upper-dedekind-real-numbers public
 open import real-numbers.apartness-real-numbers public
 open import real-numbers.arithmetically-located-dedekind-cuts public
 open import real-numbers.dedekind-real-numbers public
diff --git a/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md
new file mode 100644
index 0000000000..652c87812c
--- /dev/null
+++ b/src/real-numbers/addition-lower-dedekind-real-numbers.lagda.md
@@ -0,0 +1,243 @@
+# Addition of lower Dedekind real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.addition-lower-dedekind-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-rational-numbers
+open import elementary-number-theory.additive-group-of-rational-numbers
+open import elementary-number-theory.difference-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.strict-inequality-rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
+open import foundation.cartesian-product-types
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.propositional-truncations
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import group-theory.abelian-groups
+open import group-theory.groups
+open import group-theory.minkowski-multiplication-commutative-monoids
+
+open import logic.functoriality-existential-quantification
+
+open import real-numbers.lower-dedekind-real-numbers
+open import real-numbers.rational-lower-dedekind-real-numbers
+```
+
+</details>
+
+## Idea
+
+The sum of two
+[lower Dedekind real numbers](real-numbers.lower-dedekind-real-numbers.md) is
+the
+[Minkowski sum](group-theory.minkowski-multiplication-commutative-monoids.md) of
+their cuts.
+
+```agda
+module _
+  {l1 l2 : Level}
+  (x : lower-ℝ l1)
+  (y : lower-ℝ l2)
+  where
+
+  cut-add-lower-ℝ : subtype (l1 ⊔ l2) ℚ
+  cut-add-lower-ℝ =
+    minkowski-mul-Commutative-Monoid
+      ( commutative-monoid-add-ℚ)
+      ( cut-lower-ℝ x)
+      ( cut-lower-ℝ y)
+
+  is-in-cut-add-lower-ℝ : ℚ → UU (l1 ⊔ l2)
+  is-in-cut-add-lower-ℝ = is-in-subtype cut-add-lower-ℝ
+
+  is-inhabited-cut-add-lower-ℝ : exists ℚ cut-add-lower-ℝ
+  is-inhabited-cut-add-lower-ℝ =
+    minkowski-mul-inhabited-is-inhabited-Commutative-Monoid
+      ( commutative-monoid-add-ℚ)
+      ( cut-lower-ℝ x)
+      ( cut-lower-ℝ y)
+      ( is-inhabited-cut-lower-ℝ x)
+      ( is-inhabited-cut-lower-ℝ y)
+
+  abstract
+    is-rounded-cut-add-lower-ℝ :
+      (q : ℚ) →
+      is-in-cut-add-lower-ℝ q ↔
+      exists ℚ (λ r → le-ℚ-Prop q r ∧ cut-add-lower-ℝ r)
+    pr1 (is-rounded-cut-add-lower-ℝ q) q<x+y =
+      do
+        ((lx , ly) , (lx<x , ly<y , q=lx+ly)) ← q<x+y
+        (lx' , lx<lx' , lx'<x) ←
+          forward-implication (is-rounded-cut-lower-ℝ x lx) lx<x
+        (ly' , ly<ly' , ly'<y) ←
+          forward-implication (is-rounded-cut-lower-ℝ y ly) ly<y
+        intro-exists
+          ( lx' +ℚ ly')
+          ( tr
+              ( λ p → le-ℚ p (lx' +ℚ ly'))
+              ( inv q=lx+ly)
+              ( preserves-le-add-ℚ {lx} {lx'} {ly} {ly'} lx<lx' ly<ly') ,
+            intro-exists (lx' , ly') (lx'<x , ly'<y , refl))
+      where
+        open
+          do-syntax-trunc-Prop (∃ ℚ (λ r → le-ℚ-Prop q r ∧ cut-add-lower-ℝ r))
+    pr2 (is-rounded-cut-add-lower-ℝ q) exists-r =
+      do
+        (r , q<r , r<x+y) ← exists-r
+        ((rx , ry) , (rx<x , ry<y , r=rx+ry)) ← r<x+y
+        let
+          r-q⁺ = positive-diff-le-ℚ q r q<r
+          ε⁺ = mediant-zero-ℚ⁺ r-q⁺
+          ε = rational-ℚ⁺ ε⁺
+          ε<r-q = le-mediant-zero-ℚ⁺ r-q⁺
+        intro-exists
+          ( rx -ℚ ε , q -ℚ (rx -ℚ ε))
+          ( is-in-cut-diff-rational-ℚ⁺-lower-ℝ x rx ε⁺ rx<x ,
+            is-in-cut-le-ℚ-lower-ℝ
+              ( y)
+              ( q -ℚ (rx -ℚ ε))
+              ( ry)
+              ( binary-tr
+                ( le-ℚ)
+                ( equational-reasoning
+                  (q -ℚ rx) +ℚ ε
+                  ＝ q +ℚ (neg-ℚ rx +ℚ ε)
+                    by associative-add-ℚ q (neg-ℚ rx) ε
+                  ＝ q +ℚ (ε -ℚ rx)
+                    by ap (q +ℚ_) (commutative-add-ℚ (neg-ℚ rx) ε)
+                  ＝ q -ℚ (rx -ℚ ε)
+                    by ap (q +ℚ_) (inv (distributive-neg-diff-ℚ rx ε)))
+                ( equational-reasoning
+                  (q -ℚ rx) +ℚ (r -ℚ q)
+                  ＝ (q -ℚ rx) -ℚ (q -ℚ r)
+                    by ap ((q -ℚ rx) +ℚ_) (inv (distributive-neg-diff-ℚ q r))
+                  ＝ neg-ℚ rx -ℚ neg-ℚ r
+                    by left-translation-diff-ℚ (neg-ℚ rx) (neg-ℚ r) q
+                  ＝ neg-ℚ rx +ℚ (rx +ℚ ry)
+                    by ap (neg-ℚ rx +ℚ_) (neg-neg-ℚ r ∙ r=rx+ry)
+                  ＝ ry
+                    by is-retraction-left-div-Group group-add-ℚ rx ry)
+                ( preserves-le-right-add-ℚ (q -ℚ rx) ε (r -ℚ q) ε<r-q))
+              ( ry<y) ,
+            inv
+              ( is-identity-right-conjugation-Ab
+                ( abelian-group-add-ℚ)
+                ( rx -ℚ ε)
+                ( q)))
+      where open do-syntax-trunc-Prop (cut-add-lower-ℝ q)
+
+  add-lower-ℝ : lower-ℝ (l1 ⊔ l2)
+  pr1 add-lower-ℝ = cut-add-lower-ℝ
+  pr1 (pr2 add-lower-ℝ) = is-inhabited-cut-add-lower-ℝ
+  pr2 (pr2 add-lower-ℝ) = is-rounded-cut-add-lower-ℝ
+```
+
+## Properties
+
+### Addition of lower Dedekind real numbers is commutative
+
+```agda
+module _
+  {l1 l2 : Level} (x : lower-ℝ l1) (y : lower-ℝ l2)
+  where
+
+  commutative-add-lower-ℝ : add-lower-ℝ x y ＝ add-lower-ℝ y x
+  commutative-add-lower-ℝ =
+    eq-eq-cut-lower-ℝ
+      ( add-lower-ℝ x y)
+      ( add-lower-ℝ y x)
+      ( commutative-minkowski-mul-Commutative-Monoid
+        ( commutative-monoid-add-ℚ)
+        ( cut-lower-ℝ x)
+        ( cut-lower-ℝ y))
+```
+
+### Addition of lower Dedekind real numbers is associative
+
+```agda
+module _
+  {l1 l2 l3 : Level} (x : lower-ℝ l1) (y : lower-ℝ l2) (z : lower-ℝ l3)
+  where
+
+  associative-add-lower-ℝ :
+    add-lower-ℝ (add-lower-ℝ x y) z ＝ add-lower-ℝ x (add-lower-ℝ y z)
+  associative-add-lower-ℝ =
+    eq-eq-cut-lower-ℝ
+      ( add-lower-ℝ (add-lower-ℝ x y) z)
+      ( add-lower-ℝ x (add-lower-ℝ y z))
+      ( associative-minkowski-mul-Commutative-Monoid
+        ( commutative-monoid-add-ℚ)
+        ( cut-lower-ℝ x)
+        ( cut-lower-ℝ y)
+        ( cut-lower-ℝ z))
+```
+
+### Unit laws for the addition of lower Dedekind real numbers
+
+```agda
+module _
+  {l : Level} (x : lower-ℝ l)
+  where
+
+  abstract
+    right-unit-law-add-lower-ℝ : add-lower-ℝ x (lower-real-ℚ zero-ℚ) ＝ x
+    right-unit-law-add-lower-ℝ =
+      eq-sim-cut-lower-ℝ
+        ( add-lower-ℝ x (lower-real-ℚ zero-ℚ))
+        ( x)
+        ( (λ r →
+            elim-exists
+              ( cut-lower-ℝ x r)
+              ( λ (p , q) (p<x , q<0 , r=p+q) →
+                inv-tr
+                  ( is-in-cut-lower-ℝ x)
+                  ( r=p+q ∙ ap (p +ℚ_) (inv (neg-neg-ℚ q)))
+                  ( is-in-cut-diff-rational-ℚ⁺-lower-ℝ
+                    ( x)
+                    ( p)
+                    ( neg-ℚ q ,
+                      is-positive-le-zero-ℚ (neg-ℚ q) (neg-le-ℚ q zero-ℚ q<0))
+                    ( p<x)))) ,
+          (λ p p<x →
+            elim-exists
+              ( cut-add-lower-ℝ x (lower-real-ℚ zero-ℚ) p)
+              ( λ q (p<q , q<x) →
+                intro-exists
+                  ( q , p -ℚ q)
+                  ( q<x ,
+                    tr
+                      ( λ r → le-ℚ r zero-ℚ)
+                      ( distributive-neg-diff-ℚ q p)
+                      ( neg-le-ℚ
+                        ( zero-ℚ)
+                        ( q -ℚ p)
+                        ( backward-implication
+                          ( iff-translate-diff-le-zero-ℚ p q)
+                          ( p<q))) ,
+                    inv
+                      ( is-identity-right-conjugation-Ab
+                        ( abelian-group-add-ℚ)
+                        ( q)
+                        ( p))))
+              ( forward-implication (is-rounded-cut-lower-ℝ x p) p<x)))
+
+  left-unit-law-add-lower-ℝ : add-lower-ℝ (lower-real-ℚ zero-ℚ) x ＝ x
+  left-unit-law-add-lower-ℝ =
+    commutative-add-lower-ℝ (lower-real-ℚ zero-ℚ) x ∙ right-unit-law-add-lower-ℝ
+```
diff --git a/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md b/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md
new file mode 100644
index 0000000000..33dd0ded7d
--- /dev/null
+++ b/src/real-numbers/addition-upper-dedekind-real-numbers.lagda.md
@@ -0,0 +1,227 @@
+# Addition of upper Dedekind real numbers
+
+```agda
+{-# OPTIONS --lossy-unification #-}
+
+module real-numbers.addition-upper-dedekind-real-numbers where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.addition-rational-numbers
+open import elementary-number-theory.additive-group-of-rational-numbers
+open import elementary-number-theory.difference-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
+open import elementary-number-theory.rational-numbers
+open import elementary-number-theory.strict-inequality-rational-numbers
+
+open import foundation.action-on-identifications-functions
+open import foundation.binary-transport
+open import foundation.cartesian-product-types
+open import foundation.conjunction
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.identity-types
+open import foundation.logical-equivalences
+open import foundation.propositional-truncations
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+
+open import group-theory.abelian-groups
+open import group-theory.groups
+open import group-theory.minkowski-multiplication-commutative-monoids
+
+open import real-numbers.rational-upper-dedekind-real-numbers
+open import real-numbers.upper-dedekind-real-numbers
+```
+
+</details>
+
+## Idea
+
+The sum of two
+[upper Dedekind real numbers](real-numbers.upper-dedekind-real-numbers.md) is
+the
+[Minkowski sum](group-theory.minkowski-multiplication-commutative-monoids.md) of
+their cuts.
+
+```agda
+module _
+  {l1 l2 : Level}
+  (x : upper-ℝ l1)
+  (y : upper-ℝ l2)
+  where
+
+  cut-add-upper-ℝ : subtype (l1 ⊔ l2) ℚ
+  cut-add-upper-ℝ =
+    minkowski-mul-Commutative-Monoid
+      ( commutative-monoid-add-ℚ)
+      ( cut-upper-ℝ x)
+      ( cut-upper-ℝ y)
+
+  is-in-cut-add-upper-ℝ : ℚ → UU (l1 ⊔ l2)
+  is-in-cut-add-upper-ℝ = is-in-subtype cut-add-upper-ℝ
+
+  is-inhabited-cut-add-upper-ℝ : exists ℚ cut-add-upper-ℝ
+  is-inhabited-cut-add-upper-ℝ =
+    minkowski-mul-inhabited-is-inhabited-Commutative-Monoid
+      ( commutative-monoid-add-ℚ)
+      ( cut-upper-ℝ x)
+      ( cut-upper-ℝ y)
+      ( is-inhabited-cut-upper-ℝ x)
+      ( is-inhabited-cut-upper-ℝ y)
+
+  abstract
+    is-rounded-cut-add-upper-ℝ :
+      (q : ℚ) →
+      is-in-cut-add-upper-ℝ q ↔
+      exists ℚ (λ p → le-ℚ-Prop p q ∧ cut-add-upper-ℝ p)
+    pr1 (is-rounded-cut-add-upper-ℝ q) q<x+y =
+      do
+        ((ux , uy) , (x<ux , y<uy , q=ux+uy)) ← q<x+y
+        (ux' , ux'<ux , x<ux') ←
+          forward-implication (is-rounded-cut-upper-ℝ x ux) x<ux
+        (uy' , uy'<uy , y<uy') ←
+          forward-implication (is-rounded-cut-upper-ℝ y uy) y<uy
+        intro-exists
+          ( ux' +ℚ uy')
+          ( tr
+              ( le-ℚ (ux' +ℚ uy'))
+              ( inv (q=ux+uy))
+              ( preserves-le-add-ℚ {ux'} {ux} {uy'} {uy} ux'<ux uy'<uy) ,
+            intro-exists (ux' , uy') (x<ux' , y<uy' , refl))
+      where
+        open
+          do-syntax-trunc-Prop (∃ ℚ (λ p → le-ℚ-Prop p q ∧ cut-add-upper-ℝ p))
+    pr2 (is-rounded-cut-add-upper-ℝ q) exists-p =
+      do
+        (p , p<q , x+y<p) ← exists-p
+        ((px , py) , (x<px , y<py , p=px+py)) ← x+y<p
+        let
+          q-p⁺ = positive-diff-le-ℚ p q p<q
+          ε⁺ = mediant-zero-ℚ⁺ q-p⁺
+          ε = rational-ℚ⁺ ε⁺
+          ε<q-p = le-mediant-zero-ℚ⁺ q-p⁺
+        intro-exists
+          ( px +ℚ ε , q -ℚ (px +ℚ ε))
+          ( is-in-cut-add-rational-ℚ⁺-upper-ℝ x px ε⁺ x<px ,
+            is-in-cut-le-ℚ-upper-ℝ
+              ( y)
+              ( py)
+              ( q -ℚ (px +ℚ ε))
+              ( binary-tr
+                ( le-ℚ)
+                ( equational-reasoning
+                    (q -ℚ px) -ℚ (q -ℚ p)
+                    ＝ neg-ℚ px -ℚ neg-ℚ p
+                      by left-translation-diff-ℚ (neg-ℚ px) (neg-ℚ p) q
+                    ＝ neg-ℚ px +ℚ (px +ℚ py)
+                      by ap (neg-ℚ px +ℚ_) (neg-neg-ℚ p ∙ p=px+py)
+                    ＝ py
+                      by is-retraction-left-div-Group group-add-ℚ px py)
+                ( equational-reasoning
+                  (q -ℚ px) -ℚ ε
+                  ＝ q +ℚ (neg-ℚ px +ℚ neg-ℚ ε)
+                    by associative-add-ℚ q (neg-ℚ px) (neg-ℚ ε)
+                  ＝ q -ℚ (px +ℚ ε)
+                    by ap (q +ℚ_) (inv (distributive-neg-add-ℚ px ε)))
+                ( preserves-le-right-add-ℚ
+                  ( q -ℚ px)
+                  ( neg-ℚ (q -ℚ p))
+                  ( neg-ℚ ε)
+                  ( neg-le-ℚ ε (q -ℚ p) ε<q-p)))
+              ( y<py) ,
+            inv
+              ( is-identity-right-conjugation-Ab
+                ( abelian-group-add-ℚ)
+                ( px +ℚ ε)
+                ( q)))
+      where open do-syntax-trunc-Prop (cut-add-upper-ℝ q)
+
+  add-upper-ℝ : upper-ℝ (l1 ⊔ l2)
+  pr1 add-upper-ℝ = cut-add-upper-ℝ
+  pr1 (pr2 add-upper-ℝ) = is-inhabited-cut-add-upper-ℝ
+  pr2 (pr2 add-upper-ℝ) = is-rounded-cut-add-upper-ℝ
+```
+
+## Properties
+
+### Addition of upper Dedekind real numbers is commutative
+
+```agda
+module _
+  {l1 l2 : Level} (x : upper-ℝ l1) (y : upper-ℝ l2)
+  where
+
+  commutative-add-upper-ℝ : add-upper-ℝ x y ＝ add-upper-ℝ y x
+  commutative-add-upper-ℝ =
+    eq-eq-cut-upper-ℝ
+      ( add-upper-ℝ x y)
+      ( add-upper-ℝ y x)
+      ( commutative-minkowski-mul-Commutative-Monoid
+        ( commutative-monoid-add-ℚ)
+        ( cut-upper-ℝ x)
+        ( cut-upper-ℝ y))
+```
+
+### Addition of upper Dedekind real numbers is associative
+
+```agda
+module _
+  {l1 l2 l3 : Level} (x : upper-ℝ l1) (y : upper-ℝ l2) (z : upper-ℝ l3)
+  where
+
+  associative-add-upper-ℝ :
+    add-upper-ℝ (add-upper-ℝ x y) z ＝ add-upper-ℝ x (add-upper-ℝ y z)
+  associative-add-upper-ℝ =
+    eq-eq-cut-upper-ℝ
+      ( add-upper-ℝ (add-upper-ℝ x y) z)
+      ( add-upper-ℝ x (add-upper-ℝ y z))
+      ( associative-minkowski-mul-Commutative-Monoid
+        ( commutative-monoid-add-ℚ)
+        ( cut-upper-ℝ x)
+        ( cut-upper-ℝ y)
+        ( cut-upper-ℝ z))
+```
+
+### Unit laws for addition of upper Dedekind real numbers
+
+```agda
+module _
+  {l : Level} (x : upper-ℝ l)
+  where
+
+  right-unit-law-add-upper-ℝ : add-upper-ℝ x (upper-real-ℚ zero-ℚ) ＝ x
+  right-unit-law-add-upper-ℝ =
+    eq-sim-cut-upper-ℝ
+      ( add-upper-ℝ x (upper-real-ℚ zero-ℚ))
+      ( x)
+      ( (λ r →
+          elim-exists
+            ( cut-upper-ℝ x r)
+            ( λ (p , q) (x<p , 0<q , r=p+q) →
+              inv-tr
+                ( is-in-cut-upper-ℝ x)
+                ( r=p+q)
+                ( is-in-cut-add-rational-ℚ⁺-upper-ℝ
+                  ( x)
+                  ( p)
+                  ( q , is-positive-le-zero-ℚ q 0<q)
+                  ( x<p)))) ,
+        ( λ q x<q →
+          elim-exists
+            ( cut-add-upper-ℝ x (upper-real-ℚ zero-ℚ) q)
+            ( λ r (r<q , x<r) →
+              intro-exists
+                ( r , q -ℚ r)
+                ( x<r ,
+                  backward-implication (iff-translate-diff-le-zero-ℚ r q) r<q ,
+                  inv
+                    ( is-identity-right-conjugation-Ab
+                      ( abelian-group-add-ℚ)
+                      ( r)
+                      ( q))))
+            ( forward-implication (is-rounded-cut-upper-ℝ x q) x<q)))
+```
diff --git a/src/real-numbers/lower-dedekind-real-numbers.lagda.md b/src/real-numbers/lower-dedekind-real-numbers.lagda.md
index 3d3bfcb9e7..aed0348cb0 100644
--- a/src/real-numbers/lower-dedekind-real-numbers.lagda.md
+++ b/src/real-numbers/lower-dedekind-real-numbers.lagda.md
@@ -1,13 +1,17 @@
 # Lower Dedekind real numbers
 
 ```agda
+{-# OPTIONS --lossy-unification #-}
+
 module real-numbers.lower-dedekind-real-numbers where
 ```
 
 <details><summary>Imports</summary>
 
 ```agda
+open import elementary-number-theory.difference-rational-numbers
 open import elementary-number-theory.inequality-rational-numbers
+open import elementary-number-theory.positive-rational-numbers
 open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.strict-inequality-rational-numbers
 
@@ -122,6 +126,19 @@ module _
       ( intro-exists q (p<q , q<x))
 ```
 
+### Lower Dedekind cuts are closed under subtraction by positive rational numbers
+
+```agda
+module _
+  {l : Level} (x : lower-ℝ l) (p : ℚ) (d : ℚ⁺)
+  where
+
+  is-in-cut-diff-rational-ℚ⁺-lower-ℝ :
+    is-in-cut-lower-ℝ x p → is-in-cut-lower-ℝ x (p -ℚ rational-ℚ⁺ d)
+  is-in-cut-diff-rational-ℚ⁺-lower-ℝ =
+    is-in-cut-le-ℚ-lower-ℝ x (p -ℚ rational-ℚ⁺ d) p (le-diff-rational-ℚ⁺ p d)
+```
+
 ### Lower Dedekind cuts are closed under inequality on the rationals
 
 ```agda
diff --git a/src/real-numbers/strict-inequality-real-numbers.lagda.md b/src/real-numbers/strict-inequality-real-numbers.lagda.md
index 4b3c021e12..b4cb9f9f2c 100644
--- a/src/real-numbers/strict-inequality-real-numbers.lagda.md
+++ b/src/real-numbers/strict-inequality-real-numbers.lagda.md
@@ -20,11 +20,14 @@ open import foundation.disjunction
 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.identity-types
 open import foundation.large-binary-relations
 open import foundation.logical-equivalences
 open import foundation.negation
+open import foundation.propositional-truncations
 open import foundation.propositions
+open import foundation.subtypes
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
@@ -85,28 +88,20 @@ module _
 
   asymmetric-le-ℝ : le-ℝ x y → ¬ (le-ℝ y x)
   asymmetric-le-ℝ x<y y<x =
-    elim-exists
-      ( empty-Prop)
-      ( λ p (p-in-ux , p-in-ly) →
-        elim-exists
-          ( empty-Prop)
-          ( λ q (q-in-uy , q-in-lx) →
-            rec-coproduct
-              ( λ p<q →
-                asymmetric-le-ℚ
-                  ( p)
-                  ( q)
-                  ( p<q)
-                  ( le-lower-upper-cut-ℝ x q p q-in-lx p-in-ux))
-              ( λ q≤p →
-                not-leq-le-ℚ
-                  ( p)
-                  ( q)
-                  ( le-lower-upper-cut-ℝ y p q p-in-ly q-in-uy)
-                  ( q≤p))
-              ( decide-le-leq-ℚ p q))
-          ( y<x))
-      ( x<y)
+    do
+      p , x<p , p<y ← x<y
+      q , y<q , q<x ← y<x
+      rec-coproduct
+        ( asymmetric-le-ℚ
+            ( q)
+            ( p)
+            ( le-lower-upper-cut-ℝ x q p q<x x<p))
+        ( not-leq-le-ℚ
+            ( p)
+            ( q)
+            ( le-lower-upper-cut-ℝ y p q p<y y<q))
+        ( decide-le-leq-ℚ p q)
+    where open do-syntax-trunc-Prop empty-Prop
 ```
 
 ### Strict inequality on the reals is transitive
@@ -120,23 +115,15 @@ module _
   where
 
   transitive-le-ℝ : le-ℝ y z → le-ℝ x y → le-ℝ x z
-  transitive-le-ℝ y<z =
-    elim-exists
-      ( le-ℝ-Prop x z)
-      ( λ p (p-in-ux , p-in-ly) →
-        elim-exists
-          (le-ℝ-Prop x z)
-          (λ q (q-in-uy , q-in-lz) →
-            intro-exists
-              p
-              ( p-in-ux ,
-                le-lower-cut-ℝ
-                  ( z)
-                  ( p)
-                  ( q)
-                  ( le-lower-upper-cut-ℝ y p q p-in-ly q-in-uy)
-                  ( q-in-lz)))
-          ( y<z))
+  transitive-le-ℝ y<z x<y =
+    do
+      p , x<p , p<y ← x<y
+      q , y<q , q<z ← y<z
+      intro-exists
+        ( p)
+        ( x<p ,
+          le-lower-cut-ℝ z p q (le-lower-upper-cut-ℝ y p q p<y y<q) q<z)
+    where open do-syntax-trunc-Prop (le-ℝ-Prop x z)
 ```
 
 ### The canonical map from rationals to reals preserves and reflects strict inequality
@@ -175,26 +162,12 @@ module _
 
   concatenate-le-leq-ℝ : le-ℝ x y → leq-ℝ y z → le-ℝ x z
   concatenate-le-leq-ℝ x<y y≤z =
-    elim-exists
-      ( le-ℝ-Prop x z)
-      ( λ p (p-in-upper-x , p-in-lower-y) →
-        intro-exists p (p-in-upper-x , y≤z p p-in-lower-y))
-      ( x<y)
+    map-tot-exists (λ p → map-product id (y≤z p)) x<y
 
   concatenate-leq-le-ℝ : leq-ℝ x y → le-ℝ y z → le-ℝ x z
-  concatenate-leq-le-ℝ x≤y y<z =
-    elim-exists
-      ( le-ℝ-Prop x z)
-      ( λ p (p-in-upper-y , p-in-lower-z) →
-        intro-exists
-          ( p)
-          ( forward-implication
-            ( leq-iff-ℝ' x y)
-            ( x≤y)
-            ( p)
-            ( p-in-upper-y) ,
-        p-in-lower-z))
-      ( y<z)
+  concatenate-leq-le-ℝ x≤y =
+    map-tot-exists
+      ( λ p → map-product (forward-implication (leq-iff-ℝ' x y) x≤y p) id)
 ```
 
 ### The reals have no lower or upper bound
@@ -207,26 +180,19 @@ module _
 
   exists-lesser-ℝ : exists (ℝ lzero) (λ y → le-ℝ-Prop y x)
   exists-lesser-ℝ =
-    elim-exists
-      ( ∃ (ℝ lzero) (λ y → le-ℝ-Prop y x))
-      ( λ q q-in-lx →
-        intro-exists
-          ( real-ℚ q)
-          ( forward-implication (is-rounded-lower-cut-ℝ x q) q-in-lx))
+    map-exists
+      ( λ y → le-ℝ y x)
+      ( real-ℚ)
+      ( λ q → forward-implication (is-rounded-lower-cut-ℝ x q))
       ( is-inhabited-lower-cut-ℝ x)
 
   exists-greater-ℝ : exists (ℝ lzero) (λ y → le-ℝ-Prop x y)
   exists-greater-ℝ =
-    elim-exists
-      ( ∃ (ℝ lzero) (λ y → le-ℝ-Prop x y))
-      ( λ q q-in-ux →
-        intro-exists
-          ( real-ℚ q)
-          ( elim-exists
-              ( le-ℝ-Prop x (real-ℚ q))
-              ( λ r (r<q , r-in-ux) → intro-exists r (r-in-ux , r<q))
-              ( forward-implication (is-rounded-upper-cut-ℝ x q) q-in-ux)))
-      ( is-inhabited-upper-cut-ℝ x)
+    do
+      q , x<q ← is-inhabited-upper-cut-ℝ x
+      r , r<q , x<r ← forward-implication (is-rounded-upper-cut-ℝ x q) x<q
+      intro-exists (real-ℚ q) (intro-exists r (x<r , r<q))
+    where open do-syntax-trunc-Prop (∃ (ℝ lzero) (le-ℝ-Prop x))
 ```
 
 ### Negation reverses the strict ordering of real numbers
@@ -239,14 +205,14 @@ module _
   where
 
   reverses-order-neg-ℝ : le-ℝ x y → le-ℝ (neg-ℝ y) (neg-ℝ x)
-  reverses-order-neg-ℝ =
-    elim-exists
-      ( le-ℝ-Prop (neg-ℝ y) (neg-ℝ x))
-      ( λ p (p-in-ux , p-in-ly) →
-        intro-exists
-          ( neg-ℚ p)
-          ( tr (is-in-lower-cut-ℝ y) (inv (neg-neg-ℚ p)) p-in-ly ,
-            tr (is-in-upper-cut-ℝ x) (inv (neg-neg-ℚ p)) p-in-ux))
+  reverses-order-neg-ℝ x<y =
+    do
+      p , x<p , p<y ← x<y
+      intro-exists
+        (neg-ℚ p)
+        ( tr (is-in-lower-cut-ℝ y) (inv (neg-neg-ℚ p)) p<y ,
+          tr (is-in-upper-cut-ℝ x) (inv (neg-neg-ℚ p)) x<p)
+    where open do-syntax-trunc-Prop (le-ℝ-Prop (neg-ℝ y) (neg-ℝ x))
 ```
 
 ### If `x` is less than `y`, then `y` is not less than or equal to `x`
@@ -359,17 +325,18 @@ module _
   where
 
   dense-le-ℝ : le-ℝ x y → exists (ℝ lzero) (λ z → le-ℝ-Prop x z ∧ le-ℝ-Prop z y)
-  dense-le-ℝ =
-    elim-exists
-      ( ∃ (ℝ lzero) (λ z → le-ℝ-Prop x z ∧ le-ℝ-Prop z y))
-      ( λ q (q∈ux , q∈ly) →
-        map-binary-exists
-          ( λ z → le-ℝ x z × le-ℝ z y)
-          ( λ _ _ → real-ℚ q)
-          ( λ p r (p<q , p∈ux) (q<r , r∈ly) →
-            intro-exists p (p∈ux , p<q) , intro-exists r (q<r , r∈ly))
-          ( forward-implication (is-rounded-upper-cut-ℝ x q) q∈ux)
-          ( forward-implication (is-rounded-lower-cut-ℝ y q) q∈ly))
+  dense-le-ℝ x<y =
+    do
+      q , x<q , q<y ← x<y
+      p , p<q , x<p ← forward-implication (is-rounded-upper-cut-ℝ x q) x<q
+      r , q<r , r<y ← forward-implication (is-rounded-lower-cut-ℝ y q) q<y
+      intro-exists
+        ( real-ℚ q)
+        ( intro-exists p (x<p , p<q) , intro-exists r (q<r , r<y))
+    where
+      open
+        do-syntax-trunc-Prop
+          ( ∃ (ℝ lzero) (λ z → le-ℝ-Prop x z ∧ le-ℝ-Prop z y))
 ```
 
 ### Strict inequality on the real numbers is cotransitive
diff --git a/src/real-numbers/upper-dedekind-real-numbers.lagda.md b/src/real-numbers/upper-dedekind-real-numbers.lagda.md
index 2aa058cbbc..c7b49d4276 100644
--- a/src/real-numbers/upper-dedekind-real-numbers.lagda.md
+++ b/src/real-numbers/upper-dedekind-real-numbers.lagda.md
@@ -7,7 +7,9 @@ module real-numbers.upper-dedekind-real-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.positive-rational-numbers
 open import elementary-number-theory.rational-numbers
 open import elementary-number-theory.strict-inequality-rational-numbers
 
@@ -122,6 +124,23 @@ module _
       ( intro-exists p (p<q , p<x))
 ```
 
+### Upper Dedekind cuts are closed under the addition of positive rational numbers
+
+```agda
+module _
+  {l : Level} (x : upper-ℝ l) (p : ℚ) (d : ℚ⁺)
+  where
+
+  is-in-cut-add-rational-ℚ⁺-upper-ℝ :
+    is-in-cut-upper-ℝ x p → is-in-cut-upper-ℝ x (p +ℚ rational-ℚ⁺ d)
+  is-in-cut-add-rational-ℚ⁺-upper-ℝ =
+    is-in-cut-le-ℚ-upper-ℝ
+      ( x)
+      ( p)
+      ( p +ℚ rational-ℚ⁺ d)
+      ( le-right-add-rational-ℚ⁺ p d)
+```
+
 ### Upper Dedekind cuts are closed under inequality on the rationals
 
 ```agda