chore: misc. algebra improvements (#451)

# Description Doing a bit of work on quasigroups, and encountered some minor points of friction with the Algebra heirarchy. This PR fixes some of those, and makes some minor improvements in a few places. ## Checklist Before submitting a merge request, please check the items below: - [x] I've read [the contributing guidelines](https://github.com/plt-amy/1lab/blob/main/CONTRIBUTING.md). - [x] The imports of new modules have been sorted with `support/sort-imports.hs` (or `nix run --experimental-features nix-command -f . sort-imports`). - [x] All new code blocks have "agda" as their language. If your change affects many files without adding substantial content, and you don't want your name to appear on those pages (for example, treewide refactorings or reformattings), start the commit message and PR title with `chore:`.
the1lab · Jan 6, 2025 · d1d6951 · d1d6951
1 parent b3875c1
commit d1d6951
Show file tree

Hide file tree

Showing 10 changed files with 150 additions and 79 deletions.
diff --git a/src/Algebra/Group.lagda.md b/src/Algebra/Group.lagda.md
@@ -271,8 +271,8 @@ record make-group {ℓ} (G : Type ℓ) : Type ℓ where
     idl   : ∀ x → mul unit x ≡ x
 
   private
-    inverser : ∀ x → mul x (inv x) ≡ unit
-    inverser x =
+    invr : ∀ x → mul x (inv x) ≡ unit
+    invr x =
       mul x (inv x)                                   ≡˘⟨ idl _ ⟩
       mul unit (mul x (inv x))                        ≡˘⟨ ap₂ mul (invl _) refl ⟩
       mul (mul (inv (inv x)) (inv x)) (mul x (inv x)) ≡˘⟨ assoc _ _ _ ⟩
@@ -282,23 +282,26 @@ record make-group {ℓ} (G : Type ℓ) : Type ℓ where
       mul (inv (inv x)) (inv x)                       ≡⟨ invl _ ⟩
       unit                                            ∎
 
-  to-group-on : Group-on G
-  to-group-on .Group-on._⋆_ = mul
-  to-group-on .Group-on.has-is-group .is-group.unit = unit
-  to-group-on .Group-on.has-is-group .is-group.inverse = inv
-  to-group-on .Group-on.has-is-group .is-group.inversel = invl _
-  to-group-on .Group-on.has-is-group .is-group.inverser = inverser _
-  to-group-on .Group-on.has-is-group .is-group.has-is-monoid .is-monoid.idl {x} = idl x
-  to-group-on .Group-on.has-is-group .is-group.has-is-monoid .is-monoid.idr {x} =
+  to-is-group : is-group mul
+  to-is-group .is-group.unit = unit
+  to-is-group .is-group.inverse = inv
+  to-is-group .is-group.inversel = invl _
+  to-is-group .is-group.inverser = invr _
+  to-is-group .is-group.has-is-monoid .is-monoid.idl {x} = idl x
+  to-is-group .is-group.has-is-monoid .is-monoid.idr {x} =
     mul x ⌜ unit ⌝           ≡˘⟨ ap¡ (invl x) ⟩
     mul x (mul (inv x) x)    ≡⟨ assoc _ _ _ ⟩
-    mul ⌜ mul x (inv x) ⌝ x  ≡⟨ ap! (inverser x) ⟩
+    mul ⌜ mul x (inv x) ⌝ x  ≡⟨ ap! (invr x) ⟩
     mul unit x               ≡⟨ idl x ⟩
     x                        ∎
-  to-group-on .Group-on.has-is-group .is-group.has-is-monoid .has-is-semigroup =
+  to-is-group .is-group.has-is-monoid .has-is-semigroup =
     record { has-is-magma = record { has-is-set = group-is-set }
            ; associative = λ {x y z} → assoc x y z
            }
 
-open make-group using (to-group-on) public
+  to-group-on : Group-on G
+  to-group-on .Group-on._⋆_ = mul
+  to-group-on .Group-on.has-is-group = to-is-group
+
+open make-group using (to-is-group; to-group-on) public
 ```
diff --git a/src/Algebra/Group/Ab.lagda.md b/src/Algebra/Group/Ab.lagda.md
@@ -153,15 +153,18 @@ record make-abelian-group (T : Type ℓ) : Type ℓ where
     mg .make-group.invl   = invl
     mg .make-group.idl    = idl
 
+  to-is-abelian-group : is-abelian-group mul
+  to-is-abelian-group .is-abelian-group.has-is-group =
+    to-is-group make-abelian-group→make-group
+  to-is-abelian-group .is-abelian-group.commutes =
+    comm _ _
+
   to-group-on-ab : Group-on T
   to-group-on-ab = to-group-on make-abelian-group→make-group
 
   to-abelian-group-on : Abelian-group-on T
   to-abelian-group-on .Abelian-group-on._*_ = mul
-  to-abelian-group-on .Abelian-group-on.has-is-ab .is-abelian-group.has-is-group =
-    Group-on.has-is-group to-group-on-ab
-  to-abelian-group-on .Abelian-group-on.has-is-ab .is-abelian-group.commutes =
-    comm _ _
+  to-abelian-group-on .Abelian-group-on.has-is-ab = to-is-abelian-group
 
   to-ab : Abelian-group ℓ
   ∣ to-ab .fst ∣ = T
@@ -191,7 +194,7 @@ Grp→Ab→Grp G c = Σ-pathp refl go where
   go i .Group-on._⋆_ = G .snd .Group-on._⋆_
   go i .Group-on.has-is-group = G .snd .Group-on.has-is-group
 
-open make-abelian-group using (make-abelian-group→make-group ; to-group-on-ab ; to-abelian-group-on ; to-ab) public
+open make-abelian-group using (make-abelian-group→make-group ; to-group-on-ab ; to-is-abelian-group ; to-abelian-group-on ; to-ab) public
 
 open Functor
 

diff --git a/src/Algebra/Magma.lagda.md b/src/Algebra/Magma.lagda.md
@@ -68,7 +68,7 @@ binary operation `⋆`, on which no further laws are imposed.
     magma-hlevel : ∀ {n} → H-Level A (2 + n)
     magma-hlevel = basic-instance 2 has-is-set
 
-open is-magma public
+open is-magma
 ```
 
 Note that we do not generally benefit from the [[set truncation]] of
@@ -84,6 +84,16 @@ is-magma-is-prop x y i .has-is-set =
   is-hlevel-is-prop 2 (x .has-is-set) (y .has-is-set) i
 ```
 
+<!--
+```agda
+instance
+  H-Level-is-magma
+    : ∀ {ℓ} {A : Type ℓ} {_⋆_ : A → A → A} {n}
+    → H-Level (is-magma _⋆_) (suc n)
+  H-Level-is-magma = prop-instance is-magma-is-prop
+```
+-->
+
 By turning the operation parameter into an additional piece of data, we
 get the notion of a **magma structure** on a type, as well as the
 notion of a magma in general by doing the same to the carrier type.

diff --git a/src/Algebra/Magma/Unital/EckmannHilton.lagda.md b/src/Algebra/Magma/Unital/EckmannHilton.lagda.md
@@ -102,8 +102,8 @@ unitality allows us to prove that the operation is a monoid.
     x ⋆ (y ⋆ z) ∎)
 
   ⋆-is-monoid : is-monoid e _⋆_
-  ⋆-is-monoid .has-is-semigroup .has-is-magma = unital-mgm .has-is-magma
-  ⋆-is-monoid .has-is-semigroup .associative = ⋆-associative _ _ _
+  ⋆-is-monoid .has-is-semigroup .is-semigroup.has-is-magma = unital-mgm .has-is-magma
+  ⋆-is-monoid .has-is-semigroup .is-semigroup.associative = ⋆-associative _ _ _
   ⋆-is-monoid .idl = unital-mgm .idl
   ⋆-is-monoid .idr = unital-mgm .idr
 ```
diff --git a/src/Algebra/Monoid.lagda.md b/src/Algebra/Monoid.lagda.md
@@ -80,8 +80,6 @@ record Monoid-on (A : Type ℓ) : Type ℓ where
 
 Monoid : (ℓ : Level) → Type (lsuc ℓ)
 Monoid ℓ = Σ (Type ℓ) Monoid-on
-
-open Monoid-on
 ```
 
 There is also a predicate which witnesses when an equivalence between
@@ -125,7 +123,7 @@ First, we show that every monoid is a unital magma:
 ```agda
 module _ {id : A} {_⋆_ : A → A → A} where
   is-monoid→is-unital-magma : is-monoid id _⋆_ → is-unital-magma id _⋆_
-  is-monoid→is-unital-magma mon .has-is-magma = mon .has-is-semigroup .has-is-magma
+  is-monoid→is-unital-magma mon .has-is-magma = mon .has-is-magma
   is-monoid→is-unital-magma mon .idl = mon .idl
   is-monoid→is-unital-magma mon .idr = mon .idr
 ```
@@ -172,3 +170,33 @@ monoid-inverse-unique {1M = 1M} {_⋆_} m e x y li1 ri2 =
   1M ⋆ y        ≡⟨ m .idl ⟩
   y             ∎
 ```
+
+# Constructing monoids
+
+The interface to `Monoid-on`{.Agda} is contains some annoying nesting,
+so we provide an interface that arranges the data in a more user-friendly
+way.
+
+```agda
+record make-monoid {ℓ} (A : Type ℓ) : Type ℓ where
+  field
+    monoid-is-set : is-set A
+    _⋆_ : A → A → A
+    1M : A
+    ⋆-assoc : ∀ x y z → x ⋆ (y ⋆ z) ≡ (x ⋆ y) ⋆ z
+    ⋆-idl : ∀ x → 1M ⋆ x ≡ x
+    ⋆-idr : ∀ x → x ⋆ 1M ≡ x
+
+  to-is-monoid : is-monoid 1M _⋆_
+  to-is-monoid .has-is-semigroup .is-semigroup.has-is-magma = record { has-is-set = monoid-is-set }
+  to-is-monoid .has-is-semigroup .is-semigroup.associative = ⋆-assoc _ _ _
+  to-is-monoid .idl = ⋆-idl _
+  to-is-monoid .idr = ⋆-idr _
+
+  to-monoid-on : Monoid-on A
+  to-monoid-on .Monoid-on.identity = 1M
+  to-monoid-on .Monoid-on._⋆_ = _⋆_
+  to-monoid-on .Monoid-on.has-is-monoid = to-is-monoid
+
+open make-monoid using (to-is-monoid; to-monoid-on) public
+```
diff --git a/src/Algebra/Ring.lagda.md b/src/Algebra/Ring.lagda.md
@@ -231,37 +231,35 @@ record make-ring {ℓ} (R : Type ℓ) : Type ℓ where
 
 <!--
 ```agda
+  -- All in copatterns to prevent the unfolding from exploding on you
+  to-is-ring : is-ring 1R _*_ _+_
+  to-is-ring .is-ring.*-monoid .is-monoid.has-is-semigroup .is-semigroup.has-is-magma = record { has-is-set = ring-is-set }
+  to-is-ring .is-ring.*-monoid .is-monoid.has-is-semigroup .is-semigroup.associative = *-assoc _ _ _
+  to-is-ring .is-ring.*-monoid .is-monoid.idl = *-idl _
+  to-is-ring .is-ring.*-monoid .is-monoid.idr = *-idr _
+  to-is-ring .is-ring.+-group .is-abelian-group.has-is-group .is-group.unit = 0R
+  to-is-ring .is-ring.+-group .is-abelian-group.has-is-group .is-group.inverse = -_
+  to-is-ring .is-ring.+-group .is-abelian-group.has-is-group .is-group.has-is-monoid .is-monoid.has-is-semigroup .is-semigroup.has-is-magma = record { has-is-set = ring-is-set }
+  to-is-ring .is-ring.+-group .is-abelian-group.has-is-group .is-group.has-is-monoid .is-monoid.has-is-semigroup .is-semigroup.associative = +-assoc _ _ _
+  to-is-ring .is-ring.+-group .is-abelian-group.has-is-group .is-group.has-is-monoid .is-monoid.idl = +-idl _
+  to-is-ring .is-ring.+-group .is-abelian-group.has-is-group .is-group.has-is-monoid .is-monoid.idr = +-comm _ _ ∙ +-idl _
+  to-is-ring .is-ring.+-group .is-abelian-group.has-is-group .is-group.inversel = +-comm _ _ ∙ +-invr _
+  to-is-ring .is-ring.+-group .is-abelian-group.has-is-group .is-group.inverser = +-invr _
+  to-is-ring .is-ring.+-group .is-abelian-group.commutes = +-comm _ _
+  to-is-ring .is-ring.*-distribl = *-distribl _ _ _
+  to-is-ring .is-ring.*-distribr = *-distribr _ _ _
+
   to-ring-on : Ring-on R
-  to-ring-on = ring where
-    open is-ring hiding (-_ ; +-invr ; +-invl ; *-distribl ; *-distribr ; *-idl ; *-idr ; +-idl ; +-idr)
-    open is-monoid
-
-    -- All in copatterns to prevent the unfolding from exploding on you
-    ring : Ring-on R
-    ring .Ring-on.1r = 1R
-    ring .Ring-on._*_ = _*_
-    ring .Ring-on._+_ = _+_
-    ring .Ring-on.has-is-ring .*-monoid .has-is-semigroup .is-semigroup.has-is-magma = record { has-is-set = ring-is-set }
-    ring .Ring-on.has-is-ring .*-monoid .has-is-semigroup .is-semigroup.associative = *-assoc _ _ _
-    ring .Ring-on.has-is-ring .*-monoid .idl = *-idl _
-    ring .Ring-on.has-is-ring .*-monoid .idr = *-idr _
-    ring .Ring-on.has-is-ring .+-group .is-abelian-group.has-is-group .is-group.unit = 0R
-    ring .Ring-on.has-is-ring .+-group .is-abelian-group.has-is-group .is-group.has-is-monoid .has-is-semigroup .has-is-magma = record { has-is-set = ring-is-set }
-    ring .Ring-on.has-is-ring .+-group .is-abelian-group.has-is-group .is-group.has-is-monoid .has-is-semigroup .associative = +-assoc _ _ _
-    ring .Ring-on.has-is-ring .+-group .is-abelian-group.has-is-group .is-group.has-is-monoid .idl = +-idl _
-    ring .Ring-on.has-is-ring .+-group .is-abelian-group.has-is-group .is-group.has-is-monoid .idr = +-comm _ _ ∙ +-idl _
-    ring .Ring-on.has-is-ring .+-group .is-abelian-group.has-is-group .is-group.inverse = -_
-    ring .Ring-on.has-is-ring .+-group .is-abelian-group.has-is-group .is-group.inversel = +-comm _ _ ∙ +-invr _
-    ring .Ring-on.has-is-ring .+-group .is-abelian-group.has-is-group .is-group.inverser = +-invr _
-    ring .Ring-on.has-is-ring .+-group .is-abelian-group.commutes = +-comm _ _
-    ring .Ring-on.has-is-ring .is-ring.*-distribl = *-distribl _ _ _
-    ring .Ring-on.has-is-ring .is-ring.*-distribr = *-distribr _ _ _
+  to-ring-on .Ring-on.1r = 1R
+  to-ring-on .Ring-on._*_ = _*_
+  to-ring-on .Ring-on._+_ = _+_
+  to-ring-on .Ring-on.has-is-ring = to-is-ring
 
   to-ring : Ring ℓ
   to-ring .fst = el R ring-is-set
   to-ring .snd = to-ring-on
 
-open make-ring using (to-ring ; to-ring-on) public
+open make-ring using (to-is-ring; to-ring-on; to-ring) public
 ```
 -->
 

diff --git a/src/Algebra/Semigroup.lagda.md b/src/Algebra/Semigroup.lagda.md
@@ -34,7 +34,7 @@ equipped with a choice of _associative_ binary operation `⋆`.
 
   open is-magma has-is-magma public
 
-open is-semigroup public
+open is-semigroup
 ```
 
 To see why the [[set truncation]] is really necessary, it helps to
@@ -147,7 +147,7 @@ open import Data.Nat.Order
 open import Data.Nat.Base
 
 Nat-min : is-semigroup min
-Nat-min .has-is-magma .has-is-set = Nat-is-set
+Nat-min .has-is-magma .is-magma.has-is-set = Nat-is-set
 Nat-min .associative = min-assoc _ _ _
 ```
 
@@ -164,3 +164,27 @@ private
       sucx≤x = subst (λ e → e ≤ x) (id (suc x)) (min-≤l x (suc x))
     in ¬sucx≤x x sucx≤x
 ```
+
+# Constructing semigroups
+
+The interface to `Semigroup-on`{.Agda} is contains some annoying nesting,
+so we provide an interface that arranges the data in a more user-friendly
+way.
+
+```agda
+record make-semigroup {ℓ} (A : Type ℓ) : Type ℓ where
+  field
+    semigroup-is-set : is-set A
+    _⋆_ : A → A → A
+    ⋆-assoc : ∀ x y z → x ⋆ (y ⋆ z) ≡ (x ⋆ y) ⋆ z
+
+  to-is-semigroup : is-semigroup _⋆_
+  to-is-semigroup .has-is-magma .is-magma.has-is-set = semigroup-is-set
+  to-is-semigroup .associative = ⋆-assoc _ _ _
+
+  to-semigroup-on : Semigroup-on A
+  to-semigroup-on .fst = _⋆_
+  to-semigroup-on .snd = to-is-semigroup
+
+open make-semigroup using (to-is-semigroup; to-semigroup-on) public
+```
diff --git a/src/Cat/Monoidal/Diagram/Monoid/Representable.lagda.md b/src/Cat/Monoidal/Diagram/Monoid/Representable.lagda.md
@@ -92,37 +92,35 @@ $$.
 
 ```agda
   Mon→Hom-mon : ∀ {m} (x : Ob) → C-Monoid m → Monoid-on (Hom x m)
-  Mon→Hom-mon {m} x mon = hom-mon where
-    has-semigroup : is-semigroup λ f g → mon .μ ∘ ⟨ f , g ⟩
-    hom-mon : Monoid-on (Hom x m)
+  Mon→Hom-mon {m} x mon = to-monoid-on hom-mon where
+    open make-monoid
 
-    hom-mon .Monoid-on.identity = mon .η ∘ !
-    hom-mon .Monoid-on._⋆_ f g  = mon .μ ∘ ⟨ f , g ⟩
+    hom-mon : make-monoid (Hom x m)
+    hom-mon .monoid-is-set = hlevel 2
+    hom-mon ._⋆_ f g = mon .μ ∘ ⟨ f , g ⟩
+    hom-mon .1M = mon .η ∘ !
 ```
 
 <details>
 <summary>It's not very hard to show that the monoid laws from the
 diagram "relativize" to each $\hom$-set.</summary>
 
 ```agda
-    hom-mon .Monoid-on.has-is-monoid .has-is-semigroup = has-semigroup
-    hom-mon .Monoid-on.has-is-monoid .mon-idl {f} =
+    hom-mon .⋆-assoc f g h =
+      mon .μ ∘ ⟨ f , mon .μ ∘ ⟨ g , h ⟩ ⟩                                            ≡⟨ products! C prod ⟩
+      mon .μ ∘ (id ⊗₁ mon .μ) ∘ ⟨ f , ⟨ g , h ⟩ ⟩                                    ≡⟨ extendl (mon .μ-assoc) ⟩
+      mon .μ ∘ ((mon .μ ⊗₁ id) ∘ ⟨ ⟨ π₁ , π₁ ∘ π₂ ⟩ , π₂ ∘ π₂ ⟩) ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≡⟨ products! C prod ⟩
+      mon .μ ∘ ⟨ mon .μ ∘ ⟨ f , g ⟩ , h ⟩                                            ∎
+    hom-mon .⋆-idl f =
       mon .μ ∘ ⟨ mon .η ∘ ! , f ⟩         ≡⟨ products! C prod ⟩
       mon .μ ∘ (mon .η ⊗₁ id) ∘ ⟨ ! , f ⟩ ≡⟨ pulll (mon .μ-unitl) ⟩
       π₂ ∘ ⟨ ! , f ⟩                      ≡⟨ π₂∘⟨⟩ ⟩
       f                                   ∎
-    hom-mon .Monoid-on.has-is-monoid .mon-idr {f} =
+    hom-mon .⋆-idr f =
       mon .μ ∘ ⟨ f , mon .η ∘ ! ⟩         ≡⟨ products! C prod ⟩
       mon .μ ∘ (id ⊗₁ mon .η) ∘ ⟨ f , ! ⟩ ≡⟨ pulll (mon .μ-unitr) ⟩
       π₁ ∘ ⟨ f , ! ⟩                      ≡⟨ π₁∘⟨⟩ ⟩
       f                                   ∎
-
-    has-semigroup .has-is-magma .has-is-set = Hom-set _ _
-    has-semigroup .associative {f} {g} {h} =
-      mon .μ ∘ ⟨ f , mon .μ ∘ ⟨ g , h ⟩ ⟩                                            ≡⟨ products! C prod ⟩
-      mon .μ ∘ (id ⊗₁ mon .μ) ∘ ⟨ f , ⟨ g , h ⟩ ⟩                                    ≡⟨ extendl (mon .μ-assoc) ⟩
-      mon .μ ∘ ((mon .μ ⊗₁ id) ∘ ⟨ ⟨ π₁ , π₁ ∘ π₂ ⟩ , π₂ ∘ π₂ ⟩) ∘ ⟨ f , ⟨ g , h ⟩ ⟩ ≡⟨ products! C prod ⟩
-      mon .μ ∘ ⟨ mon .μ ∘ ⟨ f , g ⟩ , h ⟩                                            ∎
 ```
 
 </details>
@@ -385,7 +383,7 @@ object $M : \cC$.
     : ∀ (P : Functor (C ^op) (Monoids ℓ))
     → (P-rep : Representation {C = C} (Mon↪Sets F∘ P))
     → C-Monoid (P-rep .rep)
-  RepPshMon→Mon P P-rep = Hom-mon→Mon hom-mon η*-nat μ*-nat
+  RepPshMon→Mon P P-rep = Hom-mon→Mon (λ x → to-monoid-on (hom-mon x)) η*-nat μ*-nat
     module RepPshMon→Mon where
 ```
 
@@ -453,14 +451,13 @@ the monoid structure $P(x)$ to a monoid structure on $x \to M$.
 
 <!--
 ```agda
-    hom-mon : ∀ x → Monoid-on (Hom x m)
-    hom-mon x .Monoid-on.identity = η* x
-    hom-mon x .Monoid-on._⋆_ = μ*
-    hom-mon x .Monoid-on.has-is-monoid .has-is-semigroup .has-is-magma .has-is-set =
-      Hom-set x m
-    hom-mon x .Monoid-on.has-is-monoid .has-is-semigroup .associative = μ*-assoc _ _ _
-    hom-mon x .Monoid-on.has-is-monoid .mon-idl = η*-idl _
-    hom-mon x .Monoid-on.has-is-monoid .mon-idr = η*-idr _
+    hom-mon : ∀ x → make-monoid (Hom x m)
+    hom-mon x .make-monoid.monoid-is-set = hlevel 2
+    hom-mon x .make-monoid._⋆_ = μ*
+    hom-mon x .make-monoid.1M = η* x
+    hom-mon x .make-monoid.⋆-assoc = μ*-assoc
+    hom-mon x .make-monoid.⋆-idl = η*-idl
+    hom-mon x .make-monoid.⋆-idr = η*-idr
 ```
 -->
 

diff --git a/src/Order/Diagram/Join/Reasoning.lagda.md b/src/Order/Diagram/Join/Reasoning.lagda.md
@@ -72,8 +72,12 @@ Furthermore, it is associative, and thus forms a [[semigroup]].
         (≤-trans r≤∪ r≤∪))
 
   ∪-is-semigroup : is-semigroup _∪_
