[ DRY ] redefine Algebra.Definitions.Medial in terms of Interchangable

CHANGELOG.md

@@ -21,6 +21,11 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Algebra.Properties.CommutativeSemigroup`:
+  ```agda
+  interchange  ↦   medial
+  ```
+
 New modules
 -----------
 

src/Algebra/Definitions.agda

@@ -212,7 +212,7 @@ Flexible : Op₂ A → Set _
 Flexible _∙_ = ∀ x y → ((x ∙ y) ∙ x) ≈ (x ∙ (y ∙ x))
 
 Medial : Op₂ A → Set _
-Medial _∙_ = ∀ x y u z → ((x ∙ y) ∙ (u ∙ z)) ≈ ((x ∙ u) ∙ (y ∙ z))
+Medial _∙_ = Interchangable _∙_ _∙_
 
 LeftSemimedial : Op₂ A → Set _
 LeftSemimedial _∙_ = ∀ x y z → ((x ∙ x) ∙ (y ∙ z)) ≈ ((x ∙ y) ∙ (x ∙ z))

src/Algebra/Properties/CommutativeSemigroup.agda

@@ -9,10 +9,10 @@
 open import Algebra.Bundles using (CommutativeSemigroup)
 
 module Algebra.Properties.CommutativeSemigroup
-  {a ℓ} (CS : CommutativeSemigroup a ℓ)
+  {a ℓ} (commutativeSemigroup : CommutativeSemigroup a ℓ)
   where
 
-open CommutativeSemigroup CS
+open CommutativeSemigroup commutativeSemigroup
 open import Algebra.Definitions _≈_
 open import Relation.Binary.Reasoning.Setoid setoid
 open import Data.Product.Base using (_,_)
@@ -25,8 +25,8 @@ open import Algebra.Properties.Semigroup semigroup public
 ------------------------------------------------------------------------
 -- Properties
 
-interchange : Interchangable _∙_ _∙_
-interchange a b c d = begin
+medial : Medial _∙_
+medial a b c d = begin
   (a ∙ b) ∙ (c ∙ d)  ≈⟨  assoc a b (c ∙ d) ⟩
   a ∙ (b ∙ (c ∙ d))  ≈⟨ ∙-congˡ (assoc b c d) ⟨
   a ∙ ((b ∙ c) ∙ d)  ≈⟨  ∙-congˡ (∙-congʳ (comm b c)) ⟩
@@ -171,3 +171,18 @@ middleSemimedial x y z = begin
 
 semimedial : Semimedial _∙_
 semimedial = semimedialˡ , semimedialʳ
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.3
+
+interchange = medial
+{-# WARNING_ON_USAGE interchange
+"Warning: interchange was deprecated in v2.3.
+Please use medial instead."
+#-}

src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda

@@ -7,17 +7,17 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra using (CommutativeSemigroup)
-open import Data.Product.Base using (_,_)
-import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 module Algebra.Properties.CommutativeSemigroup.Divisibility
-  {a ℓ} (CS : CommutativeSemigroup a ℓ)
+  {a ℓ} (commutativeSemigroup : CommutativeSemigroup a ℓ)
   where
 
-open CommutativeSemigroup CS
-open import Algebra.Properties.CommutativeSemigroup CS
-  using (interchange; x∙yz≈xz∙y; x∙yz≈y∙xz)
-open ≈-Reasoning setoid
+open import Data.Product.Base using (_,_)
+
+open CommutativeSemigroup commutativeSemigroup
+open import Algebra.Properties.CommutativeSemigroup commutativeSemigroup
+  using (medial; x∙yz≈xz∙y; x∙yz≈y∙xz)
+open import Relation.Binary.Reasoning.Setoid setoid
 
 ------------------------------------------------------------------------
 -- Re-export the contents of divisibility over semigroups
@@ -42,7 +42,7 @@ x∣y∧z∣x/y⇒xz∣y {x} {y} {z} (x/y , x/y∙x≈y) (p , pz≈x/y) = p , (b
 
 ∙-cong-∣ : ∀ {x y a b} → x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
 ∙-cong-∣ {x} {y} {a} {b} (p , px≈y) (q , qa≈b) = p ∙ q , (begin
-  (p ∙ q) ∙ (x ∙ a) ≈⟨ interchange p q x a ⟩
+  (p ∙ q) ∙ (x ∙ a) ≈⟨ medial p q x a ⟩
   (p ∙ x) ∙ (q ∙ a) ≈⟨ ∙-cong px≈y qa≈b ⟩
   y ∙ b ∎)
 

src/Algebra/Properties/IdempotentCommutativeMonoid.agda

@@ -9,16 +9,16 @@
 open import Algebra.Bundles using (IdempotentCommutativeMonoid)
 
 module Algebra.Properties.IdempotentCommutativeMonoid
-  {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where
+  {c ℓ} (idempotentCommutativeMonoid : IdempotentCommutativeMonoid c ℓ) where
 
-open IdempotentCommutativeMonoid M
+open IdempotentCommutativeMonoid idempotentCommutativeMonoid
 
 open import Algebra.Consequences.Setoid setoid
   using (comm∧distrˡ⇒distrʳ; comm∧distrˡ⇒distr)
 open import Algebra.Definitions _≈_
   using (_DistributesOverˡ_; _DistributesOverʳ_; _DistributesOver_)
 open import Algebra.Properties.CommutativeSemigroup commutativeSemigroup
-  using (interchange)
+  using (medial)
 open import Relation.Binary.Reasoning.Setoid setoid
 
 
@@ -28,7 +28,7 @@ open import Relation.Binary.Reasoning.Setoid setoid
 ∙-distrˡ-∙ : _∙_ DistributesOverˡ _∙_
 ∙-distrˡ-∙ a b c = begin
     a ∙ (b ∙ c)        ≈⟨ ∙-congʳ (idem a) ⟨
-    (a ∙ a) ∙ (b ∙ c)  ≈⟨ interchange _ _ _ _ ⟩
+    (a ∙ a) ∙ (b ∙ c)  ≈⟨ medial _ _ _ _ ⟩
     (a ∙ b) ∙ (a ∙ c)  ∎
 
 ∙-distrʳ-∙ : _∙_ DistributesOverʳ _∙_

src/Algebra/Solver/CommutativeMonoid/Normal.agda

@@ -13,7 +13,7 @@ open import Algebra.Bundles using (CommutativeMonoid)
 module Algebra.Solver.CommutativeMonoid.Normal {c ℓ} (M : CommutativeMonoid c ℓ) where
 
 import Algebra.Properties.CommutativeSemigroup as CSProperties
-  using (interchange)
+  using (medial)
 import Algebra.Properties.Monoid.Mult as MultProperties
   using (_×_; ×-homo-1; ×-homo-+)
 open import Data.Fin.Base using (Fin; zero; suc)
@@ -27,7 +27,7 @@ import Relation.Nullary.Decidable as Dec using (map)
 
 open CommutativeMonoid M
 open MultProperties monoid using (_×_; ×-homo-1; ×-homo-+)
-open CSProperties commutativeSemigroup using (interchange)
+open CSProperties commutativeSemigroup using (medial)
 open ≈-Reasoning setoid
 
 private
@@ -117,7 +117,7 @@ comp-correct [] [] _ =  sym (identityˡ _)
 comp-correct (l ∷ v) (m ∷ w) (a ∷ ρ) = begin
   ((l + m) × a) ∙ ⟦ v • w ⟧⇓ ρ              ≈⟨ ∙-congʳ  (×-homo-+ a l m) ⟩
   (l × a) ∙ (m × a) ∙ ⟦ v • w ⟧⇓ ρ          ≈⟨ ∙-congˡ  (comp-correct v w ρ) ⟩
-  (l × a) ∙ (m × a) ∙ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) ≈⟨ interchange _ _ _ _ ⟩
+  (l × a) ∙ (m × a) ∙ (⟦ v ⟧⇓ ρ ∙ ⟦ w ⟧⇓ ρ) ≈⟨ medial _ _ _ _ ⟩
   ⟦ l ∷ v ⟧⇓ (a ∷ ρ) ∙ ⟦ m ∷ w ⟧⇓ (a ∷ ρ)   ∎
 
 ------------------------------------------------------------------------