Rename+deprecate in Algebra.Properties.CommutativeMagma.Divisibility (

#2470)

* fix #2245

* correct typo in deprecation warning

* correct typo in deprecation warning

CHANGELOG.md

@@ -24,6 +24,12 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Algebra.Properties.CommutativeMagma.Divisibility`:
+  ```agda
+  ∣-factors    ↦  x|xy∧y|xy
+  ∣-factors-≈  ↦  xy≈z⇒x|z∧y|z
+  ```
+
 * In `Data.Vec.Properties`:
   ```agda
   ++-assoc _      ↦  ++-assoc-eqFree

src/Algebra/Properties/CommutativeMagma/Divisibility.agda

@@ -7,15 +7,14 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra using (CommutativeMagma)
-open import Data.Product.Base using (_×_; _,_; map)
 
 module Algebra.Properties.CommutativeMagma.Divisibility
   {a ℓ} (CM : CommutativeMagma a ℓ)
   where
 
-open CommutativeMagma CM
+open import Data.Product.Base using (_×_; _,_)
 
-open import Relation.Binary.Reasoning.Setoid setoid
+open CommutativeMagma CM using (magma; _≈_; _∙_; comm)
 
 ------------------------------------------------------------------------
 -- Re-export the contents of magmas
@@ -31,8 +30,28 @@ x∣xy x y = y , comm y x
 xy≈z⇒x∣z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z
 xy≈z⇒x∣z x y xy≈z = ∣-respʳ xy≈z (x∣xy x y)
 
-∣-factors : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y)
-∣-factors x y = x∣xy x y , x∣yx y x
+x|xy∧y|xy : ∀ x y → (x ∣ x ∙ y) × (y ∣ x ∙ y)
+x|xy∧y|xy x y = x∣xy x y , x∣yx y x
 
-∣-factors-≈ : ∀ x y {z} → x ∙ y ≈ z → x ∣ z × y ∣ z
-∣-factors-≈ x y xy≈z = xy≈z⇒x∣z x y xy≈z , xy≈z⇒y∣z x y xy≈z
+xy≈z⇒x|z∧y|z : ∀ x y {z} → x ∙ y ≈ z → x ∣ z × y ∣ z
+xy≈z⇒x|z∧y|z x y xy≈z = xy≈z⇒x∣z x y xy≈z , xy≈z⇒y∣z x y xy≈z
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.2
+
+∣-factors = x|xy∧y|xy
+{-# WARNING_ON_USAGE ∣-factors
+"Warning: ∣-factors was deprecated in v2.2.
+Please use x|xy∧y|xy instead. "
+#-}
+∣-factors-≈ = xy≈z⇒x|z∧y|z
+{-# WARNING_ON_USAGE ∣-factors-≈
+"Warning: ∣-factors-≈ was deprecated in v2.2.
+Please use xy≈z⇒x|z∧y|z instead. "
+#-}