diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3d99a6eb2b..fda618a8c0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1782,6 +1782,11 @@ New modules
   Algebra.Module.Core
   ```
 
+* Definitions for module-like algebraic structures with left- and right- multiplication over the same scalars:
+  ```
+  Algebra.Module.Definitions.Bi.Simultaneous
+  ```
+
 * Constructive algebraic structures with apartness relations:
   ```
   Algebra.Apartness
diff --git a/src/Algebra/Module/Construct/DirectProduct.agda b/src/Algebra/Module/Construct/DirectProduct.agda
index 840cc42cab..429a2d11ca 100644
--- a/src/Algebra/Module/Construct/DirectProduct.agda
+++ b/src/Algebra/Module/Construct/DirectProduct.agda
@@ -97,6 +97,7 @@ semimodule M N = record
   { isSemimodule = record
     { isBisemimodule = Bisemimodule.isBisemimodule
       (bisemimodule M.bisemimodule N.bisemimodule)
+    ; *ₗ-*ᵣ-coincident = λ x m → M.*ₗ-*ᵣ-coincident x (proj₁ m) , N.*ₗ-*ᵣ-coincident x (proj₂ m)
     }
   } where module M = Semimodule M; module N = Semimodule N
 
@@ -155,5 +156,6 @@ bimodule M N = record
 ⟨module⟩ M N = record
   { isModule = record
     { isBimodule = Bimodule.isBimodule (bimodule M.bimodule N.bimodule)
+    ; *ₗ-*ᵣ-coincident = λ x m → M.*ₗ-*ᵣ-coincident x (proj₁ m) , N.*ₗ-*ᵣ-coincident x (proj₂ m)
     }
   } where module M = Module M; module N = Module N
diff --git a/src/Algebra/Module/Construct/TensorUnit.agda b/src/Algebra/Module/Construct/TensorUnit.agda
index 6277210520..c76f2a39ba 100644
--- a/src/Algebra/Module/Construct/TensorUnit.agda
+++ b/src/Algebra/Module/Construct/TensorUnit.agda
@@ -77,6 +77,7 @@ semimodule : {R : CommutativeSemiring c ℓ} → Semimodule R c ℓ
 semimodule {R = commutativeSemiring} = record
   { isSemimodule = record
     { isBisemimodule = Bisemimodule.isBisemimodule bisemimodule
+    ; *ₗ-*ᵣ-coincident = *-comm
     }
   } where open CommutativeSemiring commutativeSemiring
 
@@ -113,5 +114,6 @@ bimodule {R = ring} = record
 ⟨module⟩ {R = commutativeRing} = record
   { isModule = record
     { isBimodule = Bimodule.isBimodule bimodule
+    ; *ₗ-*ᵣ-coincident = *-comm
     }
   } where open CommutativeRing commutativeRing
diff --git a/src/Algebra/Module/Definitions.agda b/src/Algebra/Module/Definitions.agda
index 19c1abdb46..949aa45119 100644
--- a/src/Algebra/Module/Definitions.agda
+++ b/src/Algebra/Module/Definitions.agda
@@ -12,7 +12,9 @@ module Algebra.Module.Definitions where
   import Algebra.Module.Definitions.Left as L
   import Algebra.Module.Definitions.Right as R
   import Algebra.Module.Definitions.Bi as B
+  import Algebra.Module.Definitions.Bi.Simultaneous as BS
 
   module LeftDefs = L
   module RightDefs = R
   module BiDefs = B
+  module SimultaneousBiDefs = BS
diff --git a/src/Algebra/Module/Definitions/Bi/Simultaneous.agda b/src/Algebra/Module/Definitions/Bi/Simultaneous.agda
new file mode 100644
index 0000000000..686f4ff06c
--- /dev/null
+++ b/src/Algebra/Module/Definitions/Bi/Simultaneous.agda
@@ -0,0 +1,18 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties connecting left-scaling and right-scaling over the same scalars
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary
+
+module Algebra.Module.Definitions.Bi.Simultaneous
+  {a b ℓb} (A : Set a) {B : Set b} (_≈_ : Rel B ℓb)
+  where
+
+open import Algebra.Module.Core
+
+Coincident : Opₗ A B → Opᵣ A B → Set _
+Coincident _∙ₗ_ _∙ᵣ_ = ∀ x m → (x ∙ₗ m) ≈ (m ∙ᵣ x)
diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda
index d8a291bd13..64873252bd 100644
--- a/src/Algebra/Module/Structures.agda
+++ b/src/Algebra/Module/Structures.agda
@@ -166,14 +166,16 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr)
   open CommutativeSemiring commutativeSemiring renaming (Carrier to R)
 
   -- An R-semimodule is an R-R-bisemimodule where R is commutative.
