diff --git a/src/Algebra/Module/Morphism/Structures.agda b/src/Algebra/Module/Morphism/Structures.agda
index e874f4d341..6dac17e22d 100644
--- a/src/Algebra/Module/Morphism/Structures.agda
+++ b/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 ⟦_⟧
diff --git a/src/Algebra/Morphism/MagmaMonomorphism.agda b/src/Algebra/Morphism/MagmaMonomorphism.agda
index fbe08a5861..88bc6171d1 100644
--- a/src/Algebra/Morphism/MagmaMonomorphism.agda
+++ b/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 ⟧          ≈⟨ ∙-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) ⟧          ∎)
 
   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 ⟧  ≈⟨ ∙-homo x y ⟨
     ⟦ x ∙ y ⟧      ≈⟨  ⟦⟧-cong x∙y≈x∙z ⟩
-    ⟦ x ∙ z ⟧      ≈⟨  homo 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 _≈₁_ _∙_
diff --git a/src/Algebra/Morphism/MonoidMonomorphism.agda b/src/Algebra/Morphism/MonoidMonomorphism.agda
index 1b918295af..b720360cad 100644
--- a/src/Algebra/Morphism/MonoidMonomorphism.agda
+++ b/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 ⟨
     ⟦ ε₁ ⟧         ∎)
 
diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda
index 4669e479d9..4ed02a9dca 100644
--- a/src/Data/Nat/Binary/Properties.agda
+++ b/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ℕ