diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9d9f403d64..c5f59f3d58 100644
--- a/CHANGELOG.md
+++ b/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`:
diff --git a/notes/style-guide.md b/notes/style-guide.md
index d6201abe88..95ef7ba2d0 100644
--- a/notes/style-guide.md
+++ b/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,
diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda
index 6f2626889c..1adcb12afc 100644
--- a/src/Algebra/Consequences/Propositional.agda
+++ b/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
diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
index 068ecb2d12..f90a801fe4 100644
--- a/src/Algebra/Consequences/Setoid.agda
+++ b/src/Algebra/Consequences/Setoid.agda
@@ -35,36 +35,36 @@ open import Algebra.Consequences.Base public
 ------------------------------------------------------------------------
 -- MiddleFourExchange
 
-module _ {_•_ : Op₂ A} (cong : Congruent₂ _•_) where
+module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where
 
-  comm+assoc⇒middleFour : Commutative _•_ → Associative _•_ →
-                          _•_ MiddleFourExchange _•_
+  comm+assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
+                          _∙_ MiddleFourExchange _∙_
   comm+assoc⇒middleFour comm assoc w x y z = begin
-    (w • x) • (y • z) ≈⟨ assoc w x (y • z) ⟩
-    w • (x • (y • z)) ≈⟨ cong refl (sym (assoc x y z)) ⟩
-    w • ((x • y) • z) ≈⟨ cong refl (cong (comm x y) refl) ⟩
-    w • ((y • x) • z) ≈⟨ cong refl (assoc y x z) ⟩
-    w • (y • (x • z)) ≈⟨ sym (assoc w y (x • z)) ⟩
-    (w • y) • (x • z) ∎
-
-  identity+middleFour⇒assoc : {e : A} → Identity e _•_ →
-                              _•_ MiddleFourExchange _•_ →
-                              Associative _•_
+    (w ∙ x) ∙ (y ∙ z) ≈⟨ assoc w x (y ∙ z) ⟩
+    w ∙ (x ∙ (y ∙ z)) ≈⟨ cong refl (sym (assoc x y z)) ⟩
+    w ∙ ((x ∙ y) ∙ z) ≈⟨ cong refl (cong (comm x y) refl) ⟩
+    w ∙ ((y ∙ x) ∙ z) ≈⟨ cong refl (assoc y x z) ⟩
+    w ∙ (y ∙ (x ∙ z)) ≈⟨ sym (assoc w y (x ∙ z)) ⟩
+    (w ∙ y) ∙ (x ∙ z) ∎
+
+  identity+middleFour⇒assoc : {e : A} → Identity e _∙_ →
+                              _∙_ MiddleFourExchange _∙_ →
+                              Associative _∙_
   identity+middleFour⇒assoc {e} (identityˡ , identityʳ) middleFour x y z = begin
-    (x • y) • z       ≈⟨ cong refl (sym (identityˡ z)) ⟩
-    (x • y) • (e • z) ≈⟨ middleFour x y e z ⟩
-    (x • e) • (y • z) ≈⟨ cong (identityʳ x) refl ⟩
-    x • (y • z)       ∎
+    (x ∙ y) ∙ z       ≈⟨ cong refl (sym (identityˡ z)) ⟩
+    (x ∙ y) ∙ (e ∙ z) ≈⟨ middleFour x y e z ⟩
+    (x ∙ e) ∙ (y ∙ z) ≈⟨ cong (identityʳ x) refl ⟩
+    x ∙ (y ∙ z)       ∎
 
   identity+middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
-                             _•_ MiddleFourExchange _+_ →
-                             Commutative _•_
+                             _∙_ MiddleFourExchange _+_ →
+                             Commutative _∙_
   identity+middleFour⇒comm {_+_} {e} (identityˡ , identityʳ) middleFour x y
     = begin
-    x • y             ≈⟨ sym (cong (identityˡ x) (identityʳ y)) ⟩
-    (e + x) • (y + e) ≈⟨ middleFour e x y e ⟩
-    (e + y) • (x + e) ≈⟨ cong (identityˡ y) (identityʳ x) ⟩
-    y • x             ∎
+    x ∙ y             ≈⟨ sym (cong (identityˡ x) (identityʳ y)) ⟩
+    (e + x) ∙ (y + e) ≈⟨ middleFour e x y e ⟩
+    (e + y) ∙ (x + e) ≈⟨ cong (identityˡ y) (identityʳ x) ⟩
+    y ∙ x             ∎
 
 ------------------------------------------------------------------------
 -- SelfInverse
@@ -98,182 +98,182 @@ module _ {f : Op₁ A} (self : SelfInverse f) where
 ------------------------------------------------------------------------
 -- Magma-like structures
 
-module _ {_•_ : Op₂ A} (comm : Commutative _•_) where
+module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) where
 
-  comm+cancelˡ⇒cancelʳ : LeftCancellative _•_ → RightCancellative _•_
+  comm+cancelˡ⇒cancelʳ : LeftCancellative _∙_ → RightCancellative _∙_
   comm+cancelˡ⇒cancelʳ cancelˡ x y z eq = cancelˡ x y z $ begin
-    x • y ≈⟨ comm x y ⟩
-    y • x ≈⟨ eq ⟩
-    z • x ≈⟨ comm z x ⟩
-    x • z ∎
+    x ∙ y ≈⟨ comm x y ⟩
+    y ∙ x ≈⟨ eq ⟩
+    z ∙ x ≈⟨ comm z x ⟩
+    x ∙ z ∎
 
-  comm+cancelʳ⇒cancelˡ : RightCancellative _•_ → LeftCancellative _•_
+  comm+cancelʳ⇒cancelˡ : RightCancellative _∙_ → LeftCancellative _∙_
   comm+cancelʳ⇒cancelˡ cancelʳ x y z eq = cancelʳ x y z $ begin
-    y • x ≈⟨ comm y x ⟩
-    x • y ≈⟨ eq ⟩
-    x • z ≈⟨ comm x z ⟩
-    z • x ∎
+    y ∙ x ≈⟨ comm y x ⟩
+    x ∙ y ≈⟨ eq ⟩
+    x ∙ z ≈⟨ comm x z ⟩
+    z ∙ x ∎
 
 ------------------------------------------------------------------------
 -- Monoid-like structures
 
-module _ {_•_ : Op₂ A} (comm : Commutative _•_) {e : A} where
+module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where
 
-  comm+idˡ⇒idʳ : LeftIdentity e _•_ → RightIdentity e _•_
+  comm+idˡ⇒idʳ : LeftIdentity e _∙_ → RightIdentity e _∙_
   comm+idˡ⇒idʳ idˡ x = begin
-    x • e ≈⟨ comm x e ⟩
-    e • x ≈⟨ idˡ x ⟩
+    x ∙ e ≈⟨ comm x e ⟩
+    e ∙ x ≈⟨ idˡ x ⟩
     x     ∎
 
-  comm+idʳ⇒idˡ : RightIdentity e _•_ → LeftIdentity e _•_
+  comm+idʳ⇒idˡ : RightIdentity e _∙_ → LeftIdentity e _∙_
   comm+idʳ⇒idˡ idʳ x = begin
-    e • x ≈⟨ comm e x ⟩
-    x • e ≈⟨ idʳ x ⟩
+    e ∙ x ≈⟨ comm e x ⟩
+    x ∙ e ≈⟨ idʳ x ⟩
     x     ∎
 
-  comm+idˡ⇒id : LeftIdentity e _•_ → Identity e _•_
+  comm+idˡ⇒id : LeftIdentity e _∙_ → Identity e _∙_
   comm+idˡ⇒id idˡ = idˡ , comm+idˡ⇒idʳ idˡ
 
-  comm+idʳ⇒id : RightIdentity e _•_ → Identity e _•_
+  comm+idʳ⇒id : RightIdentity e _∙_ → Identity e _∙_
   comm+idʳ⇒id idʳ = comm+idʳ⇒idˡ idʳ , idʳ
 
-  comm+zeˡ⇒zeʳ : LeftZero e _•_ → RightZero e _•_
+  comm+zeˡ⇒zeʳ : LeftZero e _∙_ → RightZero e _∙_
   comm+zeˡ⇒zeʳ zeˡ x = begin
-    x • e ≈⟨ comm x e ⟩
-    e • x ≈⟨ zeˡ x ⟩
+    x ∙ e ≈⟨ comm x e ⟩
+    e ∙ x ≈⟨ zeˡ x ⟩
     e     ∎
 
-  comm+zeʳ⇒zeˡ : RightZero e _•_ → LeftZero e _•_
+  comm+zeʳ⇒zeˡ : RightZero e _∙_ → LeftZero e _∙_
   comm+zeʳ⇒zeˡ zeʳ x = begin
-    e • x ≈⟨ comm e x ⟩
-    x • e ≈⟨ zeʳ x ⟩
+    e ∙ x ≈⟨ comm e x ⟩
+    x ∙ e ≈⟨ zeʳ x ⟩
     e     ∎
 
-  comm+zeˡ⇒ze : LeftZero e _•_ → Zero e _•_
+  comm+zeˡ⇒ze : LeftZero e _∙_ → Zero e _∙_
   comm+zeˡ⇒ze zeˡ = zeˡ , comm+zeˡ⇒zeʳ zeˡ
 
-  comm+zeʳ⇒ze : RightZero e _•_ → Zero e _•_
+  comm+zeʳ⇒ze : RightZero e _∙_ → Zero e _∙_
   comm+zeʳ⇒ze zeʳ = comm+zeʳ⇒zeˡ zeʳ , zeʳ
 
-  comm+almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _•_ →
-                                     AlmostRightCancellative e _•_
+  comm+almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _∙_ →
+                                     AlmostRightCancellative e _∙_
   comm+almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero x y z x≉e yx≈zx =
     cancelˡ-nonZero x y z x≉e $ begin
-      x • y ≈⟨ comm x y ⟩
-      y • x ≈⟨ yx≈zx ⟩
-      z • x ≈⟨ comm z x ⟩
-      x • z ∎
+      x ∙ y ≈⟨ comm x y ⟩
+      y ∙ x ≈⟨ yx≈zx ⟩
+      z ∙ x ≈⟨ comm z x ⟩
+      x ∙ z ∎
 
-  comm+almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _•_ →
-                                     AlmostLeftCancellative e _•_
+  comm+almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _∙_ →
+                                     AlmostLeftCancellative e _∙_
   comm+almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero x y z x≉e xy≈xz =
     cancelʳ-nonZero x y z x≉e $ begin
-      y • x ≈⟨ comm y x ⟩
-      x • y ≈⟨ xy≈xz ⟩
-      x • z ≈⟨ comm x z ⟩
-      z • x ∎
+      y ∙ x ≈⟨ comm y x ⟩
+      x ∙ y ≈⟨ xy≈xz ⟩
+      x ∙ z ≈⟨ comm x z ⟩
+      z ∙ x ∎
 
 ------------------------------------------------------------------------
 -- Group-like structures
 
-module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _•_) where
+module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) where
 
-  comm+invˡ⇒invʳ : LeftInverse e _⁻¹ _•_ → RightInverse e _⁻¹ _•_
+  comm+invˡ⇒invʳ : LeftInverse e _⁻¹ _∙_ → RightInverse e _⁻¹ _∙_
   comm+invˡ⇒invʳ invˡ x = begin
-    x • (x ⁻¹) ≈⟨ comm x (x ⁻¹) ⟩
-    (x ⁻¹) • x ≈⟨ invˡ x ⟩
+    x ∙ (x ⁻¹) ≈⟨ comm x (x ⁻¹) ⟩
+    (x ⁻¹) ∙ x ≈⟨ invˡ x ⟩
     e          ∎
 
-  comm+invˡ⇒inv : LeftInverse e _⁻¹ _•_ → Inverse e _⁻¹ _•_
+  comm+invˡ⇒inv : LeftInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_
   comm+invˡ⇒inv invˡ = invˡ , comm+invˡ⇒invʳ invˡ
 
-  comm+invʳ⇒invˡ : RightInverse e _⁻¹ _•_ → LeftInverse e _⁻¹ _•_
+  comm+invʳ⇒invˡ : RightInverse e _⁻¹ _∙_ → LeftInverse e _⁻¹ _∙_
   comm+invʳ⇒invˡ invʳ x = begin
-    (x ⁻¹) • x ≈⟨ comm (x ⁻¹) x ⟩
-    x • (x ⁻¹) ≈⟨ invʳ x ⟩
+    (x ⁻¹) ∙ x ≈⟨ comm (x ⁻¹) x ⟩
+    x ∙ (x ⁻¹) ≈⟨ invʳ x ⟩
     e          ∎
 
-  comm+invʳ⇒inv : RightInverse e _⁻¹ _•_ → Inverse e _⁻¹ _•_
+  comm+invʳ⇒inv : RightInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_
   comm+invʳ⇒inv invʳ = comm+invʳ⇒invˡ invʳ , invʳ
 
-module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _•_) where
+module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) where
 
-  assoc+id+invʳ⇒invˡ-unique : Associative _•_ →
-                              Identity e _•_ → RightInverse e _⁻¹ _•_ →
-                              ∀ x y → (x • y) ≈ e → x ≈ (y ⁻¹)
+  assoc+id+invʳ⇒invˡ-unique : Associative _∙_ →
+                              Identity e _∙_ → RightInverse e _⁻¹ _∙_ →
+                              ∀ x y → (x ∙ y) ≈ e → x ≈ (y ⁻¹)
   assoc+id+invʳ⇒invˡ-unique assoc (idˡ , idʳ) invʳ x y eq = begin
     x                ≈⟨ sym (idʳ x) ⟩
-    x • e            ≈⟨ cong refl (sym (invʳ y)) ⟩
-    x • (y • (y ⁻¹)) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩
-    (x • y) • (y ⁻¹) ≈⟨ cong eq refl ⟩
-    e • (y ⁻¹)       ≈⟨ idˡ (y ⁻¹) ⟩
+    x ∙ e            ≈⟨ cong refl (sym (invʳ y)) ⟩
+    x ∙ (y ∙ (y ⁻¹)) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩
+    (x ∙ y) ∙ (y ⁻¹) ≈⟨ cong eq refl ⟩
+    e ∙ (y ⁻¹)       ≈⟨ idˡ (y ⁻¹) ⟩
     y ⁻¹             ∎
 
-  assoc+id+invˡ⇒invʳ-unique : Associative _•_ →
-                              Identity e _•_ → LeftInverse e _⁻¹ _•_ →
-                              ∀ x y → (x • y) ≈ e → y ≈ (x ⁻¹)
+  assoc+id+invˡ⇒invʳ-unique : Associative _∙_ →
+                              Identity e _∙_ → LeftInverse e _⁻¹ _∙_ →
+                              ∀ x y → (x ∙ y) ≈ e → y ≈ (x ⁻¹)
   assoc+id+invˡ⇒invʳ-unique assoc (idˡ , idʳ) invˡ x y eq = begin
     y                ≈⟨ sym (idˡ y) ⟩
-    e • y            ≈⟨ cong (sym (invˡ x)) refl ⟩
-    ((x ⁻¹) • x) • y ≈⟨ assoc (x ⁻¹) x y ⟩
-    (x ⁻¹) • (x • y) ≈⟨ cong refl eq ⟩
-    (x ⁻¹) • e       ≈⟨ idʳ (x ⁻¹) ⟩
+    e ∙ y            ≈⟨ cong (sym (invˡ x)) refl ⟩
+    ((x ⁻¹) ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩
+    (x ⁻¹) ∙ (x ∙ y) ≈⟨ cong refl eq ⟩
+    (x ⁻¹) ∙ e       ≈⟨ idʳ (x ⁻¹) ⟩
     x ⁻¹             ∎
 
 ------------------------------------------------------------------------
 -- Bisemigroup-like structures
 
-module _ {_•_ _◦_ : Op₂ A}
+module _ {_∙_ _◦_ : Op₂ A}
          (◦-cong : Congruent₂ _◦_)
-         (•-comm : Commutative _•_)
+         (∙-comm : Commutative _∙_)
          where
 
-  comm+distrˡ⇒distrʳ :  _•_ DistributesOverˡ _◦_ → _•_ DistributesOverʳ _◦_
+  comm+distrˡ⇒distrʳ :  _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_
   comm+distrˡ⇒distrʳ distrˡ x y z = begin
-    (y ◦ z) • x       ≈⟨ •-comm (y ◦ z) x ⟩
-    x • (y ◦ z)       ≈⟨ distrˡ x y z ⟩
-    (x • y) ◦ (x • z) ≈⟨ ◦-cong (•-comm x y) (•-comm x z) ⟩
-    (y • x) ◦ (z • x) ∎
+    (y ◦ z) ∙ x       ≈⟨ ∙-comm (y ◦ z) x ⟩
+    x ∙ (y ◦ z)       ≈⟨ distrˡ x y z ⟩
+    (x ∙ y) ◦ (x ∙ z) ≈⟨ ◦-cong (∙-comm x y) (∙-comm x z) ⟩
+    (y ∙ x) ◦ (z ∙ x) ∎
 
-  comm+distrʳ⇒distrˡ : _•_ DistributesOverʳ _◦_ → _•_ DistributesOverˡ _◦_
+  comm+distrʳ⇒distrˡ : _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOverˡ _◦_
   comm+distrʳ⇒distrˡ distrˡ x y z = begin
-    x • (y ◦ z)       ≈⟨ •-comm x (y ◦ z) ⟩
-    (y ◦ z) • x       ≈⟨ distrˡ x y z ⟩
-    (y • x) ◦ (z • x) ≈⟨ ◦-cong (•-comm y x) (•-comm z x) ⟩
-    (x • y) ◦ (x • z) ∎
+    x ∙ (y ◦ z)       ≈⟨ ∙-comm x (y ◦ z) ⟩
+    (y ◦ z) ∙ x       ≈⟨ distrˡ x y z ⟩
+    (y ∙ x) ◦ (z ∙ x) ≈⟨ ◦-cong (∙-comm y x) (∙-comm z x) ⟩
+    (x ∙ y) ◦ (x ∙ z) ∎
 
-  comm+distrˡ⇒distr :  _•_ DistributesOverˡ _◦_ → _•_ DistributesOver _◦_
+  comm+distrˡ⇒distr :  _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOver _◦_
   comm+distrˡ⇒distr distrˡ = distrˡ , comm+distrˡ⇒distrʳ distrˡ
 
-  comm+distrʳ⇒distr :  _•_ DistributesOverʳ _◦_ → _•_ DistributesOver _◦_
+  comm+distrʳ⇒distr :  _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOver _◦_
   comm+distrʳ⇒distr distrʳ = comm+distrʳ⇒distrˡ distrʳ , distrʳ
 
-  comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y • z)) ≈ ((x ◦ y) • (x ◦ z)))
+  comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≈ ((x ◦ y) ∙ (x ◦ z)))
   comm⇒sym[distribˡ] x {y} {z} prf = begin
-    x ◦ (z • y)       ≈⟨ ◦-cong refl (•-comm z y) ⟩
-    x ◦ (y • z)       ≈⟨ prf ⟩
-    (x ◦ y) • (x ◦ z) ≈⟨ •-comm (x ◦ y) (x ◦ z) ⟩
-    (x ◦ z) • (x ◦ y) ∎
+    x ◦ (z ∙ y)       ≈⟨ ◦-cong refl (∙-comm z y) ⟩
+    x ◦ (y ∙ z)       ≈⟨ prf ⟩
+    (x ◦ y) ∙ (x ◦ z) ≈⟨ ∙-comm (x ◦ y) (x ◦ z) ⟩
+    (x ◦ z) ∙ (x ◦ y) ∎
 
 
-module _ {_•_ _◦_ : Op₂ A}
-         (•-cong  : Congruent₂ _•_)
-         (•-assoc : Associative _•_)
+module _ {_∙_ _◦_ : Op₂ A}
+         (∙-cong  : Congruent₂ _∙_)
+         (∙-assoc : Associative _∙_)
          (◦-comm  : Commutative _◦_)
          where
 
-  distrib+absorbs⇒distribˡ : _•_ Absorbs _◦_ →
-                             _◦_ Absorbs _•_ →
-                             _◦_ DistributesOver _•_ →
-                             _•_ DistributesOverˡ _◦_
-  distrib+absorbs⇒distribˡ •-absorbs-◦ ◦-absorbs-• (◦-distribˡ-• , ◦-distribʳ-•) x y z = begin
-    x • (y ◦ z)                    ≈⟨ •-cong (•-absorbs-◦ _ _) refl ⟨
-    (x • (x ◦ y)) • (y ◦ z)        ≈⟨  •-cong (•-cong refl (◦-comm _ _)) refl ⟩
-    (x • (y ◦ x)) • (y ◦ z)        ≈⟨  •-assoc _ _ _ ⟩
-    x • ((y ◦ x) • (y ◦ z))        ≈⟨ •-cong refl (◦-distribˡ-• _ _ _) ⟨
-    x • (y ◦ (x • z))              ≈⟨ •-cong (◦-absorbs-• _ _) refl ⟨
-    (x ◦ (x • z)) • (y ◦ (x • z))  ≈⟨ ◦-distribʳ-• _ _ _ ⟨
-    (x • y) ◦ (x • z)              ∎
+  distrib+absorbs⇒distribˡ : _∙_ Absorbs _◦_ →
+                             _◦_ Absorbs _∙_ →
+                             _◦_ DistributesOver _∙_ →
+                             _∙_ DistributesOverˡ _◦_
+  distrib+absorbs⇒distribˡ ∙-absorbs-◦ ◦-absorbs-∙ (◦-distribˡ-∙ , ◦-distribʳ-∙) x y z = begin
+    x ∙ (y ◦ z)                    ≈⟨ ∙-cong (∙-absorbs-◦ _ _) refl ⟨
+    (x ∙ (x ◦ y)) ∙ (y ◦ z)        ≈⟨  ∙-cong (∙-cong refl (◦-comm _ _)) refl ⟩
+    (x ∙ (y ◦ x)) ∙ (y ◦ z)        ≈⟨  ∙-assoc _ _ _ ⟩
+    x ∙ ((y ◦ x) ∙ (y ◦ z))        ≈⟨ ∙-cong refl (◦-distribˡ-∙ _ _ _) ⟨
+    x ∙ (y ◦ (x ∙ z))              ≈⟨ ∙-cong (◦-absorbs-∙ _ _) refl ⟨
+    (x ◦ (x ∙ z)) ∙ (y ◦ (x ∙ z))  ≈⟨ ◦-distribʳ-∙ _ _ _ ⟨
+    (x ∙ y) ◦ (x ∙ z)              ∎
 
 ------------------------------------------------------------------------
 -- Ring-like structures