-  ∪-is-semigroup .has-is-magma .has-is-set = Ob-is-set
-  ∪-is-semigroup .associative = ∪-assoc
+  ∪-is-semigroup =
+    to-is-semigroup λ where
+      .semigroup-is-set → hlevel 2
+      ._⋆_ → _∪_
+      .⋆-assoc _ _ _ → ∪-assoc
+    where open make-semigroup
 ```
 
 Additionally, it respects the ordering on $P$, in each variable.

diff --git a/src/Order/Diagram/Meet/Reasoning.lagda.md b/src/Order/Diagram/Meet/Reasoning.lagda.md
@@ -72,8 +72,12 @@ Furthermore, it is associative, and thus forms a [[semigroup]].
         (∩-universal _ (≤-trans ∩≤l ∩≤r) ∩≤r))
 
   ∩-is-semigroup : is-semigroup _∩_
-  ∩-is-semigroup .has-is-magma .has-is-set = Ob-is-set
-  ∩-is-semigroup .associative = ∩-assoc
+  ∩-is-semigroup =
+    to-is-semigroup λ where
+      .semigroup-is-set → hlevel 2
+      ._⋆_ → _∩_
+      .⋆-assoc _ _ _ → ∩-assoc
+    where open make-semigroup
 ```
 
 Additionally, it respects the ordering on $P$, in each variable.