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

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