diff --git a/src/real-numbers/binary-maximum-real-numbers.lagda.md b/src/real-numbers/binary-maximum-real-numbers.lagda.md
index 7d521f85c1..339cfb5970 100644
--- a/src/real-numbers/binary-maximum-real-numbers.lagda.md
+++ b/src/real-numbers/binary-maximum-real-numbers.lagda.md
@@ -22,6 +22,9 @@ open import foundation.propositional-truncations
 open import foundation.propositions
 open import foundation.universe-levels
 
+open import group-theory.large-semigroups
+open import group-theory.semigroups
+
 open import metric-spaces.metric-space-of-short-functions-metric-spaces
 open import metric-spaces.short-functions-metric-spaces
 
@@ -200,6 +203,78 @@ module _
             ( is-least-binary-upper-bound-max-ℝ y x)))
 ```
 
+### The binary maximum is associative
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (x : ℝ l1) (y : ℝ l2) (z : ℝ l3)
+  where
+
+  abstract
+    associative-max-ℝ : max-ℝ (max-ℝ x y) z ＝ max-ℝ x (max-ℝ y z)
+    associative-max-ℝ =
+      antisymmetric-leq-ℝ
+        ( max-ℝ (max-ℝ x y) z)
+        ( max-ℝ x (max-ℝ y z))
+        ( leq-max-leq-leq-ℝ
+          ( max-ℝ x y)
+          ( z)
+          ( max-ℝ x (max-ℝ y z))
+          ( leq-max-leq-leq-ℝ
+            ( x)
+            ( y)
+            ( max-ℝ x (max-ℝ y z))
+            ( leq-left-max-ℝ x (max-ℝ y z))
+            ( transitive-leq-ℝ
+              ( y)
+              ( max-ℝ y z)
+              ( max-ℝ x (max-ℝ y z))
+              ( leq-right-max-ℝ x (max-ℝ y z))
+              ( leq-left-max-ℝ y z)))
+          ( transitive-leq-ℝ
+            ( z)
+            ( max-ℝ y z)
+            ( max-ℝ x (max-ℝ y z))
+            ( leq-right-max-ℝ x (max-ℝ y z))
+            ( leq-right-max-ℝ y z)))
+        ( leq-max-leq-leq-ℝ
+          ( x)
+          ( max-ℝ y z)
+          ( max-ℝ (max-ℝ x y) z)
+          ( transitive-leq-ℝ
+            ( x)
+            ( max-ℝ x y)
+            ( max-ℝ (max-ℝ x y) z)
+            ( leq-left-max-ℝ (max-ℝ x y) z)
+            ( leq-left-max-ℝ x y))
+          ( leq-max-leq-leq-ℝ
+            ( y)
+            ( z)
+            ( max-ℝ (max-ℝ x y) z)
+            ( transitive-leq-ℝ
+              ( y)
+              ( max-ℝ x y)
+              ( max-ℝ (max-ℝ x y) z)
+              ( leq-left-max-ℝ (max-ℝ x y) z)
+              ( leq-right-max-ℝ x y))
+            ( leq-right-max-ℝ (max-ℝ x y) z)))
+```
+
+### The large semigroup of real numbers under the maximum operator
+
+```agda
+large-semigroup-max-ℝ : Large-Semigroup lsuc
+large-semigroup-max-ℝ = make-Large-Semigroup ℝ-Set max-ℝ associative-max-ℝ
+```
+
+### The semigroup of real numbers under the maximum operator at a given level
+
+```agda
+semigroup-max-ℝ : (l : Level) → Semigroup (lsuc l)
+semigroup-max-ℝ = semigroup-Large-Semigroup large-semigroup-max-ℝ
+```
+
 ### The large poset of real numbers has joins
 
 ```agda
diff --git a/src/real-numbers/binary-minimum-real-numbers.lagda.md b/src/real-numbers/binary-minimum-real-numbers.lagda.md
index f156bb4674..519a7fab77 100644
--- a/src/real-numbers/binary-minimum-real-numbers.lagda.md
+++ b/src/real-numbers/binary-minimum-real-numbers.lagda.md
@@ -19,6 +19,9 @@ open import foundation.logical-equivalences
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 
+open import group-theory.large-semigroups
+open import group-theory.semigroups
+
 open import order-theory.greatest-lower-bounds-large-posets
 open import order-theory.large-meet-semilattices
 open import order-theory.meet-semilattices
@@ -132,6 +135,78 @@ module _
           ( is-greatest-binary-lower-bound-min-ℝ x y))
 ```
 
+### The binary minimum is associative
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (x : ℝ l1) (y : ℝ l2) (z : ℝ l3)
+  where
+
+  abstract
+    associative-min-ℝ : min-ℝ (min-ℝ x y) z ＝ min-ℝ x (min-ℝ y z)
+    associative-min-ℝ =
+      antisymmetric-leq-ℝ
+        ( min-ℝ (min-ℝ x y) z)
+        ( min-ℝ x (min-ℝ y z))
+        ( leq-min-leq-leq-ℝ
+          ( x)
+          ( min-ℝ y z)
+          ( min-ℝ (min-ℝ x y) z)
+          ( transitive-leq-ℝ
+            ( min-ℝ (min-ℝ x y) z)
+            ( min-ℝ x y)
+            ( x)
+            ( leq-left-min-ℝ x y)
+            ( leq-left-min-ℝ (min-ℝ x y) z))
+          ( leq-min-leq-leq-ℝ
+            ( y)
+            ( z)
+            ( min-ℝ ( min-ℝ x y) z)
+            ( transitive-leq-ℝ
+              ( min-ℝ (min-ℝ x y) z)
+              ( min-ℝ x y)
+              ( y)
+              ( leq-right-min-ℝ x y)
+              ( leq-left-min-ℝ (min-ℝ x y) z))
+            ( leq-right-min-ℝ (min-ℝ x y) z)))
+        ( leq-min-leq-leq-ℝ
+          ( min-ℝ x y)
+          ( z)
+          ( min-ℝ x (min-ℝ y z))
+          ( leq-min-leq-leq-ℝ
+            ( x)
+            ( y)
+            ( min-ℝ x (min-ℝ y z))
+            ( leq-left-min-ℝ x (min-ℝ y z))
+            ( transitive-leq-ℝ
+              ( min-ℝ x (min-ℝ y z))
+              ( min-ℝ y z)
+              ( y)
+              ( leq-left-min-ℝ y z)
+              ( leq-right-min-ℝ x (min-ℝ y z))))
+          ( transitive-leq-ℝ
+            ( min-ℝ x (min-ℝ y z))
+            ( min-ℝ y z)
+            ( z)
+            ( leq-right-min-ℝ y z)
+            ( leq-right-min-ℝ x (min-ℝ y z))))
+```
+
+### The large semigroup of real numbers under the minimum operator
+
+```agda
+large-semigroup-min-ℝ : Large-Semigroup lsuc
+large-semigroup-min-ℝ = make-Large-Semigroup ℝ-Set min-ℝ associative-min-ℝ
+```
+
+### The semigroup of real numbers under the minimum operator at a given level
+
+```agda
+semigroup-min-ℝ : (l : Level) → Semigroup (lsuc l)
+semigroup-min-ℝ = semigroup-Large-Semigroup large-semigroup-min-ℝ
+```
+
 ### The large poset of real numbers has meets
 
 ```agda