chore: misc. algebra improvements

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

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
 

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.

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

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
+```

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

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
+```

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

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.

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.