diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md
index 962a96a816..3c4fb0e591 100644
--- a/src/group-theory.lagda.md
+++ b/src/group-theory.lagda.md
@@ -116,6 +116,9 @@ open import group-theory.large-semigroups public
 open import group-theory.loop-groups-sets public
 open import group-theory.mere-equivalences-concrete-group-actions public
 open import group-theory.mere-equivalences-group-actions public
+open import group-theory.minkowski-multiplication-commutative-monoids public
+open import group-theory.minkowski-multiplication-monoids public
+open import group-theory.minkowski-multiplication-semigroups public
 open import group-theory.monoid-actions public
 open import group-theory.monoids public
 open import group-theory.monomorphisms-concrete-groups public
diff --git a/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md
new file mode 100644
index 0000000000..5ad656d151
--- /dev/null
+++ b/src/group-theory/minkowski-multiplication-commutative-monoids.lagda.md
@@ -0,0 +1,290 @@
+# Minkowski multiplication of subsets of a commutative monoid
+
+```agda
+module group-theory.minkowski-multiplication-commutative-monoids where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-product-types
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.identity-types
+open import foundation.inhabited-subtypes
+open import foundation.powersets
+open import foundation.subtypes
+open import foundation.unital-binary-operations
+open import foundation.universe-levels
+
+open import group-theory.commutative-monoids
+open import group-theory.minkowski-multiplication-monoids
+open import group-theory.monoids
+open import group-theory.subsets-commutative-monoids
+
+open import logic.functoriality-existential-quantification
+```
+
+</details>
+
+## Idea
+
+Given two [subsets](group-theory.subsets-commutative-monoids.md) `A` and `B` of
+a [commutative monoid](group-theory.commutative-monoids.md) `M`, the
+{{#concept "Minkowski multiplication" Disambiguation="on subsets of a commutative monoid" WD="Minkowski addition" WDID=Q1322294 Agda=minkowski-mul-Commutative-Monoid}}
+of `A` and `B` is the [set](foundation-core.sets.md) of elements that can be
+formed by multiplying an element of `A` and an element of `B`. This binary
+operation defines a commutative monoid structure on the
+[powerset](foundation.powersets.md) of `M`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (M : Commutative-Monoid l1)
+  (A : subset-Commutative-Monoid l2 M)
+  (B : subset-Commutative-Monoid l3 M)
+  where
+
+  minkowski-mul-Commutative-Monoid :
+    subset-Commutative-Monoid (l1 ⊔ l2 ⊔ l3) M
+  minkowski-mul-Commutative-Monoid =
+    minkowski-mul-Monoid (monoid-Commutative-Monoid M) A B
+```
+
+## Properties
+
+### Minkowski multiplication on subsets of a commutative monoid is associative
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (M : Commutative-Monoid l1)
+  (A : subset-Commutative-Monoid l2 M)
+  (B : subset-Commutative-Monoid l3 M)
+  (C : subset-Commutative-Monoid l4 M)
+  where
+
+  associative-minkowski-mul-Commutative-Monoid :
+    minkowski-mul-Commutative-Monoid
+      ( M)
+      ( minkowski-mul-Commutative-Monoid M A B)
+      ( C) ＝
+    minkowski-mul-Commutative-Monoid
+      ( M)
+      ( A)
+      ( minkowski-mul-Commutative-Monoid M B C)
+  associative-minkowski-mul-Commutative-Monoid =
+    associative-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A B C
+```
+
+### Minkowski multiplication on subsets of a commutative monoid is unital
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Commutative-Monoid l1)
+  (A : subset-Commutative-Monoid l2 M)
+  where
+
+  left-unit-law-minkowski-mul-Commutative-Monoid :
+    sim-subtype
+      ( minkowski-mul-Commutative-Monoid
+        ( M)
+        ( is-unit-prop-Commutative-Monoid M)
+        ( A))
+      ( A)
+  left-unit-law-minkowski-mul-Commutative-Monoid =
+    left-unit-law-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A
+
+  right-unit-law-minkowski-mul-Commutative-Monoid :
+    sim-subtype
+      ( minkowski-mul-Commutative-Monoid
+        ( M)
+        ( A)
+        ( is-unit-prop-Commutative-Monoid M))
+      ( A)
+  right-unit-law-minkowski-mul-Commutative-Monoid =
+    right-unit-law-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A
+```
+
+### Minkowski multiplication on a commutative monoid is unital
+
+```agda
+module _
+  {l : Level}
+  (M : Commutative-Monoid l)
+  where
+
+  is-unital-minkowski-mul-Commutative-Monoid :
+    is-unital (minkowski-mul-Commutative-Monoid {l} {l} {l} M)
+  is-unital-minkowski-mul-Commutative-Monoid =
+    is-unital-minkowski-mul-Monoid (monoid-Commutative-Monoid M)
+```
+
+### Minkowski multiplication on subsets of a commutative monoid is commutative
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (M : Commutative-Monoid l1)
+  (A : subset-Commutative-Monoid l2 M)
+  (B : subset-Commutative-Monoid l3 M)
+  where
+
+  commutative-minkowski-mul-leq-Commutative-Monoid :
+    minkowski-mul-Commutative-Monoid M A B ⊆
+    minkowski-mul-Commutative-Monoid M B A
+  commutative-minkowski-mul-leq-Commutative-Monoid x =
+    elim-exists
+      ( minkowski-mul-Commutative-Monoid M B A x)
+      ( λ (a , b) (a∈A , b∈B , x=ab) →
+        intro-exists
+          ( b , a)
+          ( b∈B , a∈A , x=ab ∙ commutative-mul-Commutative-Monoid M a b))
+
+module _
+  {l1 l2 l3 : Level}
+  (M : Commutative-Monoid l1)
+  (A : subset-Commutative-Monoid l2 M)
+  (B : subset-Commutative-Monoid l3 M)
+  where
+
+  commutative-minkowski-mul-Commutative-Monoid :
+    minkowski-mul-Commutative-Monoid M A B ＝
+    minkowski-mul-Commutative-Monoid M B A
+  commutative-minkowski-mul-Commutative-Monoid =
+    antisymmetric-sim-subtype
+      ( minkowski-mul-Commutative-Monoid M A B)
+      ( minkowski-mul-Commutative-Monoid M B A)
+      ( commutative-minkowski-mul-leq-Commutative-Monoid M A B ,
+        commutative-minkowski-mul-leq-Commutative-Monoid M B A)
+```
+
+### Minkowski multiplication on subsets of a commutative monoid is a commutative monoid
+
+```agda
+module _
+  {l : Level}
+  (M : Commutative-Monoid l)
+  where
+
+  commutative-monoid-minkowski-mul-Commutative-Monoid :
+    Commutative-Monoid (lsuc l)
+  pr1 commutative-monoid-minkowski-mul-Commutative-Monoid =
+    monoid-minkowski-mul-Monoid (monoid-Commutative-Monoid M)
+  pr2 commutative-monoid-minkowski-mul-Commutative-Monoid =
+    commutative-minkowski-mul-Commutative-Monoid M
+```
+
+### The Minkowski multiplication of two inhabited subsets is inhabited
+
+```agda
+module _
+  {l1 : Level}
+  (M : Commutative-Monoid l1)
+  where
+
+  minkowski-mul-inhabited-is-inhabited-Commutative-Monoid :
+    {l2 l3 : Level} →
+    (A : subset-Commutative-Monoid l2 M) →
+    (B : subset-Commutative-Monoid l3 M) →
+    is-inhabited-subtype A →
+    is-inhabited-subtype B →
+    is-inhabited-subtype (minkowski-mul-Commutative-Monoid M A B)
+  minkowski-mul-inhabited-is-inhabited-Commutative-Monoid =
+    minkowski-mul-inhabited-is-inhabited-Monoid (monoid-Commutative-Monoid M)
+```
+
+### Containment of subsets is preserved by Minkowski multiplication
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (M : Commutative-Monoid l1)
+  (B : subset-Commutative-Monoid l2 M)
+  (A : subset-Commutative-Monoid l3 M)
+  (A' : subset-Commutative-Monoid l4 M)
+  where
+
+  preserves-leq-left-minkowski-mul-Commutative-Monoid :
+    A ⊆ A' →
+    minkowski-mul-Commutative-Monoid M A B ⊆
+    minkowski-mul-Commutative-Monoid M A' B
+  preserves-leq-left-minkowski-mul-Commutative-Monoid =
+    preserves-leq-left-minkowski-mul-Monoid (monoid-Commutative-Monoid M) B A A'
+
+  preserves-leq-right-minkowski-mul-Commutative-Monoid :
+    A ⊆ A' →
+    minkowski-mul-Commutative-Monoid M B A ⊆
+    minkowski-mul-Commutative-Monoid M B A'
+  preserves-leq-right-minkowski-mul-Commutative-Monoid =
+    preserves-leq-right-minkowski-mul-Monoid
+      ( monoid-Commutative-Monoid M)
+      ( B)
+      ( A)
+      ( A')
+```
+
+### Similarity of subsets is preserved by Minkowski multiplication
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (M : Commutative-Monoid l1)
+  (B : subset-Commutative-Monoid l2 M)
+  (A : subset-Commutative-Monoid l3 M)
+  (A' : subset-Commutative-Monoid l4 M)
+  where
+
+  preserves-sim-left-minkowski-mul-Commutative-Monoid :
+    sim-subtype A A' →
+    sim-subtype
+      ( minkowski-mul-Commutative-Monoid M A B)
+      ( minkowski-mul-Commutative-Monoid M A' B)
+  preserves-sim-left-minkowski-mul-Commutative-Monoid =
+    preserves-sim-left-minkowski-mul-Monoid (monoid-Commutative-Monoid M) B A A'
+
+  preserves-sim-right-minkowski-mul-Commutative-Monoid :
+    sim-subtype A A' →
+    sim-subtype
+      ( minkowski-mul-Commutative-Monoid M B A)
+      ( minkowski-mul-Commutative-Monoid M B A')
+  preserves-sim-right-minkowski-mul-Commutative-Monoid =
+    preserves-sim-right-minkowski-mul-Monoid
+      ( monoid-Commutative-Monoid M)
+      ( B)
+      ( A)
+      ( A')
+
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  (M : Commutative-Monoid l1)
+  (A : subset-Commutative-Monoid l2 M)
+  (A' : subset-Commutative-Monoid l3 M)
+  (B : subset-Commutative-Monoid l4 M)
+  (B' : subset-Commutative-Monoid l5 M)
+  where
+
+  preserves-sim-minkowski-mul-Commutative-Monoid :
+    sim-subtype A A' →
+    sim-subtype B B' →
+    sim-subtype
+      ( minkowski-mul-Commutative-Monoid M A B)
+      ( minkowski-mul-Commutative-Monoid M A' B')
+  preserves-sim-minkowski-mul-Commutative-Monoid =
+    preserves-sim-minkowski-mul-Monoid (monoid-Commutative-Monoid M) A A' B B'
+```
+
+## See also
+
+- Minkowski multiplication on semigroups is defined in
+  [`group-theory.minkowski-multiplication-semigroups`](group-theory.minkowski-multiplication-semigroups.md).
+- Minkowski multiplication on monoids is defined in
+  [`group-theory.minkowski-multiplication-monoids`](group-theory.minkowski-multiplication-monoids.md).
+
+## External links
+
+- [Minkowski addition](https://en.wikipedia.org/wiki/Minkowski_addition) at
+  Wikipedia
diff --git a/src/group-theory/minkowski-multiplication-monoids.lagda.md b/src/group-theory/minkowski-multiplication-monoids.lagda.md
new file mode 100644
index 0000000000..185f47cbda
--- /dev/null
+++ b/src/group-theory/minkowski-multiplication-monoids.lagda.md
@@ -0,0 +1,244 @@
+# Minkowski multiplication on subsets of a monoid
+
+```agda
+module group-theory.minkowski-multiplication-monoids where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.existential-quantification
+open import foundation.identity-types
+open import foundation.inhabited-subtypes
+open import foundation.powersets
+open import foundation.subtypes
+open import foundation.transport-along-identifications
+open import foundation.unital-binary-operations
+open import foundation.universe-levels
+
+open import group-theory.minkowski-multiplication-semigroups
+open import group-theory.monoids
+open import group-theory.semigroups
+open import group-theory.subsets-monoids
+```
+
+</details>
+
+## Idea
+
+Given two [subsets](group-theory.subsets-monoids.md) `A` and `B` of a
+[monoid](group-theory.monoids.md) `M`, the
+{{#concept "Minkowski multiplication" Disambiguation="on subsets of a monoid" WD="Minkowski addition" WDID=Q1322294  Agda=minkowski-mul-Monoid}}
+of `A` and `B` is the [set](foundation-core.sets.md) of elements that can be
+formed by multiplying an element of `A` and an element of `B`. This binary
+operation defines a monoid structure on the [powerset](foundation.powersets.md)
+of `M`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (M : Monoid l1)
+  (A : subset-Monoid l2 M)
+  (B : subset-Monoid l3 M)
+  where
+
+  minkowski-mul-Monoid : subset-Monoid (l1 ⊔ l2 ⊔ l3) M
+  minkowski-mul-Monoid = minkowski-mul-Semigroup (semigroup-Monoid M) A B
+```
+
+## Properties
+
+### Minkowski multiplication on subsets of a monoid is associative
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (M : Monoid l1)
+  (A : subset-Monoid l2 M)
+  (B : subset-Monoid l3 M)
+  (C : subset-Monoid l4 M)
+  where
+
+  associative-minkowski-mul-Monoid :
+    minkowski-mul-Monoid M (minkowski-mul-Monoid M A B) C ＝
+    minkowski-mul-Monoid M A (minkowski-mul-Monoid M B C)
+  associative-minkowski-mul-Monoid =
+    associative-minkowski-mul-Semigroup (semigroup-Monoid M) A B C
+```
+
+### Unit laws for Minkowski multiplication on subsets of a monoid
+
+```agda
+module _
+  {l1 l2 : Level}
+  (M : Monoid l1)
+  (A : subset-Monoid l2 M)
+  where
+
+  left-unit-law-minkowski-mul-Monoid :
+    sim-subtype (minkowski-mul-Monoid M (is-unit-Monoid-Prop M) A) A
+  pr1 left-unit-law-minkowski-mul-Monoid a =
+    elim-exists
+      ( A a)
+      ( λ (z , a') (z=1 , a'∈A , a=za') →
+        tr
+          ( is-in-subtype A)
+          ( inv
+            ( equational-reasoning
+              a
+              ＝ mul-Monoid M z a' by a=za'
+              ＝ mul-Monoid M (unit-Monoid M) a' by ap (mul-Monoid' M a') z=1
+              ＝ a' by left-unit-law-mul-Monoid M a'))
+          ( a'∈A))
+  pr2 left-unit-law-minkowski-mul-Monoid a a∈A =
+    intro-exists
+      ( unit-Monoid M , a)
+      ( refl , a∈A , inv (left-unit-law-mul-Monoid M a))
+
+  right-unit-law-minkowski-mul-Monoid :
+    sim-subtype (minkowski-mul-Monoid M A (is-unit-Monoid-Prop M)) A
+  pr1 right-unit-law-minkowski-mul-Monoid a =
+    elim-exists
+      ( A a)
+      ( λ (a' , z) (a'∈A , z=1 , a=a'z) →
+        tr
+          ( is-in-subtype A)
+          ( inv
+            ( equational-reasoning
+              a
+              ＝ mul-Monoid M a' z by a=a'z
+              ＝ mul-Monoid M a' (unit-Monoid M) by ap (mul-Monoid M a') z=1
+              ＝ a' by right-unit-law-mul-Monoid M a'))
+          ( a'∈A))
+  pr2 right-unit-law-minkowski-mul-Monoid a a∈A =
+    intro-exists
+      ( a , unit-Monoid M)
+      ( a∈A , refl , inv (right-unit-law-mul-Monoid M a))
+```
+
+### Minkowski multiplication on subsets of a monoid forms a monoid
+
+```agda
+module _
+  {l : Level}
+  (M : Monoid l)
+  where
+
+  is-unital-minkowski-mul-Monoid :
+    is-unital (minkowski-mul-Monoid {l} {l} {l} M)
+  pr1 is-unital-minkowski-mul-Monoid = is-unit-Monoid-Prop M
+  pr1 (pr2 is-unital-minkowski-mul-Monoid) A =
+    antisymmetric-sim-subtype
+      ( minkowski-mul-Monoid M (is-unit-Monoid-Prop M) A)
+      ( A)
+      ( left-unit-law-minkowski-mul-Monoid M A)
+  pr2 (pr2 is-unital-minkowski-mul-Monoid) A =
+    antisymmetric-sim-subtype
+      ( minkowski-mul-Monoid M A (is-unit-Monoid-Prop M))
+      ( A)
+      ( right-unit-law-minkowski-mul-Monoid M A)
+
+  monoid-minkowski-mul-Monoid : Monoid (lsuc l)
+  pr1 monoid-minkowski-mul-Monoid =
+    semigroup-minkowski-mul-Semigroup (semigroup-Monoid M)
+  pr2 monoid-minkowski-mul-Monoid = is-unital-minkowski-mul-Monoid
+```
+
+### The Minkowski multiplication of two inhabited subsets of a monoid is inhabited
+
+```agda
+module _
+  {l1 : Level}
+  (M : Monoid l1)
+  where
+
+  minkowski-mul-inhabited-is-inhabited-Monoid :
+    {l2 l3 : Level} →
+    (A : subset-Monoid l2 M) →
+    (B : subset-Monoid l3 M) →
+    is-inhabited-subtype A →
+    is-inhabited-subtype B →
+    is-inhabited-subtype (minkowski-mul-Monoid M A B)
+  minkowski-mul-inhabited-is-inhabited-Monoid =
+    minkowski-mul-inhabited-is-inhabited-Semigroup (semigroup-Monoid M)
+```
+
+### Containment of subsets is preserved by Minkowski multiplication
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (M : Monoid l1)
+  (B : subset-Monoid l2 M)
+  (A : subset-Monoid l3 M)
+  (A' : subset-Monoid l4 M)
+  where
+
+  preserves-leq-left-minkowski-mul-Monoid :
+    A ⊆ A' → minkowski-mul-Monoid M A B ⊆ minkowski-mul-Monoid M A' B
+  preserves-leq-left-minkowski-mul-Monoid =
+    preserves-leq-left-minkowski-mul-Semigroup (semigroup-Monoid M) B A A'
+
+  preserves-leq-right-minkowski-mul-Monoid :
+    A ⊆ A' → minkowski-mul-Monoid M B A ⊆ minkowski-mul-Monoid M B A'
+  preserves-leq-right-minkowski-mul-Monoid =
+    preserves-leq-right-minkowski-mul-Semigroup (semigroup-Monoid M) B A A'
+```
+
+### Similarity of subsets is preserved by Minkowski multiplication
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (M : Monoid l1)
+  (B : subset-Monoid l2 M)
+  (A : subset-Monoid l3 M)
+  (A' : subset-Monoid l4 M)
+  where
+
+  preserves-sim-left-minkowski-mul-Monoid :
+    sim-subtype A A' →
+    sim-subtype (minkowski-mul-Monoid M A B) (minkowski-mul-Monoid M A' B)
+  preserves-sim-left-minkowski-mul-Monoid =
+    preserves-sim-left-minkowski-mul-Semigroup (semigroup-Monoid M) B A A'
+
+  preserves-sim-right-minkowski-mul-Monoid :
+    sim-subtype A A' →
+    sim-subtype (minkowski-mul-Monoid M B A) (minkowski-mul-Monoid M B A')
+  preserves-sim-right-minkowski-mul-Monoid =
+    preserves-sim-right-minkowski-mul-Semigroup (semigroup-Monoid M) B A A'
+
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  (M : Monoid l1)
+  (A : subset-Monoid l2 M)
+  (A' : subset-Monoid l3 M)
+  (B : subset-Monoid l4 M)
+  (B' : subset-Monoid l5 M)
+  where
+
+  preserves-sim-minkowski-mul-Monoid :
+    sim-subtype A A' →
+    sim-subtype B B' →
+    sim-subtype
+      ( minkowski-mul-Monoid M A B)
+      ( minkowski-mul-Monoid M A' B')
+  preserves-sim-minkowski-mul-Monoid =
+    preserves-sim-minkowski-mul-Semigroup (semigroup-Monoid M) A A' B B'
+```
+
+## See also
+
+- Minkowski multiplication on semigroups is defined in
+  [`group-theory.minkowski-multiplication-semigroups`](group-theory.minkowski-multiplication-semigroups.md).
+- Minkowski multiplication on commutative monoids is defined in
+  [`group-theory.minkowski-multiplication-commutative-monoids`](group-theory.minkowski-multiplication-commutative-monoids.md).
+
+## External links
+
+- [Minkowski addition](https://en.wikipedia.org/wiki/Minkowski_addition) at
+  Wikipedia
diff --git a/src/group-theory/minkowski-multiplication-semigroups.lagda.md b/src/group-theory/minkowski-multiplication-semigroups.lagda.md
new file mode 100644
index 0000000000..4fd75c3fff
--- /dev/null
+++ b/src/group-theory/minkowski-multiplication-semigroups.lagda.md
@@ -0,0 +1,244 @@
+# Minkowski multiplication on subsets of a semigroup
+
+```agda
+module group-theory.minkowski-multiplication-semigroups where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.conjunction
+open import foundation.dependent-pair-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.inhabited-subtypes
+open import foundation.powersets
+open import foundation.propositions
+open import foundation.sets
+open import foundation.subtypes
+open import foundation.universe-levels
+
+open import group-theory.semigroups
+open import group-theory.subsets-semigroups
+
+open import logic.functoriality-existential-quantification
+```
+
+</details>
+
+## Idea
+
+Given two [subsets](group-theory.subsets-semigroups.md) `A` and `B` of a
+[semigroup](group-theory.semigroups.md) `S`, the
+{{#concept "Minkowski multiplication" Disambiguation="on subsets of a semigroup" WD="Minkowski addition" WDID=Q1322294 Agda=minkowski-mul-Semigroup}}
+of `A` and `B` is the [set](foundation-core.sets.md) of elements that can be
+formed by multiplying an element of `A` and an element of `B`. This binary
+operation defines a semigroup structure on the
+[powerset](foundation.powersets.md) of `S`.
+
+## Definition
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (G : Semigroup l1)
+  (A : subset-Semigroup l2 G)
+  (B : subset-Semigroup l3 G)
+  where
+
+  minkowski-mul-Semigroup : subset-Semigroup (l1 ⊔ l2 ⊔ l3) G
+  minkowski-mul-Semigroup c = ∃
+    ( type-Semigroup G × type-Semigroup G)
+    ( λ (a , b) →
+      A a ∧ B b ∧ Id-Prop (set-Semigroup G) c (mul-Semigroup G a b))
+```
+
+## Properties
+
+### Minkowski multiplication on subsets of a semigroup is associative
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (G : Semigroup l1)
+  (A : subset-Semigroup l2 G)
+  (B : subset-Semigroup l3 G)
+  (C : subset-Semigroup l4 G)
+  where
+
+  sim-associative-minkowski-mul-Semigroup :
+    sim-subtype
+      ( minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C)
+      ( minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C))
+  pr1 sim-associative-minkowski-mul-Semigroup x =
+    elim-exists
+      ( claim)
+      ( λ (ab , c) (ab∈AB , c∈C , x=ab*c) →
+        elim-exists
+          ( claim)
+          ( λ (a , b) (a∈A , b∈B , ab=a*b) →
+            intro-exists
+              ( a , mul-Semigroup G b c)
+              ( a∈A ,
+                intro-exists (b , c) (b∈B , c∈C , refl) ,
+                ( equational-reasoning
+                  x
+                  ＝ mul-Semigroup G ab c by x=ab*c
+                  ＝ mul-Semigroup G (mul-Semigroup G a b) c
+                    by ap (mul-Semigroup' G c) ab=a*b
+                  ＝ mul-Semigroup G a (mul-Semigroup G b c)
+                    by associative-mul-Semigroup G a b c)))
+          ( ab∈AB))
+    where
+      claim =
+        minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C) x
+  pr2 sim-associative-minkowski-mul-Semigroup x =
+    elim-exists
+      ( claim)
+      ( λ (a , bc) (a∈A , bc∈BC , x=a*bc) →
+        elim-exists
+          ( claim)
+          ( λ (b , c) (b∈B , c∈C , bc=b*c) →
+            intro-exists
+              ( mul-Semigroup G a b , c)
+              ( intro-exists (a , b) (a∈A , b∈B , refl) ,
+                c∈C ,
+                ( equational-reasoning
+                  x
+                  ＝ mul-Semigroup G a bc by x=a*bc
+                  ＝ mul-Semigroup G a (mul-Semigroup G b c)
+                    by ap (mul-Semigroup G a) bc=b*c
+                  ＝ mul-Semigroup G (mul-Semigroup G a b) c
+                    by inv (associative-mul-Semigroup G a b c))))
+          ( bc∈BC))
+    where
+      claim =
+        minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C x
+
+  associative-minkowski-mul-Semigroup :
+    minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C ＝
+    minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C)
+  associative-minkowski-mul-Semigroup =
+    antisymmetric-sim-subtype
+      ( minkowski-mul-Semigroup G (minkowski-mul-Semigroup G A B) C)
+      ( minkowski-mul-Semigroup G A (minkowski-mul-Semigroup G B C))
+      ( sim-associative-minkowski-mul-Semigroup)
+```
+
+### Minkowski multiplication on subsets of a semigroup forms a semigroup
+
+```agda
+module _
+  {l : Level}
+  (G : Semigroup l)
+  where
+
+  semigroup-minkowski-mul-Semigroup : Semigroup (lsuc l)
+  pr1 semigroup-minkowski-mul-Semigroup = subtype-Set l (type-Semigroup G)
+  pr1 (pr2 semigroup-minkowski-mul-Semigroup) = minkowski-mul-Semigroup G
+  pr2 (pr2 semigroup-minkowski-mul-Semigroup) =
+    associative-minkowski-mul-Semigroup G
+```
+
+### The Minkowski multiplication of two inhabited subsets of a semigroup is inhabited
+
+```agda
+module _
+  {l1 l2 l3 : Level}
+  (G : Semigroup l1)
+  (A : subset-Semigroup l2 G)
+  (B : subset-Semigroup l3 G)
+  where
+
+  minkowski-mul-inhabited-is-inhabited-Semigroup :
+    is-inhabited-subtype A →
+    is-inhabited-subtype B →
+    is-inhabited-subtype (minkowski-mul-Semigroup G A B)
+  minkowski-mul-inhabited-is-inhabited-Semigroup =
+    map-binary-exists
+      ( is-in-subtype (minkowski-mul-Semigroup G A B))
+      ( mul-Semigroup G)
+      ( λ a b a∈A b∈B → intro-exists (a , b) (a∈A , b∈B , refl))
+```
+
+### Containment of subsets is preserved by Minkowski multiplication
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (G : Semigroup l1)
+  (B : subset-Semigroup l2 G)
+  (A : subset-Semigroup l3 G)
+  (A' : subset-Semigroup l4 G)
+  where
+
+  preserves-leq-left-minkowski-mul-Semigroup :
+    A ⊆ A' → minkowski-mul-Semigroup G A B ⊆ minkowski-mul-Semigroup G A' B
+  preserves-leq-left-minkowski-mul-Semigroup A⊆A' x =
+    map-tot-exists (λ (a , b) → map-product (A⊆A' a) id)
+
+  preserves-leq-right-minkowski-mul-Semigroup :
+    A ⊆ A' → minkowski-mul-Semigroup G B A ⊆ minkowski-mul-Semigroup G B A'
+  preserves-leq-right-minkowski-mul-Semigroup A⊆A' x =
+    map-tot-exists (λ (b , a) → map-product id (map-product (A⊆A' a) id))
+```
+
+### Similarity of subsets is preserved by Minkowski multiplication
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  (G : Semigroup l1)
+  (B : subset-Semigroup l2 G)
+  (A : subset-Semigroup l3 G)
+  (A' : subset-Semigroup l4 G)
+  where
+
+  preserves-sim-left-minkowski-mul-Semigroup :
+    sim-subtype A A' →
+    sim-subtype (minkowski-mul-Semigroup G A B) (minkowski-mul-Semigroup G A' B)
+  pr1 (preserves-sim-left-minkowski-mul-Semigroup (A⊆A' , _)) =
+    preserves-leq-left-minkowski-mul-Semigroup G B A A' A⊆A'
+  pr2 (preserves-sim-left-minkowski-mul-Semigroup (_ , A'⊆A)) =
+    preserves-leq-left-minkowski-mul-Semigroup G B A' A A'⊆A
+
+  preserves-sim-right-minkowski-mul-Semigroup :
+    sim-subtype A A' →
+    sim-subtype (minkowski-mul-Semigroup G B A) (minkowski-mul-Semigroup G B A')
+  pr1 (preserves-sim-right-minkowski-mul-Semigroup (A⊆A' , _)) =
+    preserves-leq-right-minkowski-mul-Semigroup G B A A' A⊆A'
+  pr2 (preserves-sim-right-minkowski-mul-Semigroup (_ , A'⊆A)) =
+    preserves-leq-right-minkowski-mul-Semigroup G B A' A A'⊆A
+
+module _
+  {l1 l2 l3 l4 l5 : Level}
+  (G : Semigroup l1)
+  (A : subset-Semigroup l2 G)
+  (A' : subset-Semigroup l3 G)
+  (B : subset-Semigroup l4 G)
+  (B' : subset-Semigroup l5 G)
+  where
+
+  preserves-sim-minkowski-mul-Semigroup :
+    sim-subtype A A' →
+    sim-subtype B B' →
+    sim-subtype
+      ( minkowski-mul-Semigroup G A B)
+      ( minkowski-mul-Semigroup G A' B')
+  preserves-sim-minkowski-mul-Semigroup A≈A' B≈B' =
+    transitive-sim-subtype
+      ( minkowski-mul-Semigroup G A B)
+      ( minkowski-mul-Semigroup G A B')
+      ( minkowski-mul-Semigroup G A' B')
+      ( preserves-sim-left-minkowski-mul-Semigroup G B' A A' A≈A')
+      ( preserves-sim-right-minkowski-mul-Semigroup G A B B' B≈B')
+```
+
+## External links
+
+- [Minkowski addition](https://en.wikipedia.org/wiki/Minkowski_addition) at
+  Wikipedia
diff --git a/src/group-theory/monoids.lagda.md b/src/group-theory/monoids.lagda.md
index 1e76dbc225..6a0c542cfc 100644
--- a/src/group-theory/monoids.lagda.md
+++ b/src/group-theory/monoids.lagda.md
@@ -82,6 +82,12 @@ module _
   unit-Monoid : type-Monoid
   unit-Monoid = pr1 has-unit-Monoid
 
+  is-unit-Monoid-Prop : type-Monoid → Prop l
+  is-unit-Monoid-Prop x = Id-Prop set-Monoid x unit-Monoid
+
+  is-unit-Monoid : type-Monoid → UU l
+  is-unit-Monoid x = x ＝ unit-Monoid
+
   left-unit-law-mul-Monoid : (x : type-Monoid) → mul-Monoid unit-Monoid x ＝ x
   left-unit-law-mul-Monoid = pr1 (pr2 has-unit-Monoid)