-  -- This means that *ₗ and *ᵣ coincide up to mathematical equality,
-  -- though it may be that they do not coincide up to definitional
-  -- equality.
+  -- We enforce that *ₗ and *ᵣ coincide up to mathematical equality, though it
+  -- may be that they do not coincide up to definitional equality.
+
+  open SimultaneousBiDefs R ≈ᴹ
 
   record IsSemimodule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ R M)
                       : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
     field
       isBisemimodule : IsBisemimodule semiring semiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ
+      *ₗ-*ᵣ-coincident : Coincident *ₗ *ᵣ
 
     open IsBisemimodule isBisemimodule public
 
@@ -282,15 +284,17 @@ module _ (commutativeRing : CommutativeRing r ℓr)
   open CommutativeRing commutativeRing renaming (Carrier to R)
 
   -- An R-module is an R-R-bimodule where R is commutative.
-  -- This means that *ₗ and *ᵣ coincide up to mathematical equality,
-  -- though it may be that they do not coincide up to definitional
-  -- equality.
+  -- We enforce that *ₗ and *ᵣ coincide up to mathematical equality, though it
+  -- may be that they do not coincide up to definitional equality.
+
+  open SimultaneousBiDefs R ≈ᴹ
 
   record IsModule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
     field
       isBimodule : IsBimodule ring ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ₗ *ᵣ
+      *ₗ-*ᵣ-coincident : Coincident *ₗ *ᵣ
 
     open IsBimodule isBimodule public
 
     isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ
-    isSemimodule = record { isBisemimodule = isBisemimodule }
+    isSemimodule = record { isBisemimodule = isBisemimodule; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident }
diff --git a/src/Algebra/Module/Structures/Biased.agda b/src/Algebra/Module/Structures/Biased.agda
index 99e48695ae..764745c54c 100644
--- a/src/Algebra/Module/Structures/Biased.agda
+++ b/src/Algebra/Module/Structures/Biased.agda
@@ -57,7 +57,10 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr) where
       }
 
     isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ *ₗ (flip *ₗ)
-    isSemimodule = record { isBisemimodule = isBisemimodule }
+    isSemimodule = record
+      { isBisemimodule = isBisemimodule
+      ; *ₗ-*ᵣ-coincident = λ _ _ → ≈ᴹ-refl
+      }
 
   -- Similarly, a right semimodule over a commutative semiring
   -- is already a semimodule.
@@ -88,7 +91,10 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr) where
       }
 
     isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ (flip *ᵣ) *ᵣ
-    isSemimodule = record { isBisemimodule = isBisemimodule }
+    isSemimodule = record
+      { isBisemimodule = isBisemimodule
+      ; *ₗ-*ᵣ-coincident = λ _ _ → ≈ᴹ-refl
+      }
 
 
 module _ (commutativeRing : CommutativeRing r ℓr) where
@@ -113,6 +119,7 @@ module _ (commutativeRing : CommutativeRing r ℓr) where
         ; -ᴹ‿cong = -ᴹ‿cong
         ; -ᴹ‿inverse = -ᴹ‿inverse
         }
+      ; *ₗ-*ᵣ-coincident = λ _ _ → ≈ᴹ-refl
       }
 
   -- Similarly, a right module over a commutative ring is already a module.
@@ -134,4 +141,5 @@ module _ (commutativeRing : CommutativeRing r ℓr) where
         ; -ᴹ‿cong = -ᴹ‿cong
         ; -ᴹ‿inverse = -ᴹ‿inverse
         }
+      ; *ₗ-*ᵣ-coincident = λ _ _ → ≈ᴹ-refl
       }