Rename homo to ∙-homo in Algebra.Morphism.Structures

CHANGELOG.md

@@ -32,6 +32,11 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Algebra.Morphism.Structures`:
+  ```agda
+  homo  ↦  ∙-homo
+  ```
+
 * In `Algebra.Properties.CommutativeMagma.Divisibility`:
   ```agda
   ∣-factors    ↦  x|xy∧y|xy

src/Algebra/Lattice/Morphism/Structures.agda

@@ -58,13 +58,13 @@ module LatticeMorphisms (L₁ : RawLattice a ℓ₁) (L₂ : RawLattice b ℓ₂
     ∧-isMagmaHomomorphism : ∧.IsMagmaHomomorphism ⟦_⟧
     ∧-isMagmaHomomorphism = record
       { isRelHomomorphism = isRelHomomorphism
-      ; homo = ∧-homo
+      ; ∙-homo = ∧-homo
       }
 
     ∨-isMagmaHomomorphism : ∨.IsMagmaHomomorphism ⟦_⟧
     ∨-isMagmaHomomorphism = record
       { isRelHomomorphism = isRelHomomorphism
-      ; homo = ∨-homo
+      ; ∙-homo = ∨-homo
       }
 
   record IsLatticeMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where

src/Algebra/Module/Morphism/Structures.agda

@@ -35,7 +35,7 @@ module LeftSemimoduleMorphisms
 
     open IsMonoidHomomorphism +ᴹ-isMonoidHomomorphism public
       using (isRelHomomorphism; ⟦⟧-cong)
-      renaming (isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo)
+      renaming (isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; ∙-homo to +ᴹ-homo; ε-homo to 0ᴹ-homo)
 
   record IsLeftSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
@@ -91,7 +91,7 @@ module LeftModuleMorphisms
     open IsGroupHomomorphism +ᴹ-isGroupHomomorphism public
       using (isRelHomomorphism; ⟦⟧-cong)
       renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism
-               ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo
+               ; ∙-homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo
                )
 
     isLeftSemimoduleHomomorphism : IsLeftSemimoduleHomomorphism ⟦_⟧
@@ -162,7 +162,7 @@ module RightSemimoduleMorphisms
 
     open IsMonoidHomomorphism +ᴹ-isMonoidHomomorphism public
       using (isRelHomomorphism; ⟦⟧-cong)
-      renaming (isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo)
+      renaming (isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; ∙-homo to +ᴹ-homo; ε-homo to 0ᴹ-homo)
 
   record IsRightSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
@@ -218,7 +218,7 @@ module RightModuleMorphisms
     open IsGroupHomomorphism +ᴹ-isGroupHomomorphism public
       using (isRelHomomorphism; ⟦⟧-cong)
       renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism
-               ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo
+               ; ∙-homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo
                )
     isRightSemimoduleHomomorphism : IsRightSemimoduleHomomorphism ⟦_⟧
     isRightSemimoduleHomomorphism = record
@@ -375,7 +375,7 @@ module BimoduleMorphisms
     open IsGroupHomomorphism +ᴹ-isGroupHomomorphism public
       using (isRelHomomorphism; ⟦⟧-cong)
       renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism
-               ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo
+               ; ∙-homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo
                )
 
     isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism ⟦_⟧

src/Algebra/Morphism/Bundles.agda

@@ -13,8 +13,6 @@ module Algebra.Morphism.Bundles where
 open import Algebra.Bundles.Raw
 open import Algebra.Morphism.Structures
 open import Level using (Level; suc; _⊔_)
---open import Relation.Binary.Morphism using (IsRelHomomorphism)
---open import Relation.Binary.Morphism.Bundles using (SetoidHomomorphism)
 
 private
   variable
@@ -160,7 +158,9 @@ record KleeneAlgebraHomomorphism
   semiringHomomorphism = record { isSemiringHomomorphism = isSemiringHomomorphism }
 
   open SemiringHomomorphism semiringHomomorphism public
-    hiding (*-isMagmaHomomorphism; *-isMonoidHomomorphism)
+    using ( nearSemiringHomomorphism
+          ; *-monoidHomomorphism; *-magmaHomomorphism
+          ; +-monoidHomomorphism; +-magmaHomomorphism)
 
 ------------------------------------------------------------------------
 -- Morphisms between RingWithoutOnes

