From 2b3a0dabc8b3ea3024fb015916704dcd0d9c63b3 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Mon, 2 Jan 2023 23:02:48 +0100 Subject: [PATCH 01/10] Add commutative law to modules --- src/Algebra/Module/Structures.agda | 4 +++- src/Algebra/Module/Structures/Biased.agda | 12 ++++++++++-- 2 files changed, 13 insertions(+), 3 deletions(-) diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda index 20269f13a6..a78c2866d4 100644 --- a/src/Algebra/Module/Structures.agda +++ b/src/Algebra/Module/Structures.agda @@ -171,6 +171,7 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where field isBisemimodule : IsBisemimodule semiring semiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ + *ₗ-*ᵣ-comm : ∀ x m → ≈ᴹ (*ₗ x m) (*ᵣ m x) open IsBisemimodule isBisemimodule public @@ -285,8 +286,9 @@ module _ (commutativeRing : CommutativeRing r ℓr) record IsModule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where field isBimodule : IsBimodule ring ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ₗ *ᵣ + *ₗ-*ᵣ-comm : ∀ x m → ≈ᴹ (*ₗ x m) (*ᵣ m x) open IsBimodule isBimodule public isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ - isSemimodule = record { isBisemimodule = isBisemimodule } + isSemimodule = record { isBisemimodule = isBisemimodule; *ₗ-*ᵣ-comm = *ₗ-*ᵣ-comm } diff --git a/src/Algebra/Module/Structures/Biased.agda b/src/Algebra/Module/Structures/Biased.agda index 74d825e335..a9d7838053 100644 --- a/src/Algebra/Module/Structures/Biased.agda +++ b/src/Algebra/Module/Structures/Biased.agda @@ -55,7 +55,10 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr) where } isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ *ₗ (flip *ₗ) - isSemimodule = record { isBisemimodule = isBisemimodule } + isSemimodule = record + { isBisemimodule = isBisemimodule + ; *ₗ-*ᵣ-comm = λ _ _ → ≈ᴹ-refl + } -- Similarly, a right semimodule over a commutative semiring -- is already a semimodule. @@ -86,7 +89,10 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr) where } isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ (flip *ᵣ) *ᵣ - isSemimodule = record { isBisemimodule = isBisemimodule } + isSemimodule = record + { isBisemimodule = isBisemimodule + ; *ₗ-*ᵣ-comm = λ _ _ → ≈ᴹ-refl + } module _ (commutativeRing : CommutativeRing r ℓr) where @@ -111,6 +117,7 @@ module _ (commutativeRing : CommutativeRing r ℓr) where ; -ᴹ‿cong = -ᴹ‿cong ; -ᴹ‿inverse = -ᴹ‿inverse } + ; *ₗ-*ᵣ-comm = λ _ _ → ≈ᴹ-refl } -- Similarly, a right module over a commutative ring is already a module. @@ -132,4 +139,5 @@ module _ (commutativeRing : CommutativeRing r ℓr) where ; -ᴹ‿cong = -ᴹ‿cong ; -ᴹ‿inverse = -ᴹ‿inverse } + ; *ₗ-*ᵣ-comm = λ _ _ → ≈ᴹ-refl } From 40bd8810b1dd3a68cd0facd844dc10afa3359158 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Tue, 3 Jan 2023 00:06:24 +0100 Subject: [PATCH 02/10] Add new law to constructed modules --- src/Algebra/Module/Construct/DirectProduct.agda | 2 ++ src/Algebra/Module/Construct/TensorUnit.agda | 2 ++ 2 files changed, 4 insertions(+) diff --git a/src/Algebra/Module/Construct/DirectProduct.agda b/src/Algebra/Module/Construct/DirectProduct.agda index 3c168564bd..cacd615f9d 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) + ; *ₗ-*ᵣ-comm = λ x m → M.*ₗ-*ᵣ-comm x (proj₁ m) , N.*ₗ-*ᵣ-comm 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) + ; *ₗ-*ᵣ-comm = λ x m → M.*ₗ-*ᵣ-comm x (proj₁ m) , N.*ₗ-*ᵣ-comm 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..3f07b2f054 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 + ; *ₗ-*ᵣ-comm = λ x m → *-comm x m } } where open CommutativeSemiring commutativeSemiring @@ -113,5 +114,6 @@ bimodule {R = ring} = record ⟨module⟩ {R = commutativeRing} = record { isModule = record { isBimodule = Bimodule.isBimodule bimodule + ; *ₗ-*ᵣ-comm = λ x m → *-comm x m } } where open CommutativeRing commutativeRing From c88acba46f37e6356f035783da4c179237460d1e Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 5 May 2023 09:31:50 +0200 Subject: [PATCH 03/10] Add new definitions file for new law --- src/Algebra/Module/Definitions.agda | 2 ++ .../Module/Definitions/Bi/Simultaneous.agda | 18 ++++++++++++++++++ src/Algebra/Module/Structures.agda | 4 +++- 3 files changed, 23 insertions(+), 1 deletion(-) create mode 100644 src/Algebra/Module/Definitions/Bi/Simultaneous.agda diff --git a/src/Algebra/Module/Definitions.agda b/src/Algebra/Module/Definitions.agda index cb02f94469..02af560ae8 100644 --- a/src/Algebra/Module/Definitions.agda +++ b/src/Algebra/Module/Definitions.agda @@ -14,7 +14,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..224907e305 --- /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 + +Commutative : Opₗ A B → Opᵣ A B → Set _ +Commutative _∙ₗ_ _∙ᵣ_ = ∀ x m → (x ∙ₗ m) ≈ (m ∙ᵣ x) diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda index a78c2866d4..2f664fa4e9 100644 --- a/src/Algebra/Module/Structures.agda +++ b/src/Algebra/Module/Structures.agda @@ -283,10 +283,12 @@ module _ (commutativeRing : CommutativeRing r ℓr) -- This means 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ᴹ -ᴹ *ₗ *ᵣ - *ₗ-*ᵣ-comm : ∀ x m → ≈ᴹ (*ₗ x m) (*ᵣ m x) + *ₗ-*ᵣ-comm : Commutative *ₗ *ᵣ open IsBimodule isBimodule public From bff83acc624d7df749a4a9418450dd53dbd0d365 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 5 May 2023 09:32:59 +0200 Subject: [PATCH 04/10] Fix comment --- src/Algebra/Module/Structures.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda index 2f664fa4e9..cd1b9ef540 100644 --- a/src/Algebra/Module/Structures.agda +++ b/src/Algebra/Module/Structures.agda @@ -280,7 +280,7 @@ 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 + -- 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 ≈ᴹ From 1b2b764a68e23ee6fac78997ab4d09eef3dc64dd Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Fri, 5 May 2023 09:35:42 +0200 Subject: [PATCH 05/10] Update changelog --- CHANGELOG.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2abb4c3c57..b78326bfa1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -782,6 +782,10 @@ Non-backwards compatible changes lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x) ``` +* `IsModule` now contains an extra law to enforce that left- and right- multiplication coincide: + ``` + *ₗ-*ᵣ-comm : Commutative *ₗ *ᵣ + ``` Major improvements ------------------ @@ -1347,6 +1351,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 From 97bb4a7606436657ab5816707cfd1f5fe36a8192 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 10 May 2023 13:44:54 +0200 Subject: [PATCH 06/10] Update semimodule comments --- CHANGELOG.md | 2 +- src/Algebra/Module/Structures.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b78326bfa1..398ab7a576 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -782,7 +782,7 @@ Non-backwards compatible changes lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x) ``` -* `IsModule` now contains an extra law to enforce that left- and right- multiplication coincide: +* `IsSemimodule` and `IsModule` now contain an extra law to enforce that left- and right- multiplication coincide: ``` *ₗ-*ᵣ-comm : Commutative *ₗ *ᵣ ``` diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda index cd1b9ef540..7fcdbbb6c5 100644 --- a/src/Algebra/Module/Structures.agda +++ b/src/Algebra/Module/Structures.agda @@ -164,7 +164,7 @@ 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 + -- We enforce that *ₗ and *ᵣ coincide up to mathematical equality, though it -- may be that they do not coincide up to definitional equality. record IsSemimodule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ R M) From abcb04d8a2f0037d561dfd1dc4d1a76cf9085685 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 10 May 2023 13:46:53 +0200 Subject: [PATCH 07/10] Use definition for semimodules --- src/Algebra/Module/Structures.agda | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda index 7fcdbbb6c5..1c15a5055b 100644 --- a/src/Algebra/Module/Structures.agda +++ b/src/Algebra/Module/Structures.agda @@ -167,11 +167,13 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr) -- 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ᴹ *ₗ *ᵣ - *ₗ-*ᵣ-comm : ∀ x m → ≈ᴹ (*ₗ x m) (*ᵣ m x) + *ₗ-*ᵣ-comm : Commutative *ₗ *ᵣ open IsBisemimodule isBisemimodule public From 4c13919e59aafde2f2204957c13d2052e8451094 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Wed, 10 May 2023 13:50:13 +0200 Subject: [PATCH 08/10] Refer to issue in changelog --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 398ab7a576..21bd9a2ef0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -782,7 +782,7 @@ Non-backwards compatible changes lookupₛ : P Respects _≈_ → All P xs → (∀ {x} → x ∈ xs → P x) ``` -* `IsSemimodule` and `IsModule` now contain an extra law to enforce that left- and right- multiplication coincide: +* `IsSemimodule` and `IsModule` now contain an extra law to enforce that left- and right- multiplication coincide (issue #1888): ``` *ₗ-*ᵣ-comm : Commutative *ₗ *ᵣ ``` From 9568963577415554e52dd2de7b9435acfae2dbd9 Mon Sep 17 00:00:00 2001 From: Nathan van Doorn Date: Thu, 12 Oct 2023 19:51:39 +0200 Subject: [PATCH 09/10] commutative -> coincident --- src/Algebra/Module/Construct/DirectProduct.agda | 4 ++-- src/Algebra/Module/Construct/TensorUnit.agda | 4 ++-- src/Algebra/Module/Definitions/Bi/Simultaneous.agda | 4 ++-- src/Algebra/Module/Structures.agda | 6 +++--- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/Algebra/Module/Construct/DirectProduct.agda b/src/Algebra/Module/Construct/DirectProduct.agda index 7ed8a9f713..429a2d11ca 100644 --- a/src/Algebra/Module/Construct/DirectProduct.agda +++ b/src/Algebra/Module/Construct/DirectProduct.agda @@ -97,7 +97,7 @@ semimodule M N = record { isSemimodule = record { isBisemimodule = Bisemimodule.isBisemimodule (bisemimodule M.bisemimodule N.bisemimodule) - ; *ₗ-*ᵣ-comm = λ x m → M.*ₗ-*ᵣ-comm x (proj₁ m) , N.*ₗ-*ᵣ-comm x (proj₂ m) + ; *ₗ-*ᵣ-coincident = λ x m → M.*ₗ-*ᵣ-coincident x (proj₁ m) , N.*ₗ-*ᵣ-coincident x (proj₂ m) } } where module M = Semimodule M; module N = Semimodule N @@ -156,6 +156,6 @@ bimodule M N = record ⟨module⟩ M N = record { isModule = record { isBimodule = Bimodule.isBimodule (bimodule M.bimodule N.bimodule) - ; *ₗ-*ᵣ-comm = λ x m → M.*ₗ-*ᵣ-comm x (proj₁ m) , N.*ₗ-*ᵣ-comm x (proj₂ m) + ; *ₗ-*ᵣ-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 3f07b2f054..c76f2a39ba 100644 --- a/src/Algebra/Module/Construct/TensorUnit.agda +++ b/src/Algebra/Module/Construct/TensorUnit.agda @@ -77,7 +77,7 @@ semimodule : {R : CommutativeSemiring c ℓ} → Semimodule R c ℓ semimodule {R = commutativeSemiring} = record { isSemimodule = record { isBisemimodule = Bisemimodule.isBisemimodule bisemimodule - ; *ₗ-*ᵣ-comm = λ x m → *-comm x m + ; *ₗ-*ᵣ-coincident = *-comm } } where open CommutativeSemiring commutativeSemiring @@ -114,6 +114,6 @@ bimodule {R = ring} = record ⟨module⟩ {R = commutativeRing} = record { isModule = record { isBimodule = Bimodule.isBimodule bimodule - ; *ₗ-*ᵣ-comm = λ x m → *-comm x m + ; *ₗ-*ᵣ-coincident = *-comm } } where open CommutativeRing commutativeRing diff --git a/src/Algebra/Module/Definitions/Bi/Simultaneous.agda b/src/Algebra/Module/Definitions/Bi/Simultaneous.agda index 224907e305..686f4ff06c 100644 --- a/src/Algebra/Module/Definitions/Bi/Simultaneous.agda +++ b/src/Algebra/Module/Definitions/Bi/Simultaneous.agda @@ -14,5 +14,5 @@ module Algebra.Module.Definitions.Bi.Simultaneous open import Algebra.Module.Core -Commutative : Opₗ A B → Opᵣ A B → Set _ -Commutative _∙ₗ_ _∙ᵣ_ = ∀ x m → (x ∙ₗ m) ≈ (m ∙ᵣ x) +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 88cb6db28e..64873252bd 100644 --- a/src/Algebra/Module/Structures.agda +++ b/src/Algebra/Module/Structures.agda @@ -175,7 +175,7 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where field isBisemimodule : IsBisemimodule semiring semiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ - *ₗ-*ᵣ-comm : Commutative *ₗ *ᵣ + *ₗ-*ᵣ-coincident : Coincident *ₗ *ᵣ open IsBisemimodule isBisemimodule public @@ -292,9 +292,9 @@ module _ (commutativeRing : CommutativeRing r ℓr) record IsModule (*ₗ : Opₗ R M) (*ᵣ : Opᵣ R M) : Set (r ⊔ m ⊔ ℓr ⊔ ℓm) where field isBimodule : IsBimodule ring ring ≈ᴹ +ᴹ 0ᴹ -ᴹ *ₗ *ᵣ - *ₗ-*ᵣ-comm : Commutative *ₗ *ᵣ + *ₗ-*ᵣ-coincident : Coincident *ₗ *ᵣ open IsBimodule isBimodule public isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ *ₗ *ᵣ - isSemimodule = record { isBisemimodule = isBisemimodule; *ₗ-*ᵣ-comm = *ₗ-*ᵣ-comm } + isSemimodule = record { isBisemimodule = isBisemimodule; *ₗ-*ᵣ-coincident = *ₗ-*ᵣ-coincident } From 5e6ec63c71032c7af82097c64946f200aa064de1 Mon Sep 17 00:00:00 2001 From: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com> Date: Fri, 13 Oct 2023 14:01:02 +0100 Subject: [PATCH 10/10] Update Biased.agda: fixed `comm` to `coincident` knock-on errors --- src/Algebra/Module/Structures/Biased.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Algebra/Module/Structures/Biased.agda b/src/Algebra/Module/Structures/Biased.agda index cfd62355d9..764745c54c 100644 --- a/src/Algebra/Module/Structures/Biased.agda +++ b/src/Algebra/Module/Structures/Biased.agda @@ -59,7 +59,7 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr) where isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ *ₗ (flip *ₗ) isSemimodule = record { isBisemimodule = isBisemimodule - ; *ₗ-*ᵣ-comm = λ _ _ → ≈ᴹ-refl + ; *ₗ-*ᵣ-coincident = λ _ _ → ≈ᴹ-refl } -- Similarly, a right semimodule over a commutative semiring @@ -93,7 +93,7 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr) where isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ (flip *ᵣ) *ᵣ isSemimodule = record { isBisemimodule = isBisemimodule - ; *ₗ-*ᵣ-comm = λ _ _ → ≈ᴹ-refl + ; *ₗ-*ᵣ-coincident = λ _ _ → ≈ᴹ-refl } @@ -119,7 +119,7 @@ module _ (commutativeRing : CommutativeRing r ℓr) where ; -ᴹ‿cong = -ᴹ‿cong ; -ᴹ‿inverse = -ᴹ‿inverse } - ; *ₗ-*ᵣ-comm = λ _ _ → ≈ᴹ-refl + ; *ₗ-*ᵣ-coincident = λ _ _ → ≈ᴹ-refl } -- Similarly, a right module over a commutative ring is already a module. @@ -141,5 +141,5 @@ module _ (commutativeRing : CommutativeRing r ℓr) where ; -ᴹ‿cong = -ᴹ‿cong ; -ᴹ‿inverse = -ᴹ‿inverse } - ; *ₗ-*ᵣ-comm = λ _ _ → ≈ᴹ-refl + ; *ₗ-*ᵣ-coincident = λ _ _ → ≈ᴹ-refl }