[fixes #2178] regularise and specify/systematise, the conventions for symbol usage (#2185)

* regularise and specify/systematise, the conventions for symbol usage

* typos/revisions

Author: jamesmckinna

CHANGELOG.md

@@ -112,21 +112,21 @@ Non-backwards compatible changes
   always true and cannot be assumed in user's code.
 
 * Therefore the definitions have been changed as follows to make all their arguments explicit:
-  - `LeftCancellative _•_`
-    - From: `∀ x {y z} → (x • y) ≈ (x • z) → y ≈ z`
-    - To: `∀ x y z → (x • y) ≈ (x • z) → y ≈ z`
+  - `LeftCancellative _∙_`
+    - From: `∀ x {y z} → (x ∙ y) ≈ (x ∙ z) → y ≈ z`
+    - To: `∀ x y z → (x ∙ y) ≈ (x ∙ z) → y ≈ z`
 
-  - `RightCancellative _•_`
-    - From: `∀ {x} y z → (y • x) ≈ (z • x) → y ≈ z`
-    - To: `∀ x y z → (y • x) ≈ (z • x) → y ≈ z`
+  - `RightCancellative _∙_`
+    - From: `∀ {x} y z → (y ∙ x) ≈ (z ∙ x) → y ≈ z`
+    - To: `∀ x y z → (y ∙ x) ≈ (z ∙ x) → y ≈ z`
 
-  - `AlmostLeftCancellative e _•_`
-    - From: `∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z`
-    - To: `∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z`
+  - `AlmostLeftCancellative e _∙_`
+    - From: `∀ {x} y z → ¬ x ≈ e → (x ∙ y) ≈ (x ∙ z) → y ≈ z`
+    - To: `∀ x y z → ¬ x ≈ e → (x ∙ y) ≈ (x ∙ z) → y ≈ z`
 
-  - `AlmostRightCancellative e _•_`
-    - From: `∀ {x} y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z`
-    - To: `∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z`
+  - `AlmostRightCancellative e _∙_`
+    - From: `∀ {x} y z → ¬ x ≈ e → (y ∙ x) ≈ (z ∙ x) → y ≈ z`
+    - To: `∀ x y z → ¬ x ≈ e → (y ∙ x) ≈ (z ∙ x) → y ≈ z`
 
 * Correspondingly some proofs of the above types will need additional arguments passed explicitly.
   Instances can easily be fixed by adding additional underscores, e.g.
@@ -2152,16 +2152,16 @@ Additions to existing modules
 
 * Added new proofs to `Algebra.Consequences.Propositional`:
   ```agda
-  comm+assoc⇒middleFour     : Commutative _•_ → Associative _•_ → _•_ MiddleFourExchange _•_
-  identity+middleFour⇒assoc : Identity e _•_ → _•_ MiddleFourExchange _•_ → Associative _•_
-  identity+middleFour⇒comm  : Identity e _+_ → _•_ MiddleFourExchange _+_ → Commutative _•_
+  comm+assoc⇒middleFour     : Commutative _∙_ → Associative _∙_ → _∙_ MiddleFourExchange _∙_
+  identity+middleFour⇒assoc : Identity e _∙_ → _∙_ MiddleFourExchange _∙_ → Associative _∙_
+  identity+middleFour⇒comm  : Identity e _+_ → _∙_ MiddleFourExchange _+_ → Commutative _∙_
   ```
 
 * Added new proofs to `Algebra.Consequences.Setoid`:
   ```agda
-  comm+assoc⇒middleFour     : Congruent₂ _•_ → Commutative _•_ → Associative _•_ → _•_ MiddleFourExchange _•_
-  identity+middleFour⇒assoc : Congruent₂ _•_ → Identity e _•_ → _•_ MiddleFourExchange _•_ → Associative _•_
-  identity+middleFour⇒comm  : Congruent₂ _•_ → Identity e _+_ → _•_ MiddleFourExchange _+_ → Commutative _•_
+  comm+assoc⇒middleFour     : Congruent₂ _∙_ → Commutative _∙_ → Associative _∙_ → _∙_ MiddleFourExchange _∙_
+  identity+middleFour⇒assoc : Congruent₂ _∙_ → Identity e _∙_ → _∙_ MiddleFourExchange _∙_ → Associative _∙_
+  identity+middleFour⇒comm  : Congruent₂ _∙_ → Identity e _+_ → _∙_ MiddleFourExchange _+_ → Commutative _∙_
 
   involutive⇒surjective  : Involutive f  → Surjective f
   selfInverse⇒involutive : SelfInverse f → Involutive f
@@ -2171,15 +2171,15 @@ Additions to existing modules
   selfInverse⇒injective  : SelfInverse f → Injective f
   selfInverse⇒bijective  : SelfInverse f → Bijective f
 
-  comm+idˡ⇒id              : Commutative _•_ → LeftIdentity  e _•_ → Identity e _•_
-  comm+idʳ⇒id              : Commutative _•_ → RightIdentity e _•_ → Identity e _•_
-  comm+zeˡ⇒ze              : Commutative _•_ → LeftZero      e _•_ → Zero     e _•_
-  comm+zeʳ⇒ze              : Commutative _•_ → RightZero     e _•_ → Zero     e _•_
-  comm+invˡ⇒inv            : Commutative _•_ → LeftInverse  e _⁻¹ _•_ → Inverse e _⁻¹ _•_
-  comm+invʳ⇒inv            : Commutative _•_ → RightInverse e _⁻¹ _•_ → Inverse e _⁻¹ _•_
-  comm+distrˡ⇒distr        : Commutative _•_ → _•_ DistributesOverˡ _◦_ → _•_ DistributesOver _◦_
-  comm+distrʳ⇒distr        : Commutative _•_ → _•_ DistributesOverʳ _◦_ → _•_ DistributesOver _◦_
-  distrib+absorbs⇒distribˡ : Associative _•_ → Commutative _◦_ → _•_ Absorbs _◦_ → _◦_ Absorbs _•_ → _◦_ DistributesOver _•_ → _•_ DistributesOverˡ _◦_
+  comm+idˡ⇒id              : Commutative _∙_ → LeftIdentity  e _∙_ → Identity e _∙_
+  comm+idʳ⇒id              : Commutative _∙_ → RightIdentity e _∙_ → Identity e _∙_
+  comm+zeˡ⇒ze              : Commutative _∙_ → LeftZero      e _∙_ → Zero     e _∙_
+  comm+zeʳ⇒ze              : Commutative _∙_ → RightZero     e _∙_ → Zero     e _∙_
+  comm+invˡ⇒inv            : Commutative _∙_ → LeftInverse  e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_
+  comm+invʳ⇒inv            : Commutative _∙_ → RightInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_
+  comm+distrˡ⇒distr        : Commutative _∙_ → _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOver _◦_
+  comm+distrʳ⇒distr        : Commutative _∙_ → _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOver _◦_
+  distrib+absorbs⇒distribˡ : Associative _∙_ → Commutative _◦_ → _∙_ Absorbs _◦_ → _◦_ Absorbs _∙_ → _◦_ DistributesOver _∙_ → _∙_ DistributesOverˡ _◦_
   ```
 
 * Added new functions to `Algebra.Construct.DirectProduct`:

notes/style-guide.md

@@ -347,12 +347,12 @@ line of code, indented by two spaces.
 
 #### Variables
 
-* `Level` and `Set`s can always be generalized using the keyword `variable`.
+* `Level` and `Set`s can always be generalised using the keyword `variable`.
 
 * A file may only declare variables of other types if those types are used
   in the definition of the main type that the file concerns itself with.
-  At the moment the policy is *not* to generalize over any other types to
-  minimize the amount of information that users have to keep in their head
+  At the moment the policy is *not* to generalise over any other types to
+  minimise the amount of information that users have to keep in their head
   concurrently.
 
 * Example 1: the main type in `Data.List.Properties` is `List A` where `A : Set a`.
@@ -443,6 +443,44 @@ word within a compound word is capitalized except for the first word.
   relations should be used over the `¬` symbol (e.g. `m+n≮n` should be
   used instead of `¬m+n<n`).
 
+#### Symbols for operators and relations
+
+* The stdlib aims to use a consistent set of notations, governed by a
+  consistent set of conventions, but sometimes, different
+  Unicode/emacs-input-method symbols nevertheless can be rendered by
+  identical-*seeming* symbols, so this is an attempt to document these.
+
+* The typical binary operator in the `Algebra` hierarchy, inheriting
+  from the root `Structure`/`Bundle` `isMagma`/`Magma`, is written as
+  infix `∙`, obtained as `\.`, NOT as `\bu2`. Nevertheless, there is
+  also a 'generic' operator, written as infix `·`, obtained as
+  `\cdot`. Do NOT attempt to use related, but typographically
+  indistinguishable, symbols.
+
+* Similarly, 'primed' names and symbols, used to standardise names
+  apart, or to provide (more) simply-typed versions of
+  dependently-typed operations, should be written using `\'`, NOT the
+  unmarked `'` character.
+
+* 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.
+
+* Since v2.0, the `Algebra` hierarchy systematically introduces
+  consistent symbolic notation for the negated versions of the usual
+  binary predicates for equality, ordering etc. These are obtained
+  from the corresponding input sequence by adding `n` to the symbol
+  name, so that `≤`, obtained as `\le`, becomes `≰` obtained as
+  `\len`, etc.
+
+* Correspondingly, the flipped symbols (and their negations) for the
+  converse relations are systematically introduced, eg `≥` as `\ge`
+  and `≱` as `\gen`.
+
+* Any exceptions to these conventions should be flagged on the GitHub
+  `agda-stdlib` issue tracker in the usual way.
+
 #### Functions and relations over specific datatypes
 
 * When defining a new relation `P` over a datatype `X` in a `Data.X.Relation` module,

src/Algebra/Consequences/Propositional.agda

@@ -44,16 +44,16 @@ open Base public
 ------------------------------------------------------------------------
 -- Group-like structures
 
-module _ {_•_ _⁻¹ ε} where
+module _ {_∙_ _⁻¹ ε} where
 
-  assoc+id+invʳ⇒invˡ-unique : Associative _•_ → Identity ε _•_ →
-                              RightInverse ε _⁻¹ _•_ →
-                              ∀ x y → (x • y) ≡ ε → x ≡ (y ⁻¹)
+  assoc+id+invʳ⇒invˡ-unique : Associative _∙_ → Identity ε _∙_ →
+                              RightInverse ε _⁻¹ _∙_ →
+                              ∀ x y → (x ∙ y) ≡ ε → x ≡ (y ⁻¹)
   assoc+id+invʳ⇒invˡ-unique = Base.assoc+id+invʳ⇒invˡ-unique (cong₂ _)
 
-  assoc+id+invˡ⇒invʳ-unique : Associative _•_ → Identity ε _•_ →
-                              LeftInverse ε _⁻¹ _•_ →
-                              ∀ x y → (x • y) ≡ ε → y ≡ (x ⁻¹)
+  assoc+id+invˡ⇒invʳ-unique : Associative _∙_ → Identity ε _∙_ →
+                              LeftInverse ε _⁻¹ _∙_ →
+                              ∀ x y → (x ∙ y) ≡ ε → y ≡ (x ⁻¹)
   assoc+id+invˡ⇒invʳ-unique = Base.assoc+id+invˡ⇒invʳ-unique (cong₂ _)
 
 ------------------------------------------------------------------------
@@ -76,43 +76,43 @@ module _ {_+_ _*_ -_ 0#} where
 ------------------------------------------------------------------------
 -- Bisemigroup-like structures
 
-module _ {_•_ _◦_ : Op₂ A} (•-comm : Commutative _•_) where
+module _ {_∙_ _◦_ : Op₂ A} (∙-comm : Commutative _∙_) where
 
-  comm+distrˡ⇒distrʳ : _•_ DistributesOverˡ _◦_ → _•_ DistributesOverʳ _◦_
-  comm+distrˡ⇒distrʳ = Base.comm+distrˡ⇒distrʳ (cong₂ _) •-comm
+  comm+distrˡ⇒distrʳ : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_
+  comm+distrˡ⇒distrʳ = Base.comm+distrˡ⇒distrʳ (cong₂ _) ∙-comm
 
-  comm+distrʳ⇒distrˡ : _•_ DistributesOverʳ _◦_ → _•_ DistributesOverˡ _◦_
-  comm+distrʳ⇒distrˡ = Base.comm+distrʳ⇒distrˡ (cong₂ _) •-comm
+  comm+distrʳ⇒distrˡ : _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOverˡ _◦_
+  comm+distrʳ⇒distrˡ = Base.comm+distrʳ⇒distrˡ (cong₂ _) ∙-comm
 
-  comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y • z)) ≡ ((x ◦ y) • (x ◦ z)))
-  comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _◦_) •-comm
+  comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≡ ((x ◦ y) ∙ (x ◦ z)))
+  comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _◦_) ∙-comm
 
 ------------------------------------------------------------------------
 -- Selectivity
 
