[ refactor ] deprecate Algebra.Structures.IsGroup.{uniqueˡ-⁻¹|uniqueʳ-⁻¹} with knock-ons for Algebra.Module.*

CHANGELOG.md

@@ -72,6 +72,12 @@ Deprecated names
   ∣∣-trans   ↦  ∥-trans
   ```
 
+* In `Algebra.Structures`:
+  ```agda
+  uniqueˡ-⁻¹   ↦  Algebra.Properties.Group.inverseˡ-unique
+  uniqueʳ-⁻¹   ↦  Algebra.Properties.Group.inverseʳ-unique
+  ```
+
 * In `Data.List.Base`:
   ```agda
   and       ↦  Data.Bool.ListAction.and

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

src/Algebra/Module/Structures.agda

@@ -20,6 +20,7 @@ import Algebra.Definitions as Defs
 open import Algebra.Module.Definitions
   using (module LeftDefs; module RightDefs; module BiDefs;
   module SimultaneousBiDefs)
+import Algebra.Properties.AbelianGroup as AbelianGroupProperties
 open import Algebra.Structures using (IsCommutativeMonoid; IsAbelianGroup)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Level using (Level; _⊔_)
@@ -213,10 +214,12 @@ module _ (ring : Ring r ℓr)
       ( isGroup    to +ᴹ-isGroup
       ; inverseˡ   to -ᴹ‿inverseˡ
       ; inverseʳ   to -ᴹ‿inverseʳ
-      ; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ
-      ; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ
       )
 
+    open AbelianGroupProperties record { isAbelianGroup = +ᴹ-isAbelianGroup } public
+      using () renaming (inverseˡ-unique to uniqueˡ‿-ᴹ; inverseʳ-unique to uniqueʳ‿-ᴹ)
+
+
   record IsRightModule (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where
     open Defs ≈ᴹ
     field
@@ -241,10 +244,12 @@ module _ (ring : Ring r ℓr)
       ( isGroup    to +ᴹ-isGroup
       ; inverseˡ   to -ᴹ‿inverseˡ
       ; inverseʳ   to -ᴹ‿inverseʳ
-      ; uniqueˡ-⁻¹ to uniqueˡ‿-ᴹ
-      ; uniqueʳ-⁻¹ to uniqueʳ‿-ᴹ
       )
 
+    open AbelianGroupProperties record { isAbelianGroup = +ᴹ-isAbelianGroup } public
+      using () renaming (inverseˡ-unique to uniqueˡ‿-ᴹ; inverseʳ-unique to uniqueʳ‿-ᴹ)
+
+
 module _ (R-ring : Ring r ℓr) (S-ring : Ring s ℓs)
          (≈ᴹ : Rel {m} M ℓm) (+ᴹ : Op₂ M) (0ᴹ : M) (-ᴹ : Op₁ M)
   where

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_⟶_)

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