refactor: cosmetic improvement over #2546 (#2759)

Author: jamesmckinna

CHANGELOG.md

@@ -201,6 +201,12 @@ Additions to existing modules
     ∙-congʳ : RightCongruent _≈_ _∙_
   ```
 
+* In `Algebra.Construct.Initial`:
+  ```agda
+  assoc : Associative _≈_ _∙_
+  idem  : Idempotent _≈_ _∙_
+  ```
+
 * In `Algebra.Construct.Pointwise`:
   ```agda
   isNearSemiring                  : IsNearSemiring _≈_ _+_ _*_ 0# →

src/Algebra/Construct/Initial.agda

@@ -19,7 +19,7 @@ open import Algebra.Bundles
 open import Algebra.Bundles.Raw
   using (RawMagma)
 open import Algebra.Core using (Op₂)
-open import Algebra.Definitions using (Congruent₂)
+open import Algebra.Definitions using (Congruent₂; Associative; Idempotent)
 open import Algebra.Structures using (IsMagma; IsSemigroup; IsBand)
 open import Data.Empty.Polymorphic using (⊥)
 open import Relation.Binary.Core using (Rel)
@@ -63,6 +63,12 @@ module ℤero where
   ∙-cong : Congruent₂ _≈_ _∙_
   ∙-cong {x = ()}
 
+  assoc : Associative _≈_ _∙_
+  assoc ()
+
+  idem : Idempotent _≈_ _∙_
+  idem ()
+
 open ℤero
 
 ------------------------------------------------------------------------
@@ -75,16 +81,16 @@ rawMagma = record { ℤero }
 -- Structures
 
 isEquivalence : IsEquivalence _≈_
-isEquivalence = record { refl = refl; sym = sym; trans = λ {k = k} → trans {k = k} }
+isEquivalence = record { refl = refl; sym = sym; trans = λ where {i = ()} }
 
 isMagma : IsMagma _≈_ _∙_
-isMagma = record { isEquivalence = isEquivalence ; ∙-cong = λ {y = y} {u = u} {v = v} → ∙-cong {y = y} {v = v} }
+isMagma = record { isEquivalence = isEquivalence ; ∙-cong = λ where {x = ()} }
 
 isSemigroup : IsSemigroup _≈_ _∙_
-isSemigroup = record { isMagma = isMagma ; assoc = λ () }
+isSemigroup = record { isMagma = isMagma ; assoc = assoc }
 
 isBand : IsBand _≈_ _∙_
-isBand = record { isSemigroup = isSemigroup ; idem = λ () }
+isBand = record { isSemigroup = isSemigroup ; idem = idem }
 
 ------------------------------------------------------------------------
 -- Bundles