-module _ {_•_ : Op₂ A} where
+module _ {_∙_ : Op₂ A} where
 
-  sel⇒idem : Selective _•_ → Idempotent _•_
+  sel⇒idem : Selective _∙_ → Idempotent _∙_
   sel⇒idem = Base.sel⇒idem _≡_
 
 ------------------------------------------------------------------------
 -- Middle-Four Exchange
 
-module _ {_•_ : Op₂ A} where
+module _ {_∙_ : Op₂ A} where
 
-  comm+assoc⇒middleFour : Commutative _•_ → Associative _•_ →
-                          _•_ MiddleFourExchange _•_
-  comm+assoc⇒middleFour = Base.comm+assoc⇒middleFour (cong₂ _•_)
+  comm+assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
+                          _∙_ MiddleFourExchange _∙_
+  comm+assoc⇒middleFour = Base.comm+assoc⇒middleFour (cong₂ _∙_)
 
-  identity+middleFour⇒assoc : {e : A} → Identity e _•_ →
-                              _•_ MiddleFourExchange _•_ →
-                              Associative _•_
-  identity+middleFour⇒assoc = Base.identity+middleFour⇒assoc (cong₂ _•_)
+  identity+middleFour⇒assoc : {e : A} → Identity e _∙_ →
+                              _∙_ MiddleFourExchange _∙_ →
+                              Associative _∙_
+  identity+middleFour⇒assoc = Base.identity+middleFour⇒assoc (cong₂ _∙_)
 
   identity+middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
-                             _•_ MiddleFourExchange _+_ →
-                             Commutative _•_
-  identity+middleFour⇒comm = Base.identity+middleFour⇒comm (cong₂ _•_)
+                             _∙_ MiddleFourExchange _+_ →
+                             Commutative _∙_
+  identity+middleFour⇒comm = Base.identity+middleFour⇒comm (cong₂ _∙_)
 
 ------------------------------------------------------------------------
 -- Without Loss of Generality