src/Algebra/Morphism/Construct/Composition.agda

@@ -40,7 +40,7 @@ module _ {M₁ : RawMagma a ℓ₁}
     → IsMagmaHomomorphism M₁ M₃ (g ∘ f)
   isMagmaHomomorphism f-homo g-homo = record
     { isRelHomomorphism = isRelHomomorphism F.isRelHomomorphism G.isRelHomomorphism
-    ; homo              = λ x y → ≈₃-trans (G.⟦⟧-cong (F.homo x y)) (G.homo (f x) (f y))
+    ; ∙-homo            = λ x y → ≈₃-trans (G.⟦⟧-cong (F.homo x y)) (G.homo (f x) (f y))
     } where module F = IsMagmaHomomorphism f-homo; module G = IsMagmaHomomorphism g-homo
 
   isMagmaMonomorphism

src/Algebra/Morphism/Construct/Identity.agda

@@ -42,7 +42,7 @@ module _ (M : RawMagma c ℓ) (open RawMagma M) (refl : Reflexive _≈_) where
   isMagmaHomomorphism : IsMagmaHomomorphism id
   isMagmaHomomorphism = record
     { isRelHomomorphism = isRelHomomorphism _
-    ; homo              = λ _ _ → refl
+    ; ∙-homo            = λ _ _ → refl
     }
 
   isMagmaMonomorphism : IsMagmaMonomorphism id

src/Algebra/Morphism/Construct/Initial.agda

@@ -51,7 +51,7 @@ isMagmaHomomorphism : (M : RawMagma m ℓm) →
                       IsMagmaHomomorphism rawMagma M zero
 isMagmaHomomorphism M = record
   { isRelHomomorphism = record { cong = cong (RawMagma._≈_ M) }
-  ; homo = λ()
+  ; ∙-homo = λ()
   }
 
 isMagmaMonomorphism : (M : RawMagma m ℓm) →

src/Algebra/Morphism/Construct/Terminal.agda

@@ -50,7 +50,7 @@ isMagmaHomomorphism : (M : RawMagma a ℓa) →
                       IsMagmaHomomorphism M rawMagma one
 isMagmaHomomorphism M = record
   { isRelHomomorphism = record { cong = _ }
-  ; homo = _
+  ; ∙-homo = _
   }
 
 isMonoidHomomorphism : (M : RawMonoid a ℓa) →

src/Algebra/Morphism/MagmaMonomorphism.agda

