diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2959d3d6ce..fce644e3fd 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -51,6 +51,18 @@ Deprecated names
   *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc   ↦  *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc
   ```
 
+* In `Algebra.Modules.Structures.IsLeftModule`:
+  ```agda
+  uniqueˡ‿⁻ᴹ   ↦  Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ
+  uniqueʳ‿⁻ᴹ   ↦  Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ
+  ```
+
+* In `Algebra.Modules.Structures.IsRightModule`:
+  ```agda
+  uniqueˡ‿⁻ᴹ   ↦  Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ
+  uniqueʳ‿⁻ᴹ   ↦  Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ
+  ```
+
 * In `Algebra.Properties.Magma.Divisibility`:
   ```agda
   ∣∣-sym       ↦  ∥-sym
@@ -86,6 +98,12 @@ Deprecated names
   ∣-trans    ↦  ∣ʳ-trans
   ```
 
+* In `Algebra.Structures.Group`:
+  ```agda
+  uniqueˡ-⁻¹   ↦  Algebra.Properties.Group.inverseˡ-unique
+  uniqueʳ-⁻¹   ↦  Algebra.Properties.Group.inverseʳ-unique
+  ```
+
 * In `Data.List.Base`:
   ```agda
   and       ↦  Data.Bool.ListAction.and
@@ -113,6 +131,8 @@ Deprecated names
 New modules
 -----------
 
+* `Algebra.Module.Properties.{Bimodule|LeftModule|RightModule}`.
+
 * `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`.
 
 * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.
@@ -155,6 +175,12 @@ Additions to existing modules
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
 
