Addition on lower and upper Dedekind reals

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-ℚ

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

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

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

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

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

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