[ refactor ] rename ∣∣ to ∥, ∤∤ to ∦ throughout `Algebra.Defi…

…nitions.RawMagma` and `Algebra.Properties.*.Divisibility` (#2562)

* refactor: rename `∣∣` to `∥`, `∤∤` to `∦` throughout

* doc: added note to `style-guide`

CHANGELOG.md

@@ -21,6 +21,36 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Algebra.Definitions.RawMagma`:
+  ```agda
+  _∣∣_   ↦  _∥_
+  _∤∤_    ↦  _∦_
+  ```
+
+* In `Algebra.Properties.Magma.Divisibility`:
+  ```agda
+  ∣∣-sym       ↦  ∥-sym
+  ∣∣-respˡ-≈   ↦  ∥-respˡ-≈
+  ∣∣-respʳ-≈   ↦  ∥-respʳ-≈
+  ∣∣-resp-≈    ↦  ∥-resp-≈
+  ∤∤-sym  -≈    ↦  ∦-sym
+  ∤∤-respˡ-≈    ↦  ∦-respˡ-≈
+  ∤∤-respʳ-≈    ↦  ∦-respʳ-≈
+  ∤∤-resp-≈     ↦  ∦-resp-≈
+  ```
+
+* In `Algebra.Properties.Monoid.Divisibility`:
+  ```agda
+  ∣∣-refl            ↦  ∥-refl
+  ∣∣-reflexive       ↦  ∥-reflexive
+  ∣∣-isEquivalence   ↦  ∥-isEquivalence
+  ```
+
+* In `Algebra.Properties.Semigroup.Divisibility`:
+  ```agda
+  ∣∣-trans   ↦  ∥-trans
+  ```
+
 New modules
 -----------
 

doc/style-guide.md

@@ -571,8 +571,9 @@ word within a compound word is capitalized except for the first word.
 
 * Likewise, standard infix symbols for eg, divisibility on numeric
   datatypes/algebraic structure, should be written `\|`, NOT the
-  unmarked `|` character. An exception to this is the *strict*
-  ordering relation, written using `<`, NOT `\<` as might be expected.
+  unmarked `|` character. Ditto. mutual divisibility `\||` etc. An
+  exception to this is the *strict* ordering relation, written using
+  `<`, NOT `\<` as might be expected.
 
 * Since v2.0, the `Algebra` hierarchy systematically introduces
   consistent symbolic notation for the negated versions of the usual

src/Algebra/Definitions/RawMagma.agda

@@ -11,7 +11,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles.Raw using (RawMagma)
-open import Data.Product.Base using (_×_; ∃)
+open import Data.Product.Base using (_×_)
 open import Level using (_⊔_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary.Negation.Core using (¬_)
@@ -25,7 +25,7 @@ open RawMagma M renaming (Carrier to A)
 ------------------------------------------------------------------------
 -- Divisibility
 
-infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_ _∣∣_ _∤∤_
+infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_ _∥_ _∦_
 
 -- Divisibility from the left.
 --
@@ -34,7 +34,7 @@ infix 5 _∣ˡ_ _∤ˡ_ _∣ʳ_ _∤ʳ_ _∣_ _∤_ _∣∣_ _∤∤_
 -- make the use of pattern synonyms more ergonomic (see #2216 for
 -- further details). The record field names are not designed to be
 -- used explicitly and indeed aren't re-exported publicly by
--- `Algebra.X.Properties.Divisibility` modules.
+-- `Algebra.Properties.X.Divisibility` modules.
 
 record _∣ˡ_ (x y : A) : Set (a ⊔ ℓ) where
   constructor _,_
@@ -79,8 +79,29 @@ x ∤ y = ¬ x ∣ y
 -- Example: for ℕ  this is equivalent to x ≡ y,
 --          for ℤ  this is equivalent to (x ≡ y or x ≡ - y).
 
-_∣∣_ : Rel A (a ⊔ ℓ)
-x ∣∣ y = x ∣ y × y ∣ x
+_∥_ : Rel A (a ⊔ ℓ)
+x ∥ y = x ∣ y × y ∣ x
+
+_∦_ : Rel A (a ⊔ ℓ)
+x ∦ y = ¬ x ∥ y
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.3
+
+_∣∣_ = _∥_
+{-# WARNING_ON_USAGE _∣∣_
+"Warning: _∣∣_ was deprecated in v2.3.
+Please use _∥_ instead."
+#-}
+_∤∤_ = _∦_
+{-# WARNING_ON_USAGE _∤∤_
+"Warning: _∤∤_ was deprecated in v2.3.
+Please use _∦_ instead."
+#-}
 
-_∤∤_ : Rel A (a ⊔ ℓ)
-x ∤∤ y = ¬ x ∣∣ y

src/Algebra/Properties/Magma/Divisibility.agda

@@ -21,7 +21,7 @@ open Magma M
 -- Re-export divisibility relations publicly
 
 open import Algebra.Definitions.RawMagma rawMagma public
-  using (_∣_; _∤_; _∣∣_; _∤∤_; _∣ˡ_; _∤ˡ_; _∣ʳ_; _∤ʳ_; _,_)
+  using (_∣_; _∤_; _∥_; _∦_; _∣ˡ_; _∤ˡ_; _∣ʳ_; _∤ʳ_; _,_)
 
 ------------------------------------------------------------------------
 -- Properties of divisibility
@@ -54,34 +54,34 @@ xy≈z⇒y∣z x y xy≈z = ∣-respʳ-≈ xy≈z (x∣yx y x)
 ∤-resp-≈ = ∤-respʳ-≈ , ∤-respˡ-≈
 
 ------------------------------------------------------------------------
--- Properties of mutual divisibility _∣∣_
+-- Properties of mutual divisibility _∥_
 
-∣∣-sym : Symmetric _∣∣_
-∣∣-sym = swap
+∥-sym : Symmetric _∥_
+∥-sym = swap
 
-∣∣-respˡ-≈ : _∣∣_ Respectsˡ _≈_
-∣∣-respˡ-≈ x≈z (x∣y , y∣x) = ∣-respˡ-≈ x≈z x∣y , ∣-respʳ-≈ x≈z y∣x
+∥-respˡ-≈ : _∥_ Respectsˡ _≈_
+∥-respˡ-≈ x≈z (x∣y , y∣x) = ∣-respˡ-≈ x≈z x∣y , ∣-respʳ-≈ x≈z y∣x
 
-∣∣-respʳ-≈ : _∣∣_ Respectsʳ _≈_
-∣∣-respʳ-≈ y≈z (x∣y , y∣x) = ∣-respʳ-≈ y≈z x∣y , ∣-respˡ-≈ y≈z y∣x
+∥-respʳ-≈ : _∥_ Respectsʳ _≈_
+∥-respʳ-≈ y≈z (x∣y , y∣x) = ∣-respʳ-≈ y≈z x∣y , ∣-respˡ-≈ y≈z y∣x
 
-∣∣-resp-≈ : _∣∣_ Respects₂ _≈_
-∣∣-resp-≈ = ∣∣-respʳ-≈ , ∣∣-respˡ-≈
+∥-resp-≈ : _∥_ Respects₂ _≈_
+∥-resp-≈ = ∥-respʳ-≈ , ∥-respˡ-≈
 
 ------------------------------------------------------------------------
 -- Properties of mutual non-divisibility _∤∤_
 
-∤∤-sym : Symmetric _∤∤_
-∤∤-sym x∤∤y y∣∣x = contradiction (∣∣-sym y∣∣x) x∤∤y
+∦-sym : Symmetric _∦_
+∦-sym x∦y y∥x = contradiction (∥-sym y∥x) x∦y
 
-∤∤-respˡ-≈ : _∤∤_ Respectsˡ _≈_
-∤∤-respˡ-≈ x≈y x∤∤z y∣∣z = contradiction (∣∣-respˡ-≈ (sym x≈y) y∣∣z) x∤∤z
+∦-respˡ-≈ : _∦_ Respectsˡ _≈_
+∦-respˡ-≈ x≈y x∦z y∥z = contradiction (∥-respˡ-≈ (sym x≈y) y∥z) x∦z
 
-∤∤-respʳ-≈ : _∤∤_ Respectsʳ _≈_
-∤∤-respʳ-≈ x≈y z∤∤x z∣∣y = contradiction (∣∣-respʳ-≈ (sym x≈y) z∣∣y) z∤∤x
+∦-respʳ-≈ : _∦_ Respectsʳ _≈_
+∦-respʳ-≈ x≈y z∦x z∥y = contradiction (∥-respʳ-≈ (sym x≈y) z∥y) z∦x
 
-∤∤-resp-≈ : _∤∤_ Respects₂ _≈_
-∤∤-resp-≈ = ∤∤-respʳ-≈ , ∤∤-respˡ-≈
+∦-resp-≈ : _∦_ Respects₂ _≈_
+∦-resp-≈ = ∦-respʳ-≈ , ∦-respˡ-≈
 
 
 ------------------------------------------------------------------------
@@ -107,3 +107,46 @@ Please use ∣-respʳ-≈ instead. "
 "Warning: ∣-resp was deprecated in v2.2.
 Please use ∣-resp-≈ instead. "
 #-}
+
+-- Version 2.3
+
+∣∣-sym = ∥-sym
+{-# WARNING_ON_USAGE ∣∣-sym
+"Warning: ∣∣-sym was deprecated in v2.3.
+Please use ∥-sym instead. "
+#-}
+∣∣-respˡ-≈ = ∥-respˡ-≈
+{-# WARNING_ON_USAGE ∣∣-respˡ-≈
+"Warning: ∣∣-respˡ-≈ was deprecated in v2.3.
+Please use ∥-respˡ-≈ instead. "
+#-}
+∣∣-respʳ-≈ = ∥-respʳ-≈
+{-# WARNING_ON_USAGE ∣∣-respʳ-≈
+"Warning: ∣∣-respʳ-≈ was deprecated in v2.3.
+Please use ∥-respʳ-≈ instead. "
+#-}
+∣∣-resp-≈ = ∥-resp-≈
+{-# WARNING_ON_USAGE ∣∣-resp-≈
+"Warning: ∣∣-resp-≈ was deprecated in v2.3.
+Please use ∥-resp-≈ instead. "
+#-}
+∤∤-sym = ∦-sym
+{-# WARNING_ON_USAGE ∤∤-sym
+"Warning: ∤∤-sym was deprecated in v2.3.
+Please use ∦-sym instead. "
+#-}
+∤∤-respˡ-≈ = ∦-respˡ-≈
+{-# WARNING_ON_USAGE ∤∤-respˡ-≈
+"Warning: ∤∤-respˡ-≈ was deprecated in v2.3.
+Please use ∦-respˡ-≈ instead. "
+#-}
+∤∤-respʳ-≈ = ∦-respʳ-≈
+{-# WARNING_ON_USAGE ∤∤-respʳ-≈
+"Warning: ∤∤-respʳ-≈ was deprecated in v2.3.
+Please use ∦-respʳ-≈ instead. "
+#-}
+∤∤-resp-≈ = ∦-resp-≈
+{-# WARNING_ON_USAGE ∤∤-resp-≈
+"Warning: ∤∤-resp-≈ was deprecated in v2.3.
+Please use ∦-resp-≈ instead. "
+#-}

src/Algebra/Properties/Monoid/Divisibility.agda

@@ -52,15 +52,42 @@ infix 4 ε∣_
 ------------------------------------------------------------------------
 -- Properties of mutual divisibiity
 
-∣∣-refl : Reflexive _∣∣_
-∣∣-refl = ∣-refl , ∣-refl
+∥-refl : Reflexive _∥_
+∥-refl = ∣-refl , ∣-refl
 
-∣∣-reflexive : _≈_ ⇒ _∣∣_
-∣∣-reflexive x≈y = ∣-reflexive x≈y , ∣-reflexive (sym x≈y)
+∥-reflexive : _≈_ ⇒ _∥_
+∥-reflexive x≈y = ∣-reflexive x≈y , ∣-reflexive (sym x≈y)
 
-∣∣-isEquivalence : IsEquivalence _∣∣_
-∣∣-isEquivalence = record
-  { refl  = λ {x} → ∣∣-refl {x}
-  ; sym   = λ {x} {y} → ∣∣-sym {x} {y}
-  ; trans = λ {x} {y} {z} → ∣∣-trans {x} {y} {z}
+∥-isEquivalence : IsEquivalence _∥_
+∥-isEquivalence = record
+  { refl  = λ {x} → ∥-refl {x}
+  ; sym   = λ {x} {y} → ∥-sym {x} {y}
+  ; trans = λ {x} {y} {z} → ∥-trans {x} {y} {z}
   }
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.3
+
+∣∣-refl = ∥-refl
+{-# WARNING_ON_USAGE ∣∣-refl
+"Warning: ∣∣-refl was deprecated in v2.3.
+Please use ∥-refl instead. "
+#-}
+
+∣∣-reflexive = ∥-reflexive
+{-# WARNING_ON_USAGE ∣∣-reflexive
+"Warning: ∣∣-reflexive was deprecated in v2.3.
+Please use ∥-reflexive instead. "
+#-}
+
+∣∣-isEquivalence = ∥-isEquivalence
+{-# WARNING_ON_USAGE ∣∣-isEquivalence
+"Warning: ∣∣-isEquivalence was deprecated in v2.3.
+Please use ∥-isEquivalence instead. "
+#-}

src/Algebra/Properties/Semigroup/Divisibility.agda

@@ -28,7 +28,22 @@ open import Algebra.Properties.Magma.Divisibility magma public
   q ∙ p , trans (assoc q p _) (trans (∙-congˡ px≈y) qy≈z)
 
 ------------------------------------------------------------------------
--- Properties of _∣∣_
+-- Properties of _∥_
 
-∣∣-trans : Transitive _∣∣_
-∣∣-trans (x∣y , y∣x) (y∣z , z∣y) = ∣-trans x∣y y∣z , ∣-trans z∣y y∣x
+∥-trans : Transitive _∥_
+∥-trans (x∣y , y∣x) (y∣z , z∣y) = ∣-trans x∣y y∣z , ∣-trans z∣y y∣x
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.3
+
+∣∣-trans = ∥-trans
+{-# WARNING_ON_USAGE ∣∣-trans
+"Warning: ∣∣-trans was deprecated in v2.3.
+Please use ∥-trans instead. "
+#-}