@@ -40,56 +40,56 @@ module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
 
   cong : Congruent₂ _≈₁_ _∙_
   cong {x} {y} {u} {v} x≈y u≈v = injective (begin
-    ⟦ x ∙ u ⟧      ≈⟨  homo x u ⟩
-    ⟦ x ⟧ ◦ ⟦ u ⟧  ≈⟨  ◦-cong (⟦⟧-cong x≈y) (⟦⟧-cong u≈v) ⟩
-    ⟦ y ⟧ ◦ ⟦ v ⟧  ≈⟨ homo y v ⟨
+    ⟦ x ∙ u ⟧      ≈⟨ ∙-homo x u ⟩
+    ⟦ x ⟧ ◦ ⟦ u ⟧  ≈⟨ ◦-cong (⟦⟧-cong x≈y) (⟦⟧-cong u≈v) ⟩
+    ⟦ y ⟧ ◦ ⟦ v ⟧  ≈⟨ ∙-homo y v ⟨
     ⟦ y ∙ v ⟧      ∎)
 
   assoc : Associative _≈₂_ _◦_ → Associative _≈₁_ _∙_
   assoc assoc x y z = injective (begin
-    ⟦ (x ∙ y) ∙ z ⟧          ≈⟨  homo (x ∙ y) z ⟩
-    ⟦ x ∙ y ⟧ ◦ ⟦ z ⟧        ≈⟨  ◦-cong (homo x y) refl ⟩
-    (⟦ x ⟧ ◦ ⟦ y ⟧) ◦ ⟦ z ⟧  ≈⟨  assoc ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ ⟩
-    ⟦ x ⟧ ◦ (⟦ y ⟧ ◦ ⟦ z ⟧)  ≈⟨ ◦-cong refl (homo y z) ⟨
-    ⟦ x ⟧ ◦ ⟦ y ∙ z ⟧        ≈⟨ homo x (y ∙ z) ⟨
+    ⟦ (x ∙ y) ∙ z ⟧          ≈⟨ ∙-homo (x ∙ y) z ⟩
+    ⟦ x ∙ y ⟧ ◦ ⟦ z ⟧        ≈⟨ ◦-cong (∙-homo x y) refl ⟩
+    (⟦ x ⟧ ◦ ⟦ y ⟧) ◦ ⟦ z ⟧  ≈⟨ assoc ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ ⟩
+    ⟦ x ⟧ ◦ (⟦ y ⟧ ◦ ⟦ z ⟧)  ≈⟨ ◦-cong refl (∙-homo y z) ⟨
+    ⟦ x ⟧ ◦ ⟦ y ∙ z ⟧        ≈⟨ ∙-homo x (y ∙ z) ⟨
     ⟦ x ∙ (y ∙ z) ⟧          ∎)
 
   comm : Commutative _≈₂_ _◦_ → Commutative _≈₁_ _∙_
   comm comm x y = injective (begin
-    ⟦ x ∙ y ⟧      ≈⟨  homo x y ⟩
-    ⟦ x ⟧ ◦ ⟦ y ⟧  ≈⟨  comm ⟦ x ⟧ ⟦ y ⟧ ⟩
-    ⟦ y ⟧ ◦ ⟦ x ⟧  ≈⟨ homo y x ⟨
+    ⟦ x ∙ y ⟧      ≈⟨ ∙-homo x y ⟩
+    ⟦ x ⟧ ◦ ⟦ y ⟧  ≈⟨ comm ⟦ x ⟧ ⟦ y ⟧ ⟩
+    ⟦ y ⟧ ◦ ⟦ x ⟧  ≈⟨ ∙-homo y x ⟨
     ⟦ y ∙ x ⟧      ∎)
 
   idem : Idempotent _≈₂_ _◦_ → Idempotent _≈₁_ _∙_
   idem idem x = injective (begin
-    ⟦ x ∙ x ⟧     ≈⟨ homo x x ⟩
+    ⟦ x ∙ x ⟧     ≈⟨ ∙-homo x x ⟩
     ⟦ x ⟧ ◦ ⟦ x ⟧ ≈⟨ idem ⟦ x ⟧ ⟩
     ⟦ x ⟧         ∎)
 
   sel : Selective _≈₂_ _◦_ → Selective _≈₁_ _∙_
   sel sel x y with sel ⟦ x ⟧ ⟦ y ⟧
   ... | inj₁ x◦y≈x = inj₁ (injective (begin
-    ⟦ x ∙ y ⟧      ≈⟨ homo x y ⟩
+    ⟦ x ∙ y ⟧      ≈⟨ ∙-homo x y ⟩
     ⟦ x ⟧ ◦ ⟦ y ⟧  ≈⟨ x◦y≈x ⟩
     ⟦ x ⟧          ∎))
   ... | inj₂ x◦y≈y = inj₂ (injective (begin
-    ⟦ x ∙ y ⟧      ≈⟨ homo x y ⟩
+    ⟦ x ∙ y ⟧      ≈⟨ ∙-homo x y ⟩
     ⟦ x ⟧ ◦ ⟦ y ⟧  ≈⟨ x◦y≈y ⟩
     ⟦ y ⟧          ∎))
 
   cancelˡ : LeftCancellative _≈₂_ _◦_ → LeftCancellative _≈₁_ _∙_
   cancelˡ cancelˡ x y z x∙y≈x∙z = injective (cancelˡ ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ (begin
-    ⟦ x ⟧ ◦ ⟦ y ⟧  ≈⟨ homo x y ⟨
-    ⟦ x ∙ y ⟧      ≈⟨  ⟦⟧-cong x∙y≈x∙z ⟩
-    ⟦ x ∙ z ⟧      ≈⟨  homo x z ⟩
+    ⟦ x ⟧ ◦ ⟦ y ⟧  ≈⟨ ∙-homo x y ⟨
+    ⟦ x ∙ y ⟧      ≈⟨ ⟦⟧-cong x∙y≈x∙z ⟩
+    ⟦ x ∙ z ⟧      ≈⟨ ∙-homo x z ⟩
     ⟦ x ⟧ ◦ ⟦ z ⟧  ∎))
 
   cancelʳ : RightCancellative _≈₂_ _◦_ → RightCancellative _≈₁_ _∙_
   cancelʳ cancelʳ x y z y∙x≈z∙x = injective (cancelʳ ⟦ x ⟧ ⟦ y ⟧ ⟦ z ⟧ (begin
-    ⟦ y ⟧ ◦ ⟦ x ⟧  ≈⟨ homo y x ⟨
-    ⟦ y ∙ x ⟧      ≈⟨  ⟦⟧-cong y∙x≈z∙x ⟩
-    ⟦ z ∙ x ⟧      ≈⟨  homo z x ⟩
+    ⟦ y ⟧ ◦ ⟦ x ⟧  ≈⟨ ∙-homo y x ⟨
+    ⟦ y ∙ x ⟧      ≈⟨ ⟦⟧-cong y∙x≈z∙x ⟩
+    ⟦ z ∙ x ⟧      ≈⟨ ∙-homo z x ⟩
     ⟦ z ⟧ ◦ ⟦ x ⟧  ∎))
 
   cancel : Cancellative _≈₂_ _◦_ → Cancellative _≈₁_ _∙_

