diff --git a/CHANGELOG.md b/CHANGELOG.md
index 38c13e12be..ff7916cf92 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -151,6 +151,12 @@ Additions to existing modules
   ⊕-∧-booleanRing   : BooleanRing _ _
   ```
 
+* In `Algebra.Morphism.Structures.IsMagmaHomomorphism`:
+  ```agda
+  ⟦_⟧∙_ : A → B → B
+  _∙⟦_⟧ : B → A → B
+  ```
+
 * In `Algebra.Properties.RingWithoutOne`:
   ```agda
   [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y
diff --git a/src/Algebra/Lattice/Morphism/Structures.agda b/src/Algebra/Lattice/Morphism/Structures.agda
index f56235c2b0..1f12d1ef9a 100644
--- a/src/Algebra/Lattice/Morphism/Structures.agda
+++ b/src/Algebra/Lattice/Morphism/Structures.agda
@@ -87,6 +87,7 @@ module LatticeMorphisms (L₁ : RawLattice a ℓ₁) (L₂ : RawLattice b ℓ₂
 
     open ∧.IsMagmaMonomorphism ∧-isMagmaMonomorphism public
       using (isRelMonomorphism)
+      renaming (⟦_⟧∙_ to ⟦_⟧∧_; _∙⟦_⟧ to _∧⟦_⟧)
 
 
   record IsLatticeIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
diff --git a/src/Algebra/Module/Morphism/Structures.agda b/src/Algebra/Module/Morphism/Structures.agda
index 3ef580ebea..70ef423664 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; ⟦_⟧∙_ to ⟦_⟧+ᴹ_; _∙⟦_⟧ to _+ᴹ⟦_⟧)
 
   record IsLeftSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
@@ -92,7 +92,7 @@ module LeftModuleMorphisms
       using (isRelHomomorphism; ⟦⟧-cong)
       renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism
                ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo
-               )
+               ; ⟦_⟧∙_ to ⟦_⟧+ᴹ_; _∙⟦_⟧ to _+ᴹ⟦_⟧)
 
     isLeftSemimoduleHomomorphism : IsLeftSemimoduleHomomorphism ⟦_⟧
     isLeftSemimoduleHomomorphism = record
@@ -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; ⟦_⟧∙_ to ⟦_⟧+ᴹ_; _∙⟦_⟧ to _+ᴹ⟦_⟧)
 
   record IsRightSemimoduleMonomorphism (⟦_⟧ : A → B) : Set (r ⊔ m₁ ⊔ ℓm₁ ⊔ ℓm₂) where
     field
@@ -219,7 +219,7 @@ module RightModuleMorphisms
       using (isRelHomomorphism; ⟦⟧-cong)
       renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism
                ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo
-               )
+               ; ⟦_⟧∙_ to ⟦_⟧+ᴹ_; _∙⟦_⟧ to _+ᴹ⟦_⟧)
     isRightSemimoduleHomomorphism : IsRightSemimoduleHomomorphism ⟦_⟧
     isRightSemimoduleHomomorphism = record
       { +ᴹ-isMonoidHomomorphism = +ᴹ-isMonoidHomomorphism
@@ -376,7 +376,7 @@ module BimoduleMorphisms
       using (isRelHomomorphism; ⟦⟧-cong)
       renaming ( isMagmaHomomorphism to +ᴹ-isMagmaHomomorphism; isMonoidHomomorphism to +ᴹ-isMonoidHomomorphism
                ; homo to +ᴹ-homo; ε-homo to 0ᴹ-homo; ⁻¹-homo to -ᴹ-homo
-               )
+               ; ⟦_⟧∙_ to ⟦_⟧+ᴹ_; _∙⟦_⟧ to _+ᴹ⟦_⟧)
 
     isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism ⟦_⟧
     isBisemimoduleHomomorphism = record
diff --git a/src/Algebra/Morphism/Bundles.agda b/src/Algebra/Morphism/Bundles.agda
index 5c6a8063ae..83ae947dc3 100644
--- a/src/Algebra/Morphism/Bundles.agda
+++ b/src/Algebra/Morphism/Bundles.agda
@@ -163,7 +163,8 @@ record KleeneAlgebraHomomorphism
   semiringHomomorphism = record { isSemiringHomomorphism = isSemiringHomomorphism }
 
   open SemiringHomomorphism semiringHomomorphism public
-    hiding (*-isMagmaHomomorphism; *-isMonoidHomomorphism)
+    hiding (*-isMagmaHomomorphism; *-isMonoidHomomorphism
+           ; ⟦_⟧+_; _+⟦_⟧; ⟦_⟧*_; _*⟦_⟧)
 
 ------------------------------------------------------------------------
 -- Morphisms between RingWithoutOnes
diff --git a/src/Algebra/Morphism/Structures.agda b/src/Algebra/Morphism/Structures.agda
index af7e025fff..e63aa1d9fe 100644
--- a/src/Algebra/Morphism/Structures.agda
+++ b/src/Algebra/Morphism/Structures.agda
@@ -89,6 +89,12 @@ module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) wher
     open IsRelHomomorphism isRelHomomorphism public
       renaming (cong to ⟦⟧-cong)
 
+    ⟦_⟧∙_ : A → B → B
+    ⟦ x ⟧∙ y = ⟦ x ⟧ ◦ y
+
+    _∙⟦_⟧ : B → A → B
+    y ∙⟦ x ⟧ = y ◦ ⟦ x ⟧
+
 
   record IsMagmaMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
@@ -261,7 +267,10 @@ module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSe
       *-homo : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_
 
     open +.IsMonoidHomomorphism +-isMonoidHomomorphism public
-      renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism)
+      renaming (homo to +-homo; ε-homo to 0#-homo
+               ; isMagmaHomomorphism to +-isMagmaHomomorphism
+               ; ⟦_⟧∙_ to ⟦_⟧+_; _∙⟦_⟧ to _+⟦_⟧
+               )
 
     *-isMagmaHomomorphism : *.IsMagmaHomomorphism ⟦_⟧
     *-isMagmaHomomorphism = record
@@ -269,6 +278,10 @@ module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSe
       ; homo = *-homo
       }
 
+    open *.IsMagmaHomomorphism *-isMagmaHomomorphism public
+      using ()
+      renaming (⟦_⟧∙_ to ⟦_⟧*_; _∙⟦_⟧ to _*⟦_⟧)
+
   record IsNearSemiringMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧
@@ -429,7 +442,11 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi
       *-homo : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_
 
     open +.IsGroupHomomorphism +-isGroupHomomorphism public
-      renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism; isMonoidHomomorphism to +-isMonoidHomomorphism)
+      renaming (homo to +-homo; ε-homo to 0#-homo
+               ; isMagmaHomomorphism to +-isMagmaHomomorphism
+               ; isMonoidHomomorphism to +-isMonoidHomomorphism
+               ; ⟦_⟧∙_ to ⟦_⟧+_; _∙⟦_⟧ to _+⟦_⟧
+               )
 
     isNearSemiringHomomorphism : +*.IsNearSemiringHomomorphism ⟦_⟧
     isNearSemiringHomomorphism = record
@@ -443,6 +460,10 @@ module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRi
       ; homo = *-homo
       }
 
+    open *.IsMagmaHomomorphism *-isMagmaHomomorphism public
+      using ()
+      renaming (⟦_⟧∙_ to ⟦_⟧*_; _∙⟦_⟧ to _*⟦_⟧)
+
   record IsRingWithoutOneMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
     field
       isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