+* In `Algebra.Modules.Properties`:
+  ```agda
+  inverseˡ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → x ≈ -ᴹ y
+  inverseʳ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → y ≈ -ᴹ x
+  ```
+
 * In `Algebra.Properties.Magma.Divisibility`:
   ```agda
   ∣ˡ-respʳ-≈  : _∣ˡ_ Respectsʳ _≈_
diff --git a/src/Algebra/Module/Bundles.agda b/src/Algebra/Module/Bundles.agda
index 6db104fe06..437a971ce5 100644
--- a/src/Algebra/Module/Bundles.agda
+++ b/src/Algebra/Module/Bundles.agda
@@ -39,7 +39,6 @@ open import Algebra.Module.Definitions
 open import Function.Base using (flip)
 open import Level using (Level; _⊔_; suc)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Nullary    using (¬_)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 private
diff --git a/src/Algebra/Module/Properties.agda b/src/Algebra/Module/Properties.agda
index 28f61b50bc..b9b529681f 100644
--- a/src/Algebra/Module/Properties.agda
+++ b/src/Algebra/Module/Properties.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra                using (CommutativeRing; Involutive)
+open import Algebra.Bundles        using (CommutativeRing)
 open import Algebra.Module.Bundles using (Module)
 open import Level                  using (Level)
 
@@ -18,7 +18,5 @@ module Algebra.Module.Properties
 
 open Module mod
 open import Algebra.Module.Properties.Semimodule semimodule public
-open import Algebra.Properties.Group using (⁻¹-involutive)
-
--ᴹ-involutive : Involutive _≈ᴹ_ -ᴹ_
--ᴹ-involutive = ⁻¹-involutive +ᴹ-group
+open import Algebra.Module.Properties.Bimodule bimodule public
+  using (inverseˡ-uniqueᴹ; inverseʳ-uniqueᴹ; -ᴹ-involutive)
diff --git a/src/Algebra/Module/Properties/Bimodule.agda b/src/Algebra/Module/Properties/Bimodule.agda
new file mode 100644
index 0000000000..539759c1b6
--- /dev/null
+++ b/src/Algebra/Module/Properties/Bimodule.agda
@@ -0,0 +1,21 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of bimodules.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles        using (Ring)
+open import Algebra.Module.Bundles using (Bimodule)
+open import Level                  using (Level)
+
+module Algebra.Module.Properties.Bimodule
+  {r ℓr s ℓs m ℓm : Level}
+  {ringR : Ring r ℓr} {ringS : Ring s ℓs}
+  (mod   : Bimodule ringR ringS m ℓm)
+  where
+
+open Bimodule mod
+open import Algebra.Module.Properties.LeftModule leftModule public
+  using (inverseˡ-uniqueᴹ; inverseʳ-uniqueᴹ; -ᴹ-involutive)
diff --git a/src/Algebra/Module/Properties/LeftModule.agda b/src/Algebra/Module/Properties/LeftModule.agda
new file mode 100644
index 0000000000..ad6d33cc67
--- /dev/null
+++ b/src/Algebra/Module/Properties/LeftModule.agda
@@ -0,0 +1,25 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of left modules.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles        using (Ring)
+open import Algebra.Module.Bundles using (LeftModule)
+open import Level                  using (Level)
+
+module Algebra.Module.Properties.LeftModule
+  {r ℓr m ℓm : Level}
+  {ring  : Ring r ℓr}
+  (mod   : LeftModule ring m ℓm)
+  where
+
+open Ring       ring
+open LeftModule mod
+open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public
+  using ()
+  renaming (inverseˡ-unique to inverseˡ-uniqueᴹ
+           ; inverseʳ-unique to inverseʳ-uniqueᴹ
+           ; ⁻¹-involutive to -ᴹ-involutive)
diff --git a/src/Algebra/Module/Properties/RightModule.agda b/src/Algebra/Module/Properties/RightModule.agda
new file mode 100644
index 0000000000..ef6b7c9f90
--- /dev/null
+++ b/src/Algebra/Module/Properties/RightModule.agda
@@ -0,0 +1,25 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of right modules.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles        using (Ring)
+open import Algebra.Module.Bundles using (RightModule)
+open import Level                  using (Level)
+
+module Algebra.Module.Properties.RightModule
+  {r ℓr m ℓm : Level}
+  {ring  : Ring r ℓr}
+  (mod   : RightModule ring m ℓm)
+  where
+
+open Ring        ring
+open RightModule mod
+open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public
+  using ()
+  renaming (inverseˡ-unique to inverseˡ-uniqueᴹ
+           ; inverseʳ-unique to inverseʳ-uniqueᴹ
+           ; ⁻¹-involutive to -ᴹ-involutive)
diff --git a/src/Algebra/Module/Properties/Semimodule.agda b/src/Algebra/Module/Properties/Semimodule.agda
index f6db3680b4..d7686b25ef 100644
--- a/src/Algebra/Module/Properties/Semimodule.agda
+++ b/src/Algebra/Module/Properties/Semimodule.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra                using (CommutativeSemiring)
+open import Algebra.Bundles        using (CommutativeSemiring)
 open import Algebra.Module.Bundles using (Semimodule)
 open import Level                  using (Level)
 
@@ -18,8 +18,8 @@ module Algebra.Module.Properties.Semimodule
 
 open CommutativeSemiring semiring
 open Semimodule          semimod
-open import Relation.Nullary.Negation using (contraposition)
 open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid
+open import Relation.Nullary.Negation using (contraposition)
 
 x≈0⇒x*y≈0 : ∀ {x y} → x ≈ 0# → x *ₗ y ≈ᴹ 0ᴹ
 x≈0⇒x*y≈0 {x} {y} x≈0 = begin
diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda
index a7cb6b0bc2..0084b33d90 100644
--- a/src/Algebra/Module/Structures.agda
+++ b/src/Algebra/Module/Structures.agda
@@ -6,10 +6,6 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Structures using (IsEquivalence)
-
 module Algebra.Module.Structures where
 
 open import Algebra.Bundles
@@ -23,6 +19,10 @@ open import Algebra.Module.Definitions
 open import Algebra.Structures using (IsCommutativeMonoid; IsAbelianGroup)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Level using (Level; _⊔_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
+
 
 private
   variable
@@ -216,6 +216,15 @@ module _ (ring : Ring r ℓr)
       ; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ
       ; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ
       )
+    {-# WARNING_ON_USAGE uniqueˡ‿-ᴹ
+    "Warning: uniqueˡ‿-ᴹ was deprecated in v2.3.
+    Please use Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ instead."
+    #-}
+    {-# WARNING_ON_USAGE uniqueʳ‿-ᴹ
+    "Warning: uniqueʳ‿-ᴹ was deprecated in v2.3.
+    Please use Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ instead."
+    #-}
+
 
   record IsRightModule (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
     open Defs ≈ᴹ
@@ -244,6 +253,15 @@ module _ (ring : Ring r ℓr)
       ; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ
       ; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ
       )
+    {-# WARNING_ON_USAGE uniqueˡ‿-ᴹ
+    "Warning: uniqueˡ‿-ᴹ was deprecated in v2.3.
+    Please use Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ instead."
+    #-}
+    {-# WARNING_ON_USAGE uniqueʳ‿-ᴹ
+    "Warning: uniqueʳ‿-ᴹ was deprecated in v2.3.
+    Please use Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ instead."
+    #-}
+
 
 module _ (R-ring : Ring r ℓr) (S-ring : Ring s ℓs)
          (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M)
diff --git a/src/Algebra/Morphism.agda b/src/Algebra/Morphism.agda
index e3bcb53e9b..555398fdde 100644
--- a/src/Algebra/Morphism.agda
+++ b/src/Algebra/Morphism.agda
@@ -10,7 +10,6 @@ module Algebra.Morphism where
 
 import Algebra.Morphism.Definitions as MorphismDefinitions
 open import Algebra
-import Algebra.Properties.Group as GroupP
 open import Function.Base
 open import Level
 open import Relation.Binary.Core using (Rel; _Preserves_⟶_)
diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index 1aae80d1cc..b15bad236f 100644
--- a/src/Algebra/Structures.agda
+++ b/src/Algebra/Structures.agda
@@ -323,10 +323,18 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) w
   uniqueˡ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → x ≈ (y ⁻¹)
   uniqueˡ-⁻¹ = Consequences.assoc∧id∧invʳ⇒invˡ-unique
                 setoid ∙-cong assoc identity inverseʳ
+  {-# WARNING_ON_USAGE uniqueˡ-⁻¹
+  "Warning: uniqueˡ-⁻¹ was deprecated in v2.3.
+  Please use Algebra.Properties.Group.inverseˡ-unique instead. "
+  #-}
 
   uniqueʳ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → y ≈ (x ⁻¹)
   uniqueʳ-⁻¹ = Consequences.assoc∧id∧invˡ⇒invʳ-unique
                 setoid ∙-cong assoc identity inverseˡ
+  {-# WARNING_ON_USAGE uniqueʳ-⁻¹
+  "Warning: uniqueʳ-⁻¹ was deprecated in v2.3.
+  Please use Algebra.Properties.Group.inverseʳ-unique instead. "
+  #-}
 
   isInvertibleMagma : IsInvertibleMagma _∙_ ε _⁻¹
   isInvertibleMagma = record