src/Algebra/Morphism/MonoidMonomorphism.agda

@@ -43,14 +43,14 @@ module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
 
   identityˡ : LeftIdentity _≈₂_ ε₂ _◦_ → LeftIdentity _≈₁_ ε₁ _∙_
   identityˡ idˡ x = injective (begin
-    ⟦ ε₁ ∙ x ⟧      ≈⟨ homo ε₁ x ⟩
+    ⟦ ε₁ ∙ x ⟧      ≈⟨ ∙-homo ε₁ x ⟩
     ⟦ ε₁ ⟧ ◦ ⟦ x ⟧  ≈⟨ ◦-cong ε-homo refl ⟩
     ε₂ ◦ ⟦ x ⟧      ≈⟨ idˡ ⟦ x ⟧ ⟩
     ⟦ x ⟧           ∎)
 
   identityʳ : RightIdentity _≈₂_ ε₂ _◦_ → RightIdentity _≈₁_ ε₁ _∙_
   identityʳ idʳ x = injective (begin
-    ⟦ x ∙ ε₁ ⟧      ≈⟨ homo x ε₁ ⟩
+    ⟦ x ∙ ε₁ ⟧      ≈⟨ ∙-homo x ε₁ ⟩
     ⟦ x ⟧ ◦ ⟦ ε₁ ⟧  ≈⟨ ◦-cong refl ε-homo ⟩
     ⟦ x ⟧ ◦ ε₂      ≈⟨ idʳ ⟦ x ⟧ ⟩
     ⟦ x ⟧           ∎)
@@ -60,17 +60,17 @@ module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
 
   zeroˡ : LeftZero _≈₂_ ε₂ _◦_ → LeftZero _≈₁_ ε₁ _∙_
   zeroˡ zeˡ x = injective (begin
-    ⟦ ε₁ ∙ x ⟧     ≈⟨  homo ε₁ x ⟩
-    ⟦ ε₁ ⟧ ◦ ⟦ x ⟧ ≈⟨  ◦-cong ε-homo refl ⟩
-    ε₂   ◦ ⟦ x ⟧   ≈⟨  zeˡ ⟦ x ⟧ ⟩
+    ⟦ ε₁ ∙ x ⟧     ≈⟨ ∙-homo ε₁ x ⟩
+    ⟦ ε₁ ⟧ ◦ ⟦ x ⟧ ≈⟨ ◦-cong ε-homo refl ⟩
+    ε₂   ◦ ⟦ x ⟧   ≈⟨ zeˡ ⟦ x ⟧ ⟩
     ε₂             ≈⟨ ε-homo ⟨
     ⟦ ε₁ ⟧         ∎)
 
   zeroʳ : RightZero _≈₂_ ε₂ _◦_ → RightZero _≈₁_ ε₁ _∙_
   zeroʳ zeʳ x = injective (begin
-    ⟦ x ∙ ε₁ ⟧     ≈⟨  homo x ε₁ ⟩
-    ⟦ x ⟧ ◦ ⟦ ε₁ ⟧ ≈⟨  ◦-cong refl ε-homo ⟩
-    ⟦ x ⟧ ◦ ε₂     ≈⟨  zeʳ ⟦ x ⟧ ⟩
+    ⟦ x ∙ ε₁ ⟧     ≈⟨ ∙-homo x ε₁ ⟩
+    ⟦ x ⟧ ◦ ⟦ ε₁ ⟧ ≈⟨ ◦-cong refl ε-homo ⟩
+    ⟦ x ⟧ ◦ ε₂     ≈⟨ zeʳ ⟦ x ⟧ ⟩
     ε₂             ≈⟨ ε-homo ⟨
     ⟦ ε₁ ⟧         ∎)
 

src/Algebra/Morphism/Structures.agda

@@ -83,7 +83,14 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher
   record IsMagmaHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
-      homo              : Homomorphic₂ ⟦_⟧ _∙_ _◦_
+      ∙-homo            : Homomorphic₂ ⟦_⟧ _∙_ _◦_
+
+    -- Deprecated.
+    homo = ∙-homo
+    {-# WARNING_ON_USAGE homo
+    "Warning: homo was deprecated in v2.2.
+    Please use ∙-homo instead. "
+    #-}
 
     open IsRelHomomorphism isRelHomomorphism public
       renaming (cong to ⟦⟧-cong)
@@ -200,7 +207,6 @@ module GroupMorphisms (G₁ : RawGroup a ℓ₁) (G₂ : RawGroup b ℓ₂) wher
       injective           : Injective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsGroupHomomorphism isGroupHomomorphism public
-      renaming (homo to ∙-homo)
 
     isMonoidMonomorphism : IsMonoidMonomorphism ⟦_⟧
     isMonoidMonomorphism = record
@@ -265,13 +271,13 @@ module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSe
     *-isMagmaHomomorphism : *.IsMagmaHomomorphism ⟦_⟧
     *-isMagmaHomomorphism = record
       { isRelHomomorphism = isRelHomomorphism
-      ; homo = *-homo
+      ; ∙-homo = *-homo
       }
 
   record IsNearSemiringMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧
-      injective          : Injective _≈₁_ _≈₂_ ⟦_⟧
+      injective                  : Injective _≈₁_ _≈₂_ ⟦_⟧
 
     open IsNearSemiringHomomorphism isNearSemiringHomomorphism public
 
@@ -439,7 +445,7 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi
     *-isMagmaHomomorphism : *.IsMagmaHomomorphism ⟦_⟧
     *-isMagmaHomomorphism = record
       { isRelHomomorphism = isRelHomomorphism
-      ; homo = *-homo
+      ; ∙-homo = *-homo
       }
 
   record IsRingWithoutOneMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -452,7 +458,7 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi
     +-isGroupMonomorphism : +.IsGroupMonomorphism ⟦_⟧
     +-isGroupMonomorphism = record
       { isGroupHomomorphism = +-isGroupHomomorphism
-      ; injective            = injective
+      ; injective           = injective
       }
 
     open +.IsGroupMonomorphism +-isGroupMonomorphism public
@@ -475,7 +481,7 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi
     +-isGroupIsomorphism   : +.IsGroupIsomorphism ⟦_⟧
     +-isGroupIsomorphism  = record
       { isGroupMonomorphism = +-isGroupMonomorphism
-      ; surjective           = surjective
+      ; surjective          = surjective
       }
 
     open +.IsGroupIsomorphism +-isGroupIsomorphism public
@@ -641,19 +647,19 @@ module QuasigroupMorphisms (Q₁ : RawQuasigroup a ℓ₁) (Q₂ : RawQuasigroup
     ∙-isMagmaHomomorphism : ∙.IsMagmaHomomorphism ⟦_⟧
     ∙-isMagmaHomomorphism = record
       { isRelHomomorphism = isRelHomomorphism
-      ; homo = ∙-homo
+      ; ∙-homo = ∙-homo
       }
 
     \\-isMagmaHomomorphism : \\.IsMagmaHomomorphism ⟦_⟧
     \\-isMagmaHomomorphism = record
       { isRelHomomorphism  = isRelHomomorphism
-      ; homo = \\-homo
+      ; ∙-homo = \\-homo
       }
 
     //-isMagmaHomomorphism : //.IsMagmaHomomorphism ⟦_⟧
     //-isMagmaHomomorphism = record
       { isRelHomomorphism  = isRelHomomorphism
-      ; homo = //-homo
+      ; ∙-homo = //-homo
       }
 
   record IsQuasigroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where

src/Data/Integer/Properties.agda

@@ -1645,7 +1645,7 @@ i*j≢0 i j rewrite abs-* i j = ℕ.m*n≢0 ∣ i ∣ ∣ j ∣
 ^-isMagmaHomomorphism : ∀ i → Morphism.IsMagmaHomomorphism ℕ.+-rawMagma *-rawMagma (i ^_)
 ^-isMagmaHomomorphism i = record
   { isRelHomomorphism = record { cong = cong (i ^_) }
-  ; homo              = ^-distribˡ-+-* i
+  ; ∙-homo            = ^-distribˡ-+-* i
   }
 
 ^-isMonoidHomomorphism : ∀ i → Morphism.IsMonoidHomomorphism ℕ.+-0-rawMonoid *-1-rawMonoid (i ^_)

src/Data/List/Effectful/Foldable.agda

@@ -72,7 +72,7 @@ module _ (M : Monoid c ℓ) (f : A → Monoid.Carrier M) where
     { isMagmaHomomorphism = record
       { isRelHomomorphism = record
         { cong = reflexive ∘ ≡.cong h }
-      ; homo = λ xs _ → ++-homo xs
+      ; ∙-homo = λ xs _ → ++-homo xs
       }
     ; ε-homo = []-homo
     }

src/Data/List/Properties.agda

@@ -229,7 +229,7 @@ module _ (A : Set a) where
     { isRelHomomorphism = record
       { cong = cong length
       }
-    ; homo = λ xs ys → length-++ xs {ys}
+    ; ∙-homo = λ xs ys → length-++ xs {ys}
     }
 
   length-isMonoidHomomorphism : IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length

src/Data/Nat/Binary/Properties.agda

@@ -699,7 +699,7 @@ toℕ-homo-+ 1+[2 x ] 1+[2 y ] = begin
 toℕ-isMagmaHomomorphism-+ : IsMagmaHomomorphism +-rawMagma ℕ.+-rawMagma toℕ
 toℕ-isMagmaHomomorphism-+ = record
   { isRelHomomorphism = toℕ-isRelHomomorphism
-  ; homo              = toℕ-homo-+
+  ; ∙-homo            = toℕ-homo-+
   }
 
 toℕ-isMonoidHomomorphism-+ : IsMonoidHomomorphism +-0-rawMonoid ℕ.+-0-rawMonoid toℕ
@@ -1012,7 +1012,7 @@ toℕ-homo-* x y =  aux x y (size x ℕ.+ size y) ℕ.≤-refl
 toℕ-isMagmaHomomorphism-* : IsMagmaHomomorphism *-rawMagma ℕ.*-rawMagma toℕ
 toℕ-isMagmaHomomorphism-* = record
   { isRelHomomorphism = toℕ-isRelHomomorphism
-  ; homo              = toℕ-homo-*
+  ; ∙-homo            = toℕ-homo-*
   }
 
 toℕ-isMonoidHomomorphism-* : IsMonoidHomomorphism *-1-rawMonoid ℕ.*-1-rawMonoid toℕ

src/Data/Parity/Properties.agda

@@ -422,7 +422,7 @@ toSign-isMagmaHomomorphism : IsMagmaHomomorphism ℙ.+-rawMagma 𝕊.*-rawMagma
 toSign-isMagmaHomomorphism = record
   { isRelHomomorphism = record
     { cong = cong toSign }
-  ; homo = +-homo-*
+  ; ∙-homo = +-homo-*
   }
 
 toSign-isMagmaMonomorphism : IsMagmaMonomorphism ℙ.+-rawMagma 𝕊.*-rawMagma toSign
@@ -532,7 +532,7 @@ parity-isMagmaHomomorphism : IsMagmaHomomorphism ℕ.+-rawMagma ℙ.+-rawMagma p
 parity-isMagmaHomomorphism = record
   { isRelHomomorphism = record
     { cong = cong parity }
-  ; homo = +-homo-+
+  ; ∙-homo = +-homo-+
   }
 
 parity-isMonoidHomomorphism : IsMonoidHomomorphism ℕ.+-0-rawMonoid ℙ.+-0-rawMonoid parity