diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3867278c6c..a7d32e0f92 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -29,6 +29,17 @@ Bug-fixes
 Non-backwards compatible changes
 --------------------------------
 
+* The notation for `Decidable` relations has been (partially) standardised: thus
+  - `_≡?_` (at `infix 4`) for `DecidableEquality`
+  - `_≈?_` (ditto.) for the fieldname of the general `IsDecEquivalence`
+
+  Despite being non-backwards compatible, because a fieldname has changed, the
+  old notation `_≟_` (which was used for both of the above) has been retained,
+  but deprecated. This leads to a large amount of (trivial) deprecations, in
+  addition to the substantive one under `Relation.Binary.Structures`, and in
+  `Data.{Nat|Fin}.Properties` for the concrete datatypes. These deprecations
+  are summarised below, but are not each documented for each affected module.
+
 * [issue #2547](https://github.com/agda/agda-stdlib/issues/2547)
   The names of the *implicit* binders in the following definitions have been
   rectified to be consistent with the rest of `Relation.Binary.Definitions`:
@@ -39,6 +50,7 @@ Non-backwards compatible changes
   `Algebra.*`, the field name of the basic homomorphism property `homo` in
   `Algebra.Morphism.Structures.IsMagmaHomomorphism` has been renamed to `∙-homo`.
 
+
 Minor improvements
 ------------------
 
@@ -59,7 +71,7 @@ Deprecated names
   inj⇒≟    ↦  inj⇒≡?
   ≟-≡      ↦  ≡?-≡
   ≟-≡-refl ↦  ≡?-≡-refl
-  ≟-≢     ↦  ≡?-≢
+  ≟-≢      ↦  ≡?-≢
   ```
 
 * In `Data.Integer.GCD`:
@@ -96,6 +108,22 @@ Deprecated names
   ≢-≟-identity     ↦   ≢-≡?-identity
   ```
 
+* In `Effect.Monad.Partiality`:
+  ```agda
+  _≟-Kind_     ↦   _≡?-Kind_
+  ```
+
+* In `Reflection.AST.AlphaEquality`:
+  ```agda
+  ≟⇒α     ↦   ≡?⇒α
+  ```
+
+* In `Relation.Binary.PropositionalEquality`:
+  ```agda
+  ≡-≟-identity     ↦   ≡-≡?-identity
+  ≢-≟-identity     ↦   ≢-≡?-identity
+  ```
+
 * In `Relation.Nary`:
   ```agda
   ≟-mapₙ     ↦   ≡?-mapₙ
diff --git a/doc/style-guide.md b/doc/style-guide.md
index ec81edbdd5..2714a94d4c 100644
--- a/doc/style-guide.md
+++ b/doc/style-guide.md
@@ -590,7 +590,7 @@ word within a compound word is capitalized except for the first word.
   where `R` is the underlying property being asserted to be `Decidable`,
   moreover typically sharing the same fixity and precedence as `R`: thus
   - `_≡?_` (at `infix 4`) for `DecidableEquality`
-  - `_≈?_` (ditto.) for the name of the general `IsDecEquivalence`
+  - `_≈?_` (ditto.) for the fieldname of the general `IsDecEquivalence`
 
 * Any exceptions to these conventions should be flagged on the GitHub
   `agda-stdlib` issue tracker in the usual way.
diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index afb18d81e9..1f3f2464f5 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -139,7 +139,7 @@ true  ≤? true  = yes b≤b
 ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
 ≤-isDecTotalOrder = record
   { isTotalOrder = ≤-isTotalOrder
-  ; _≟_          = _≡?_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≤?_
   }
 
diff --git a/src/Data/Char/Properties.agda b/src/Data/Char/Properties.agda
index 20b5adbedc..1844bfeb7c 100644
--- a/src/Data/Char/Properties.agda
+++ b/src/Data/Char/Properties.agda
@@ -179,7 +179,7 @@ _≤?_ = Refl.decidable <-cmp
 ≤-isDecPartialOrder : IsDecPartialOrder _≡_ _≤_
 ≤-isDecPartialOrder = record
   { isPartialOrder = ≤-isPartialOrder
-  ; _≟_            = _≡?_
+  ; _≈?_           = _≡?_
   ; _≤?_           = _≤?_
   }
 
@@ -245,7 +245,7 @@ x ≈? y = toℕ x ℕ.≡? toℕ y
 ≈-isDecEquivalence : IsDecEquivalence _≈_
 ≈-isDecEquivalence = record
   { isEquivalence = ≈-isEquivalence
-  ; _≟_            = _≈?_
+  ; _≈?_           = _≈?_
   }
 ≈-decSetoid : DecSetoid _ _
 ≈-decSetoid = record
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index e03f36cd04..e511fc492e 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -123,7 +123,7 @@ suc x ≡? suc y = map′ (cong suc) suc-injective (x ≡? y)
 ≡-isDecEquivalence : IsDecEquivalence {A = Fin n} _≡_
 ≡-isDecEquivalence = record
   { isEquivalence = ≡.isEquivalence
-  ; _≟_           = _≡?_
+  ; _≈?_          = _≡?_
   }
 
 ------------------------------------------------------------------------
@@ -356,7 +356,7 @@ m <? n = suc (toℕ m) ℕ.≤? toℕ n
 ≤-isDecTotalOrder : IsDecTotalOrder {A = Fin n} _≡_ _≤_
 ≤-isDecTotalOrder = record
   { isTotalOrder = ≤-isTotalOrder
-  ; _≟_          = _≡?_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≤?_
   }
 
@@ -1198,7 +1198,7 @@ module _ {ℓ} {S : Setoid a ℓ} (inj : Injection S (≡-setoid n)) where
   inj⇒decSetoid = record
     { isDecEquivalence = record
       { isEquivalence = isEquivalence
-      ; _≟_           = inj⇒≡?
+      ; _≈?_           = inj⇒≡?
       }
     }
 
diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda
index ac5ecfd804..528ab7c496 100644
--- a/src/Data/Fin/Subset/Properties.agda
+++ b/src/Data/Fin/Subset/Properties.agda
@@ -317,7 +317,7 @@ module _ (n : ℕ) where
   ⊂-isDecStrictPartialOrder : IsDecStrictPartialOrder {A = Subset n} _≡_ _⊂_
   ⊂-isDecStrictPartialOrder = record
     { isStrictPartialOrder = ⊂-isStrictPartialOrder
-    ; _≟_  = ≡-dec _≡?_
+    ; _≈?_ = ≡-dec _≡?_
     ; _<?_ = _⊂?_
     }
 
diff --git a/src/Data/Float/Properties.agda b/src/Data/Float/Properties.agda
index 9fe3e33ea4..d496e410bd 100644
--- a/src/Data/Float/Properties.agda
+++ b/src/Data/Float/Properties.agda
@@ -76,7 +76,7 @@ _≈?_ = On.decidable (Maybe.map Word64.toℕ ∘ toWord64) _≡_ (Maybe.≡-dec
 ≈-isDecEquivalence : IsDecEquivalence _≈_
 ≈-isDecEquivalence = record
   { isEquivalence = ≈-isEquivalence
-  ; _≟_           = _≈?_
+  ; _≈?_          = _≈?_
   }
 
 ≈-decSetoid : DecSetoid _ _
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 9ef98f4e62..aba5067444 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -162,7 +162,7 @@ _≤?_ : Decidable _≤_
 ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
 ≤-isDecTotalOrder = record
   { isTotalOrder = ≤-isTotalOrder
-  ; _≟_          = _≡?_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≤?_
   }
 
@@ -2404,4 +2404,3 @@ _≟_ = _≡?_
 "Warning: _≟_ was deprecated in v2.4.
 Please use _≡?_ instead."
 #-}
-
diff --git a/src/Data/List/Relation/Binary/Infix/Homogeneous/Properties.agda b/src/Data/List/Relation/Binary/Infix/Homogeneous/Properties.agda
index 642258716b..3828516236 100644
--- a/src/Data/List/Relation/Binary/Infix/Homogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Infix/Homogeneous/Properties.agda
@@ -42,6 +42,6 @@ isPartialOrder po = record
 isDecPartialOrder : IsDecPartialOrder R S → IsDecPartialOrder (Pointwise R) (Infix S)
 isDecPartialOrder dpo = record
   { isPartialOrder = isPartialOrder DPO.isPartialOrder
-  ; _≟_            = Pointwise.decidable DPO._≈?_
+  ; _≈?_           = Pointwise.decidable DPO._≈?_
   ; _≤?_           = infix? DPO._≤?_
   } where module DPO = IsDecPartialOrder dpo
diff --git a/src/Data/List/Relation/Binary/Lex/Strict.agda b/src/Data/List/Relation/Binary/Lex/Strict.agda
index 2c7dac26d0..1ede36d717 100644
--- a/src/Data/List/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/List/Relation/Binary/Lex/Strict.agda
@@ -203,7 +203,7 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
                           IsDecPartialOrder _≋_ _≤_
     ≤-isDecPartialOrder sto = record
       { isPartialOrder = ≤-isPartialOrder isStrictPartialOrder
-      ; _≟_             = Pointwise.decidable _≈?_
+      ; _≈?_            = Pointwise.decidable _≈?_
       ; _≤?_           = ≤-decidable _≈?_ _<?_
       } where open IsStrictTotalOrder sto
 
@@ -218,7 +218,7 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
                         IsDecTotalOrder _≋_ _≤_
     ≤-isDecTotalOrder sto = record
       { isTotalOrder = ≤-isTotalOrder sto
-      ; _≟_          = Pointwise.decidable _≈?_
+      ; _≈?_         = Pointwise.decidable _≈?_
       ; _≤?_         = ≤-decidable _≈?_ _<?_
       }
       where open IsStrictTotalOrder sto
diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda
index 817fa1cd3e..f43f6ff24b 100644
--- a/src/Data/List/Relation/Binary/Pointwise.agda
+++ b/src/Data/List/Relation/Binary/Pointwise.agda
@@ -65,7 +65,7 @@ isEquivalence eq = record
 isDecEquivalence : IsDecEquivalence R → IsDecEquivalence (Pointwise R)
 isDecEquivalence eq = record
   { isEquivalence = isEquivalence DE.isEquivalence
-  ; _≟_           = decidable     DE._≈?_
+  ; _≈?_          = decidable     DE._≈?_
   } where module DE = IsDecEquivalence eq
 
 isPreorder : IsPreorder R S → IsPreorder (Pointwise R) (Pointwise S)
diff --git a/src/Data/List/Relation/Binary/Prefix/Homogeneous/Properties.agda b/src/Data/List/Relation/Binary/Prefix/Homogeneous/Properties.agda
index b922af4cef..5e5141fa69 100644
--- a/src/Data/List/Relation/Binary/Prefix/Homogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Prefix/Homogeneous/Properties.agda
@@ -43,6 +43,6 @@ isPartialOrder po = record
 isDecPartialOrder : IsDecPartialOrder R S → IsDecPartialOrder (Pointwise R) (Prefix S)
 isDecPartialOrder dpo = record
   { isPartialOrder = isPartialOrder DPO.isPartialOrder
-  ; _≟_            = Pointwise.decidable DPO._≈?_
+  ; _≈?_           = Pointwise.decidable DPO._≈?_
   ; _≤?_           = prefix? DPO._≤?_
   } where module DPO = IsDecPartialOrder dpo
diff --git a/src/Data/List/Relation/Binary/Sublist/DecPropositional.agda b/src/Data/List/Relation/Binary/Sublist/DecPropositional.agda
index 3b1d1a9e71..2afa82bb87 100644
--- a/src/Data/List/Relation/Binary/Sublist/DecPropositional.agda
+++ b/src/Data/List/Relation/Binary/Sublist/DecPropositional.agda
@@ -35,7 +35,7 @@ open DecSetoidSublist (decSetoid _≈?_) using (_⊆?_) public
 ⊆-isDecPartialOrder : IsDecPartialOrder _≡_ _⊆_
 ⊆-isDecPartialOrder = record
   { isPartialOrder = ⊆-isPartialOrder
-  ; _≟_            = _≡?_
+  ; _≈?_           = _≡?_
   ; _≤?_           = _⊆?_
   }
 
diff --git a/src/Data/List/Relation/Binary/Sublist/DecSetoid.agda b/src/Data/List/Relation/Binary/Sublist/DecSetoid.agda
index ffa97d7a32..367e45783b 100644
--- a/src/Data/List/Relation/Binary/Sublist/DecSetoid.agda
+++ b/src/Data/List/Relation/Binary/Sublist/DecSetoid.agda
@@ -41,7 +41,7 @@ _⊆?_ = HeterogeneousProperties.sublist? _≈?_
 ⊆-isDecPartialOrder : IsDecPartialOrder _≋_ _⊆_
 ⊆-isDecPartialOrder = record
   { isPartialOrder = ⊆-isPartialOrder
-  ; _≟_            = _≋?_
+  ; _≈?_           = _≋?_
   ; _≤?_           = _⊆?_
   }
 
diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
index cca49934c0..6aeea7ad4a 100644
--- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
@@ -448,7 +448,7 @@ module _ {E : Rel A e} {R : Rel A r} where
                       IsDecPartialOrder (Pointwise E) (Sublist R)
   isDecPartialOrder ER-isDecPartialOrder = record
     { isPartialOrder = isPartialOrder ER.isPartialOrder
-    ; _≟_            = Pw.decidable   ER._≈?_
+    ; _≈?_           = Pw.decidable   ER._≈?_
     ; _≤?_           = sublist?       ER._≤?_
     } where module ER = IsDecPartialOrder ER-isDecPartialOrder
 
diff --git a/src/Data/List/Relation/Binary/Suffix/Homogeneous/Properties.agda b/src/Data/List/Relation/Binary/Suffix/Homogeneous/Properties.agda
index e61eef25ef..f25a5811d3 100644
--- a/src/Data/List/Relation/Binary/Suffix/Homogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Suffix/Homogeneous/Properties.agda
@@ -42,6 +42,6 @@ isPartialOrder po = record
 isDecPartialOrder : IsDecPartialOrder R S → IsDecPartialOrder (Pointwise R) (Suffix S)
 isDecPartialOrder dpo = record
   { isPartialOrder = isPartialOrder DPO.isPartialOrder
-  ; _≟_             = Pointwise.decidable DPO._≈?_
+  ; _≈?_            = Pointwise.decidable DPO._≈?_
   ; _≤?_           = suffix? DPO._≤?_
   } where module DPO = IsDecPartialOrder dpo
diff --git a/src/Data/Maybe/Relation/Binary/Pointwise.agda b/src/Data/Maybe/Relation/Binary/Pointwise.agda
index 962803099d..535415a6bc 100644
--- a/src/Data/Maybe/Relation/Binary/Pointwise.agda
+++ b/src/Data/Maybe/Relation/Binary/Pointwise.agda
@@ -92,7 +92,7 @@ module _ {a r} {A : Set a} {R : Rel A r} where
   isDecEquivalence : IsDecEquivalence R → IsDecEquivalence (Pointwise R)
   isDecEquivalence R-isDecEquivalence = record
     { isEquivalence = isEquivalence R.isEquivalence
-    ; _≟_           = dec R._≈?_
+    ; _≈?_          = dec R._≈?_
     } where module R = IsDecEquivalence R-isDecEquivalence
 
   pointwise⊆any : ∀ {x} → Pointwise R (just x) ⊆ Any (R x)
diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda
index 2691c529d7..a030600f20 100644
--- a/src/Data/Nat/Binary/Properties.agda
+++ b/src/Data/Nat/Binary/Properties.agda
@@ -584,7 +584,7 @@ x ≤? y with <-cmp x y
 ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
 ≤-isDecTotalOrder = record
   { isTotalOrder = ≤-isTotalOrder
-  ; _≟_          = _≡?_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≤?_
   }
 
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 8374a29356..e58c110dcd 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -123,7 +123,7 @@ m ≡? n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))
 ≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ})
 ≡-isDecEquivalence = record
   { isEquivalence = isEquivalence
-  ; _≟_            = _≡?_
+  ; _≈?_           = _≡?_
   }
 
 ≡-decSetoid : DecSetoid 0ℓ 0ℓ
@@ -253,7 +253,7 @@ _≥?_ = flip _≤?_
 ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
 ≤-isDecTotalOrder = record
   { isTotalOrder = ≤-isTotalOrder
-  ; _≟_          = _≡?_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≤?_
   }
 
diff --git a/src/Data/Product/Relation/Binary/Lex/NonStrict.agda b/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
index b28bb4610d..1101396b28 100644
--- a/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
+++ b/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
@@ -157,7 +157,7 @@ module _ {_≈₁_ : Rel A ℓ₁} {_≤₁_ : Rel A ℓ₂}
     { isTotalOrder = ×-isTotalOrder (_≟_ to₁)
                                     (isTotalOrder to₁)
                                     (isTotalOrder to₂)
-    ; _≟_          = Pointwise.×-decidable (_≈?_ to₁) (_≈?_ to₂)
+    ; _≈?_         = Pointwise.×-decidable (_≈?_ to₁) (_≈?_ to₂)
     ; _≤?_         = ×-decidable (_≈?_ to₁) (_≤?_ to₁) (_≤?_ to₂)
     }
     where open IsDecTotalOrder
diff --git a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
index 7e5541396f..443344a132 100644
--- a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
+++ b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
@@ -108,7 +108,7 @@ Pointwise R S (a , c) (b , d) = (R a b) × (S c d)
 ×-isDecEquivalence eq₁ eq₂ = record
   { isEquivalence = ×-isEquivalence
                       (isEquivalence eq₁) (isEquivalence eq₂)
-  ; _≟_           = ×-decidable (_≈?_ eq₁) (_≈?_ eq₂)
+  ; _≈?_          = ×-decidable (_≈?_ eq₁) (_≈?_ eq₂)
   } where open IsDecEquivalence
 
 ×-isPreorder : IsPreorder ≈₁ R → IsPreorder ≈₂ S →
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index db438c8f8f..697bb788e1 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -600,7 +600,7 @@ _≥?_ = flip _≤?_
 ≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
 ≤-isDecTotalOrder = record
   { isTotalOrder = ≤-isTotalOrder
-  ; _≟_          = _≡?_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≤?_
   }
 
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index c1e9908091..55f72423be 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -147,7 +147,7 @@ p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≡? ↥ q ℤ.* 
 ≃-isDecEquivalence : IsDecEquivalence _≃_
 ≃-isDecEquivalence = record
   { isEquivalence = ≃-isEquivalence
-  ; _≟_           = _≃?_
+  ; _≈?_          = _≃?_
   }
 
 ≄-isApartnessRelation : IsApartnessRelation _≃_ _≄_
@@ -326,7 +326,7 @@ _≥?_ = flip _≤?_
 ≤-isDecTotalOrder : IsDecTotalOrder _≃_ _≤_
 ≤-isDecTotalOrder = record
   { isTotalOrder = ≤-isTotalOrder
-  ; _≟_          = _≃?_
+  ; _≈?_         = _≃?_
   ; _≤?_         = _≤?_
   }
 
diff --git a/src/Data/String/Properties.agda b/src/Data/String/Properties.agda
index b47388d243..4ddf72062c 100644
--- a/src/Data/String/Properties.agda
+++ b/src/Data/String/Properties.agda
@@ -78,7 +78,7 @@ x ≈? y = Pointwise.decidable Char._≡?_ (toList x) (toList y)
 ≈-isDecEquivalence : IsDecEquivalence _≈_
 ≈-isDecEquivalence = record
   { isEquivalence = ≈-isEquivalence
-  ; _≟_           = _≈?_
+  ; _≈?_          = _≈?_
   }
 
 ≈-decSetoid : DecSetoid _ _
diff --git a/src/Data/Sum/Relation/Binary/LeftOrder.agda b/src/Data/Sum/Relation/Binary/LeftOrder.agda
index 32da713d04..dc53d78915 100644
--- a/src/Data/Sum/Relation/Binary/LeftOrder.agda
+++ b/src/Data/Sum/Relation/Binary/LeftOrder.agda
@@ -203,7 +203,7 @@ module _ {a₁ a₂} {A₁ : Set a₁} {A₂ : Set a₂}
                         IsDecTotalOrder (Pointwise ≈₁ ≈₂) (∼₁ ⊎-< ∼₂)
   ⊎-<-isDecTotalOrder to₁ to₂ = record
     { isTotalOrder = ⊎-<-isTotalOrder (isTotalOrder to₁) (isTotalOrder to₂)
-    ; _≟_          = PW.⊎-decidable (_≈?_  to₁) (_≈?_  to₂)
+    ; _≈?_         = PW.⊎-decidable (_≈?_  to₁) (_≈?_  to₂)
     ; _≤?_         = ⊎-<-decidable (_≤?_ to₁) (_≤?_ to₂)
     }
     where open IsDecTotalOrder
diff --git a/src/Data/Sum/Relation/Binary/Pointwise.agda b/src/Data/Sum/Relation/Binary/Pointwise.agda
index 6181d6166b..b27bd803d7 100644
--- a/src/Data/Sum/Relation/Binary/Pointwise.agda
+++ b/src/Data/Sum/Relation/Binary/Pointwise.agda
@@ -142,7 +142,7 @@ drop-inj₂ (inj₂ x) = x
 ⊎-isDecEquivalence eq₁ eq₂ = record
   { isEquivalence =
       ⊎-isEquivalence (isEquivalence eq₁) (isEquivalence eq₂)
-  ; _≟_           = ⊎-decidable (_≈?_ eq₁) (_≈?_ eq₂)
+  ; _≈?_          = ⊎-decidable (_≈?_ eq₁) (_≈?_ eq₂)
   } where open IsDecEquivalence
 
 ⊎-isPreorder : IsPreorder ≈₁ R → IsPreorder ≈₂ S →
diff --git a/src/Data/Unit/Polymorphic/Properties.agda b/src/Data/Unit/Polymorphic/Properties.agda
index 1d380179d4..eb9ddaa0c7 100644
--- a/src/Data/Unit/Polymorphic/Properties.agda
+++ b/src/Data/Unit/Polymorphic/Properties.agda
@@ -81,7 +81,7 @@ _ ≡? _ = yes refl
 ≡-isDecTotalOrder : ∀ ℓ → IsDecTotalOrder {ℓ} _≡_ _≡_
 ≡-isDecTotalOrder ℓ = record
   { isTotalOrder = ≡-isTotalOrder ℓ
-  ; _≟_          = _≡?_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≡?_
   }
 
diff --git a/src/Data/Unit/Properties.agda b/src/Data/Unit/Properties.agda
index e146852051..d81f104887 100644
--- a/src/Data/Unit/Properties.agda
+++ b/src/Data/Unit/Properties.agda
@@ -79,7 +79,7 @@ _ ≡? _ = yes refl
 ≡-isDecTotalOrder : IsDecTotalOrder _≡_ _≡_
 ≡-isDecTotalOrder = record
   { isTotalOrder = ≡-isTotalOrder
-  ; _≟_          = _≡?_
+  ; _≈?_         = _≡?_
   ; _≤?_         = _≡?_
   }
 
@@ -111,4 +111,3 @@ _≟_ = _≡?_
 "Warning: _≟_ was deprecated in v2.4.
 Please use _≡?_ instead."
 #-}
-
diff --git a/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda b/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
index acf7895d12..3734b8bbcf 100644
--- a/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
+++ b/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
@@ -68,7 +68,7 @@ module _ {R : Rel A ℓ} where
                      ∀ n → IsDecEquivalence (Pointwise R {n})
   isDecEquivalence isDecEq n = record
     { isEquivalence = isEquivalence Eq.isEquivalence n
-    ; _≟_           = decidable Eq._≈?_
+    ; _≈?_          = decidable Eq._≈?_
     } where module Eq = IsDecEquivalence isDecEq
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Vec/Relation/Binary/Lex/Strict.agda b/src/Data/Vec/Relation/Binary/Lex/Strict.agda
index 7d226b6327..3170964775 100644
--- a/src/Data/Vec/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/Strict.agda
@@ -167,7 +167,7 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
                               ∀ {n} → IsDecStrictPartialOrder (_≋_ {n} {n}) _<_
   <-isDecStrictPartialOrder ≺-isDecStrictPartialOrder = record
     { isStrictPartialOrder = <-isStrictPartialOrder O.isStrictPartialOrder
-    ; _≟_                  = Pointwise.decidable O._≈?_
+    ; _≈?_                 = Pointwise.decidable O._≈?_
     ; _<?_                 = <-decidable O._≈?_ O._<?_
     } where module O = IsDecStrictPartialOrder ≺-isDecStrictPartialOrder
 
@@ -279,7 +279,7 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
                         ∀ {n} → IsDecPartialOrder (_≋_ {n} {n}) _≤_
   ≤-isDecPartialOrder ≺-isDecStrictPartialOrder = record
     { isPartialOrder = ≤-isPartialOrder isStrictPartialOrder
-    ; _≟_            = Pointwise.decidable _≈?_
+    ; _≈?_           = Pointwise.decidable _≈?_
     ; _≤?_           = ≤-dec _≈?_ _<?_
     } where open IsDecStrictPartialOrder ≺-isDecStrictPartialOrder
 
@@ -294,7 +294,7 @@ module _ {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
                       ∀ {n} → IsDecTotalOrder (_≋_ {n} {n}) _≤_
   ≤-isDecTotalOrder ≺-isStrictTotalOrder = record
     { isTotalOrder = ≤-isTotalOrder ≺-isStrictTotalOrder
-    ; _≟_          = Pointwise.decidable _≈?_
+    ; _≈?_         = Pointwise.decidable _≈?_
     ; _≤?_         = ≤-dec _≈?_ _<?_
     } where open IsStrictTotalOrder ≺-isStrictTotalOrder
 
@@ -347,4 +347,3 @@ module ≤-Reasoning
     (<-transˡ Eq.isPartialEquivalence <-resp-≈ trans)
     (<-transʳ Eq.isPartialEquivalence <-resp-≈ trans)
     public
-
diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda b/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
index b73160eda6..ecbf837518 100644
--- a/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
+++ b/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
@@ -132,7 +132,7 @@ isDecEquivalence : ∀ {_∼_ : Rel A ℓ} {n} →
                    IsDecEquivalence (Pointwise _∼_ {n = n})
 isDecEquivalence decEquiv = record
   { isEquivalence = isEquivalence DecEq.isEquivalence
-  ; _≟_           = decidable DecEq._≈?_
+  ; _≈?_          = decidable DecEq._≈?_
   } where module DecEq = IsDecEquivalence decEquiv
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
index 20b56feaf5..d23f1db68a 100644
--- a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
+++ b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
@@ -139,7 +139,7 @@ module _ {_∼_ : Rel A ℓ} where
                      IsDecEquivalence (Pointwise _∼_ {n})
   isDecEquivalence decEquiv n = record
     { isEquivalence = isEquivalence Eq.isEquivalence n
-    ; _≟_           = decidable Eq._≈?_
+    ; _≈?_          = decidable Eq._≈?_
     } where module Eq = IsDecEquivalence decEquiv
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Word64/Properties.agda b/src/Data/Word64/Properties.agda
index 8aace3b0e0..0db0a1e85c 100644
--- a/src/Data/Word64/Properties.agda
+++ b/src/Data/Word64/Properties.agda
@@ -70,7 +70,7 @@ x ≈? y = toℕ x ℕ.≡? toℕ y
 ≈-isDecEquivalence : IsDecEquivalence _≈_
 ≈-isDecEquivalence = record
   { isEquivalence = ≈-isEquivalence
-  ; _≟_           = _≈?_
+  ; _≈?_          = _≈?_
   }
 
 ≈-decSetoid : DecSetoid _ _
diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda
index d1923a5377..66ca609dc6 100644
--- a/src/Relation/Binary/Bundles.agda
+++ b/src/Relation/Binary/Bundles.agda
@@ -64,7 +64,7 @@ record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where
     isDecEquivalence : IsDecEquivalence _≈_
 
   open IsDecEquivalence isDecEquivalence public
-    using (_≟_; _≈?_; isEquivalence)
+    using (_≈?_; _≟_; isEquivalence)
 
   setoid : Setoid c ℓ
   setoid = record
@@ -140,7 +140,7 @@ record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   private module DPO = IsDecPreorder isDecPreorder
 
   open DPO public
-    using (_≟_; _≈?_; _≲?_; isPreorder)
+    using (_≈?_; _≲?_; isPreorder)
 
   preorder : Preorder c ℓ₁ ℓ₂
   preorder = record
@@ -203,7 +203,7 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   private module DPO = IsDecPartialOrder isDecPartialOrder
 
   open DPO public
-    using (_≟_; _≈?_; _≤?_; isPartialOrder; isDecPreorder)
+    using (_≈?_; _≤?_; isPartialOrder; isDecPreorder)
 
   poset : Poset c ℓ₁ ℓ₂
   poset = record
@@ -258,7 +258,7 @@ record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂
   private module DSPO = IsDecStrictPartialOrder isDecStrictPartialOrder
 
   open DSPO public
-    using (_≟_; _≈?_; _<?_; isStrictPartialOrder)
+    using (_<?_; _≈?_; isStrictPartialOrder)
 
   strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂
   strictPartialOrder = record
@@ -318,7 +318,7 @@ record DecTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   private module DTO = IsDecTotalOrder isDecTotalOrder
 
   open DTO public
-    using (_≟_; _≈?_; _≤?_; isTotalOrder; isDecPartialOrder)
+    using (_≈?_; _≤?_; isTotalOrder; isDecPartialOrder)
 
   totalOrder : TotalOrder c ℓ₁ ℓ₂
   totalOrder = record
@@ -352,7 +352,7 @@ record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) wh
 
   open IsStrictTotalOrder isStrictTotalOrder public
     using
-    ( _≟_; _≈?_; _<?_; compare; isStrictPartialOrder
+    ( _≈?_; _<?_; compare; isStrictPartialOrder
     ; isDecStrictPartialOrder; isDecEquivalence
     )
 
@@ -423,4 +423,3 @@ record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) w
   open RawRelation rawRelation public
     renaming (_≁_ to _¬#_; _∼ᵒ_ to _#ᵒ_; _≁ᵒ_ to _¬#ᵒ_)
     hiding (Carrier; _≈_ ; _∼_)
-
diff --git a/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda b/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
index 79909bc807..21b2ec5dfa 100644
--- a/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
+++ b/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
@@ -134,7 +134,7 @@ module _ {e} {_≈_ : Rel A e} where
 ≤₋-isDecPartialOrder-≡ : IsDecPartialOrder _≡_ _≤_ → IsDecPartialOrder _≡_ _≤₋_
 ≤₋-isDecPartialOrder-≡ ≤-isDecPartialOrder = record
   { isPartialOrder = ≤₋-isPartialOrder-≡ isPartialOrder
-  ; _≟_            = ≡-dec _≈?_
+  ; _≈?_           = ≡-dec _≈?_
   ; _≤?_           = ≤₋-dec _≤?_
   } where open IsDecPartialOrder ≤-isDecPartialOrder
 
@@ -147,7 +147,7 @@ module _ {e} {_≈_ : Rel A e} where
 ≤₋-isDecTotalOrder-≡ : IsDecTotalOrder _≡_ _≤_ → IsDecTotalOrder _≡_ _≤₋_
 ≤₋-isDecTotalOrder-≡ ≤-isDecTotalOrder = record
   { isTotalOrder = ≤₋-isTotalOrder-≡ isTotalOrder
-  ; _≟_          = ≡-dec _≈?_
+  ; _≈?_         = ≡-dec _≈?_
   ; _≤?_         = ≤₋-dec _≤?_
   } where open IsDecTotalOrder ≤-isDecTotalOrder
 
@@ -174,7 +174,7 @@ module _ {e} {_≈_ : Rel A e} where
   ≤₋-isDecPartialOrder : IsDecPartialOrder _≈_ _≤_ → IsDecPartialOrder _≈₋_ _≤₋_
   ≤₋-isDecPartialOrder ≤-isDecPartialOrder = record
     { isPartialOrder = ≤₋-isPartialOrder isPartialOrder
-    ; _≟_            = ≈₋-dec _≈?_
+    ; _≈?_           = ≈₋-dec _≈?_
     ; _≤?_           = ≤₋-dec _≤?_
     } where open IsDecPartialOrder ≤-isDecPartialOrder
 
@@ -187,6 +187,6 @@ module _ {e} {_≈_ : Rel A e} where
   ≤₋-isDecTotalOrder : IsDecTotalOrder _≈_ _≤_ → IsDecTotalOrder _≈₋_ _≤₋_
   ≤₋-isDecTotalOrder ≤-isDecTotalOrder = record
     { isTotalOrder = ≤₋-isTotalOrder isTotalOrder
-    ; _≟_          = ≈₋-dec _≈?_
+    ; _≈?_         = ≈₋-dec _≈?_
     ; _≤?_         = ≤₋-dec _≤?_
     } where open IsDecTotalOrder ≤-isDecTotalOrder
diff --git a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
index 8fe95ebd81..b6e6b55043 100644
--- a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
+++ b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
@@ -166,7 +166,7 @@ module _ {e} {_≈_ : Rel A e} where
                                IsDecStrictPartialOrder _≡_ _<₋_
 <₋-isDecStrictPartialOrder-≡ dectot = record
   { isStrictPartialOrder = <₋-isStrictPartialOrder-≡ isStrictPartialOrder
-  ; _≟_                  = ≡-dec _≈?_
+  ; _≈?_                 = ≡-dec _≈?_
   ; _<?_                 = <₋-dec _<?_
   } where open IsDecStrictPartialOrder dectot
 
@@ -197,7 +197,7 @@ module _ {e} {_≈_ : Rel A e} where
                                IsDecStrictPartialOrder _≈₋_ _<₋_
   <₋-isDecStrictPartialOrder dectot = record
     { isStrictPartialOrder = <₋-isStrictPartialOrder isStrictPartialOrder
-    ; _≟_                  = ≈₋-dec _≈?_
+    ; _≈?_                 = ≈₋-dec _≈?_
     ; _<?_                 = <₋-dec _<?_
     } where open IsDecStrictPartialOrder dectot
 
diff --git a/src/Relation/Binary/Construct/Add/Point/Equality.agda b/src/Relation/Binary/Construct/Add/Point/Equality.agda
index a3dccddbf7..5f18636854 100644
--- a/src/Relation/Binary/Construct/Add/Point/Equality.agda
+++ b/src/Relation/Binary/Construct/Add/Point/Equality.agda
@@ -79,5 +79,5 @@ data _≈∙_ : Rel (Pointed A) (a ⊔ ℓ) where
 ≈∙-isDecEquivalence : IsDecEquivalence _≈_ → IsDecEquivalence _≈∙_
 ≈∙-isDecEquivalence ≈-isDecEquivalence = record
   { isEquivalence = ≈∙-isEquivalence isEquivalence
-  ; _≟_           = ≈∙-dec _≈?_
+  ; _≈?_          = ≈∙-dec _≈?_
   } where open IsDecEquivalence ≈-isDecEquivalence
diff --git a/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda b/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
index 6587683b0c..2538cb3387 100644
--- a/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
+++ b/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
@@ -133,7 +133,7 @@ module _ {e} {_≈_ : Rel A e} where
 ≤⁺-isDecPartialOrder-≡ : IsDecPartialOrder _≡_ _≤_ → IsDecPartialOrder _≡_ _≤⁺_
 ≤⁺-isDecPartialOrder-≡ ≤-isDecPartialOrder = record
   { isPartialOrder = ≤⁺-isPartialOrder-≡ isPartialOrder
-  ; _≟_            = ≡-dec _≈?_
+  ; _≈?_           = ≡-dec _≈?_
   ; _≤?_           = ≤⁺-dec _≤?_
   } where open IsDecPartialOrder ≤-isDecPartialOrder
 
@@ -146,7 +146,7 @@ module _ {e} {_≈_ : Rel A e} where
 ≤⁺-isDecTotalOrder-≡ : IsDecTotalOrder _≡_ _≤_ → IsDecTotalOrder _≡_ _≤⁺_
 ≤⁺-isDecTotalOrder-≡ ≤-isDecTotalOrder = record
   { isTotalOrder = ≤⁺-isTotalOrder-≡ isTotalOrder
-  ; _≟_          = ≡-dec _≈?_
+  ; _≈?_         = ≡-dec _≈?_
   ; _≤?_         = ≤⁺-dec _≤?_
   } where open IsDecTotalOrder ≤-isDecTotalOrder
 
@@ -173,7 +173,7 @@ module _ {e} {_≈_ : Rel A e} where
   ≤⁺-isDecPartialOrder : IsDecPartialOrder _≈_ _≤_ → IsDecPartialOrder _≈⁺_ _≤⁺_
   ≤⁺-isDecPartialOrder ≤-isDecPartialOrder = record
     { isPartialOrder = ≤⁺-isPartialOrder isPartialOrder
-    ; _≟_            = ≈⁺-dec _≈?_
+    ; _≈?_           = ≈⁺-dec _≈?_
     ; _≤?_           = ≤⁺-dec _≤?_
     } where open IsDecPartialOrder ≤-isDecPartialOrder
 
@@ -186,6 +186,6 @@ module _ {e} {_≈_ : Rel A e} where
   ≤⁺-isDecTotalOrder : IsDecTotalOrder _≈_ _≤_ → IsDecTotalOrder _≈⁺_ _≤⁺_
   ≤⁺-isDecTotalOrder ≤-isDecTotalOrder = record
     { isTotalOrder = ≤⁺-isTotalOrder isTotalOrder
-    ; _≟_          = ≈⁺-dec _≈?_
+    ; _≈?_         = ≈⁺-dec _≈?_
     ; _≤?_         = ≤⁺-dec _≤?_
     } where open IsDecTotalOrder ≤-isDecTotalOrder
diff --git a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
index eafeeed7b4..fda4386247 100644
--- a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
+++ b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
@@ -150,7 +150,7 @@ module _ {e} {_≈_ : Rel A e} where
                                IsDecStrictPartialOrder _≡_ _<⁺_
 <⁺-isDecStrictPartialOrder-≡ dectot = record
   { isStrictPartialOrder = <⁺-isStrictPartialOrder-≡ isStrictPartialOrder
-  ; _≟_                  = ≡-dec _≈?_
+  ; _≈?_                 = ≡-dec _≈?_
   ; _<?_                 = <⁺-dec _<?_
   } where open IsDecStrictPartialOrder dectot
 
@@ -181,7 +181,7 @@ module _ {e} {_≈_ : Rel A e} where
                                IsDecStrictPartialOrder _≈⁺_ _<⁺_
   <⁺-isDecStrictPartialOrder dectot = record
     { isStrictPartialOrder = <⁺-isStrictPartialOrder isStrictPartialOrder
-    ; _≟_                  = ≈⁺-dec _≈?_
+    ; _≈?_                 = ≈⁺-dec _≈?_
     ; _<?_                 = <⁺-dec _<?_
     } where open IsDecStrictPartialOrder dectot
 
@@ -191,4 +191,3 @@ module _ {e} {_≈_ : Rel A e} where
     { isStrictPartialOrder = <⁺-isStrictPartialOrder isStrictPartialOrder
     ; compare              = <⁺-cmp compare
     } where open IsStrictTotalOrder strictot
-
diff --git a/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda b/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda
index eee787bf14..9e56932063 100644
--- a/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda
+++ b/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda
@@ -134,7 +134,7 @@ module _ {_~_ : Rel A ℓ} where
   isDecPartialOrder : IsDecStrictPartialOrder _≡_ _~_ → IsDecPartialOrder _≡_ _~ᵒ_
   isDecPartialOrder O = record
     { isPartialOrder = isPartialOrder O.isStrictPartialOrder
-    ; _≟_            = O._≈?_
+    ; _≈?_           = O._≈?_
     ; _≤?_           = dec O._≈?_ O._<?_
     } where module O = IsDecStrictPartialOrder O
 
@@ -147,6 +147,6 @@ module _ {_~_ : Rel A ℓ} where
   isDecTotalOrder : IsStrictTotalOrder _≡_ _~_ → IsDecTotalOrder _≡_ _~ᵒ_
   isDecTotalOrder O = record
     { isTotalOrder = isTotalOrder O
-    ; _≟_          = _≈?_
+    ; _≈?_         = _≈?_
     ; _≤?_         = dec _≈?_ _<?_
     } where open IsStrictTotalOrder O
diff --git a/src/Relation/Binary/Construct/Flip/EqAndOrd.agda b/src/Relation/Binary/Construct/Flip/EqAndOrd.agda
index 79aa0ce21c..075ec2f8a8 100644
--- a/src/Relation/Binary/Construct/Flip/EqAndOrd.agda
+++ b/src/Relation/Binary/Construct/Flip/EqAndOrd.agda
@@ -102,7 +102,7 @@ isEquivalence {≈ = ≈} eq = record
 isDecEquivalence : IsDecEquivalence ≈ → IsDecEquivalence (flip ≈)
 isDecEquivalence {≈ = ≈} eq = record
   { isEquivalence = isEquivalence Dec.isEquivalence
-  ; _≟_           = dec ≈ Dec._≈?_
+  ; _≈?_          = dec ≈ Dec._≈?_
   } where module Dec = IsDecEquivalence eq
 
 isPreorder : IsPreorder ≈ ∼ → IsPreorder ≈ (flip ∼)
@@ -133,7 +133,7 @@ isTotalOrder O = record
 isDecTotalOrder : IsDecTotalOrder ≈ ≤ → IsDecTotalOrder ≈ (flip ≤)
 isDecTotalOrder O = record
   { isTotalOrder = isTotalOrder O.isTotalOrder
-  ; _≟_          = O._≈?_
+  ; _≈?_         = O._≈?_
   ; _≤?_         = dec _ O._≤?_
   } where module O = IsDecTotalOrder O
 
diff --git a/src/Relation/Binary/Construct/Flip/Ord.agda b/src/Relation/Binary/Construct/Flip/Ord.agda
index c830a5fab9..381093e453 100644
--- a/src/Relation/Binary/Construct/Flip/Ord.agda
+++ b/src/Relation/Binary/Construct/Flip/Ord.agda
@@ -101,7 +101,7 @@ isEquivalence {≈ = ≈} eq = record
 isDecEquivalence : IsDecEquivalence ≈ → IsDecEquivalence (flip ≈)
 isDecEquivalence {≈ = ≈} dec = record
   { isEquivalence = isEquivalence Dec.isEquivalence
-  ; _≟_           = decidable ≈ Dec._≈?_
+  ; _≈?_          = decidable ≈ Dec._≈?_
   } where module Dec = IsDecEquivalence dec
 
 isPreorder : IsPreorder ≈ ∼ → IsPreorder (flip ≈) (flip ∼)
@@ -127,7 +127,7 @@ isTotalOrder {≈ = ≈} {≤ = ≤} O = record
 isDecTotalOrder : IsDecTotalOrder ≈ ≤ → IsDecTotalOrder (flip ≈) (flip ≤)
 isDecTotalOrder {≈ = ≈} {≤ = ≤} O = record
   { isTotalOrder = isTotalOrder O.isTotalOrder
-  ; _≟_          = decidable ≈ O._≈?_
+  ; _≈?_         = decidable ≈ O._≈?_
   ; _≤?_         = decidable ≤ O._≤?_
   } where module O = IsDecTotalOrder O
 
diff --git a/src/Relation/Binary/Construct/Interior/Symmetric.agda b/src/Relation/Binary/Construct/Interior/Symmetric.agda
index 4acbd92e20..bb0f11c4fd 100644
--- a/src/Relation/Binary/Construct/Interior/Symmetric.agda
+++ b/src/Relation/Binary/Construct/Interior/Symmetric.agda
@@ -111,7 +111,7 @@ module _ {R : Rel A ℓ} (refl : Reflexive R) (trans : Transitive R) where
     isDecPartialOrder : IsDecPartialOrder (SymInterior R) R
     isDecPartialOrder = record
       { isPartialOrder = isPartialOrder
-      ; _≟_  = decidable R?
+      ; _≈?_ = decidable R?
       ; _≤?_ = R?
       }
 
@@ -123,4 +123,3 @@ module _ {R : Rel A ℓ} (refl : Reflexive R) (trans : Transitive R) where
 
     isDecEquivalence : IsDecEquivalence (SymInterior R)
     isDecEquivalence = DecPoset.Eq.isDecEquivalence decPoset
-
diff --git a/src/Relation/Binary/Construct/Intersection.agda b/src/Relation/Binary/Construct/Intersection.agda
index fbf3004c5d..77dc37ebb2 100644
--- a/src/Relation/Binary/Construct/Intersection.agda
+++ b/src/Relation/Binary/Construct/Intersection.agda
@@ -104,7 +104,7 @@ isEquivalence {L = L} {R = R} eqₗ eqᵣ = record
 isDecEquivalence : IsDecEquivalence L → IsDecEquivalence R → IsDecEquivalence (L ∩ R)
 isDecEquivalence eqₗ eqᵣ = record
   { isEquivalence = isEquivalence L.isEquivalence R.isEquivalence
-  ; _≟_            = L._≈?_ ∩? R._≈?_
+  ; _≈?_           = L._≈?_ ∩? R._≈?_
   } where module L = IsDecEquivalence eqₗ; module R = IsDecEquivalence eqᵣ
 
 isPreorder : IsPreorder ≈ L → IsPreorder ≈ R → IsPreorder ≈ (L ∩ R)
diff --git a/src/Relation/Binary/Construct/NaturalOrder/Left.agda b/src/Relation/Binary/Construct/NaturalOrder/Left.agda
index 89e6687042..ed96b5f238 100644
--- a/src/Relation/Binary/Construct/NaturalOrder/Left.agda
+++ b/src/Relation/Binary/Construct/NaturalOrder/Left.agda
@@ -143,7 +143,7 @@ isDecPartialOrder : IsSemilattice _∙_ → Decidable _≈_ →
                     IsDecPartialOrder _≈_ _≤_
 isDecPartialOrder semilattice _≈?_ = record
   { isPartialOrder = isPartialOrder semilattice
-  ; _≟_            = _≈?_
+  ; _≈?_           = _≈?_
   ; _≤?_           = dec _≈?_
   }
 
@@ -158,7 +158,7 @@ isDecTotalOrder : IsSemilattice _∙_ → Selective _∙_ →
                   Decidable _≈_ → IsDecTotalOrder _≈_ _≤_
 isDecTotalOrder latt sel _≈?_ = record
   { isTotalOrder = isTotalOrder latt sel
-  ; _≟_          = _≈?_
+  ; _≈?_         = _≈?_
   ; _≤?_         = dec _≈?_
   }
 
diff --git a/src/Relation/Binary/Construct/NaturalOrder/Right.agda b/src/Relation/Binary/Construct/NaturalOrder/Right.agda
index 6adbc3dec6..39a9aeaec2 100644
--- a/src/Relation/Binary/Construct/NaturalOrder/Right.agda
+++ b/src/Relation/Binary/Construct/NaturalOrder/Right.agda
@@ -115,7 +115,7 @@ isDecPartialOrder : IsSemilattice _∙_ → Decidable _≈_ →
                     IsDecPartialOrder _≈_ _≤_
 isDecPartialOrder semilattice _≈?_ = record
   { isPartialOrder = isPartialOrder semilattice
-  ; _≟_            = _≈?_
+  ; _≈?_           = _≈?_
   ; _≤?_           = dec _≈?_
   }
 
@@ -130,7 +130,7 @@ isDecTotalOrder : IsSemilattice _∙_ → Selective _∙_ →
                   Decidable _≈_ → IsDecTotalOrder _≈_ _≤_
 isDecTotalOrder latt sel _≈?_ = record
   { isTotalOrder = isTotalOrder latt sel
-  ; _≟_          = _≈?_
+  ; _≈?_         = _≈?_
   ; _≤?_         = dec _≈?_
   }
 
diff --git a/src/Relation/Binary/Construct/NonStrictToStrict.agda b/src/Relation/Binary/Construct/NonStrictToStrict.agda
index 178b0b0248..73e0ff5a04 100644
--- a/src/Relation/Binary/Construct/NonStrictToStrict.agda
+++ b/src/Relation/Binary/Construct/NonStrictToStrict.agda
@@ -135,7 +135,7 @@ x < y = x ≤ y × x ≉ y
                             IsDecStrictPartialOrder _≈_ _<_
 <-isDecStrictPartialOrder dpo = record
   { isStrictPartialOrder = <-isStrictPartialOrder isPartialOrder
-  ; _≟_  = _≈?_
+  ; _≈?_ = _≈?_
   ; _<?_ = <-decidable _≈?_ _≤?_
   } where open IsDecPartialOrder dpo
 
diff --git a/src/Relation/Binary/Construct/On.agda b/src/Relation/Binary/Construct/On.agda
index 56e238c122..c505488c61 100644
--- a/src/Relation/Binary/Construct/On.agda
+++ b/src/Relation/Binary/Construct/On.agda
@@ -100,7 +100,7 @@ module _ (f : B → A) {≈ : Rel A ℓ₁} where
                      IsDecEquivalence (≈ on f)
   isDecEquivalence dec = record
     { isEquivalence = isEquivalence Dec.isEquivalence
-    ; _≟_           = decidable f ≈ Dec._≈?_
+    ; _≈?_          = decidable f ≈ Dec._≈?_
     } where module Dec = IsDecEquivalence dec
 
 module _ (f : B → A) {≈ : Rel A ℓ₁} {∼ : Rel A ℓ₂} where
@@ -123,7 +123,7 @@ module _ (f : B → A) {≈ : Rel A ℓ₁} {∼ : Rel A ℓ₂} where
                       IsDecPartialOrder (≈ on f) (∼ on f)
   isDecPartialOrder dpo = record
     { isPartialOrder = isPartialOrder DPO.isPartialOrder
-    ; _≟_            = decidable f _ DPO._≈?_
+    ; _≈?_           = decidable f _ DPO._≈?_
     ; _≤?_           = decidable f _ DPO._≤?_
     } where module DPO = IsDecPartialOrder dpo
 
@@ -147,7 +147,7 @@ module _ (f : B → A) {≈ : Rel A ℓ₁} {∼ : Rel A ℓ₂} where
                     IsDecTotalOrder (≈ on f) (∼ on f)
   isDecTotalOrder dec = record
     { isTotalOrder = isTotalOrder Dec.isTotalOrder
-    ; _≟_          = decidable f ≈ Dec._≈?_
+    ; _≈?_         = decidable f ≈ Dec._≈?_
     ; _≤?_         = decidable f ∼ Dec._≤?_
     } where module Dec = IsDecTotalOrder dec
 
diff --git a/src/Relation/Binary/Construct/StrictToNonStrict.agda b/src/Relation/Binary/Construct/StrictToNonStrict.agda
index 0597594c6a..b8b3f13067 100644
--- a/src/Relation/Binary/Construct/StrictToNonStrict.agda
+++ b/src/Relation/Binary/Construct/StrictToNonStrict.agda
@@ -145,7 +145,7 @@ isTotalOrder STO = record
 isDecTotalOrder : IsStrictTotalOrder _≈_ _<_ → IsDecTotalOrder _≈_ _≤_
 isDecTotalOrder STO = record
   { isTotalOrder = isTotalOrder STO
-  ; _≟_          = S._≈?_
+  ; _≈?_         = S._≈?_
   ; _≤?_         = decidable′ S.compare
   }
   where module S = IsStrictTotalOrder STO
diff --git a/src/Relation/Binary/HeterogeneousEquality.agda b/src/Relation/Binary/HeterogeneousEquality.agda
index 59785c7857..1be883007c 100644
--- a/src/Relation/Binary/HeterogeneousEquality.agda
+++ b/src/Relation/Binary/HeterogeneousEquality.agda
@@ -198,7 +198,7 @@ decSetoid dec = record
   { _≈_              = λ x y → x ≅ y
   ; isDecEquivalence = record
       { isEquivalence = isEquivalence
-      ; _≟_            = dec
+      ; _≈?_           = dec
       }
   }
 
diff --git a/src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda b/src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda
index 0f878a752c..a07a8c08e9 100644
--- a/src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda
+++ b/src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda
@@ -37,7 +37,7 @@ isDecEquivalence : ∀ {_≈_ : IRel Aᵢ ℓ} → IsIndexedDecEquivalence Aᵢ
                    (index : I) → IsDecEquivalence (_≈_ {index})
 isDecEquivalence isEq index = record
   { isEquivalence = isEquivalence E.isEquivalenceᵢ index
-  ; _≟_            = E._≈ᵢ?_
+  ; _≈?_           = E._≈ᵢ?_
   } where module E = IsIndexedDecEquivalence isEq
 
 isPreorder : ∀ {_≈_ : IRel Aᵢ ℓ₁} {_∼_ : IRel Aᵢ ℓ₂} →
diff --git a/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda b/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda
index d64f2c50b1..289a1ee91f 100644
--- a/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda
+++ b/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda
@@ -121,6 +121,6 @@ dualMeetSemilattice = record
 ≈-dec⇒isDecPartialOrder : Decidable _≈_ → IsDecPartialOrder _≈_ _≤_
 ≈-dec⇒isDecPartialOrder _≈?_ = record
   { isPartialOrder = isPartialOrder
-  ; _≟_            = _≈?_
+  ; _≈?_           = _≈?_
   ; _≤?_           = ≈-dec⇒≤-dec _≈?_
   }
diff --git a/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda b/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda
index aead77f0da..81a0b64227 100644
--- a/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda
+++ b/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda
@@ -54,6 +54,6 @@ open J dualJoinSemilattice public
 ≈-dec⇒isDecPartialOrder : Decidable _≈_ → IsDecPartialOrder _≈_ _≤_
 ≈-dec⇒isDecPartialOrder _≈?_ = record
   { isPartialOrder = isPartialOrder
-  ; _≟_            = _≈?_
+  ; _≈?_           = _≈?_
   ; _≤?_           = ≈-dec⇒≤-dec _≈?_
   }
diff --git a/src/Relation/Binary/Morphism/OrderMonomorphism.agda b/src/Relation/Binary/Morphism/OrderMonomorphism.agda
index 94e4698035..008b8bf2a8 100644
--- a/src/Relation/Binary/Morphism/OrderMonomorphism.agda
+++ b/src/Relation/Binary/Morphism/OrderMonomorphism.agda
@@ -92,7 +92,7 @@ isTotalOrder O = record
 isDecTotalOrder : IsDecTotalOrder _≈₂_ _≲₂_ → IsDecTotalOrder _≈₁_ _≲₁_
 isDecTotalOrder O = record
   { isTotalOrder = isTotalOrder O.isTotalOrder
-  ; _≟_          = EqM.dec O._≈?_
+  ; _≈?_         = EqM.dec O._≈?_
   ; _≤?_         = dec O._≤?_
   } where module O = IsDecTotalOrder O
 
diff --git a/src/Relation/Binary/Morphism/RelMonomorphism.agda b/src/Relation/Binary/Morphism/RelMonomorphism.agda
index e4e641f712..6727801690 100644
--- a/src/Relation/Binary/Morphism/RelMonomorphism.agda
+++ b/src/Relation/Binary/Morphism/RelMonomorphism.agda
@@ -61,5 +61,5 @@ isEquivalence isEq = record
 isDecEquivalence : IsDecEquivalence _∼₂_ → IsDecEquivalence _∼₁_
 isDecEquivalence isDecEq = record
   { isEquivalence  = isEquivalence E.isEquivalence
-  ; _≟_            = dec E._≈?_
+  ; _≈?_           = dec E._≈?_
   } where module E = IsDecEquivalence isDecEq
diff --git a/src/Relation/Binary/Properties/Poset.agda b/src/Relation/Binary/Properties/Poset.agda
index 1087c5306e..8c96473614 100644
--- a/src/Relation/Binary/Properties/Poset.agda
+++ b/src/Relation/Binary/Properties/Poset.agda
@@ -114,7 +114,7 @@ open StrictPartialOrder <-strictPartialOrder public
 ≤-dec⇒isDecPartialOrder : Decidable _≤_ → IsDecPartialOrder _≈_ _≤_
 ≤-dec⇒isDecPartialOrder _≤?_ = record
   { isPartialOrder = isPartialOrder
-  ; _≟_            = ≤-dec⇒≈-dec _≤?_
+  ; _≈?_           = ≤-dec⇒≈-dec _≤?_
   ; _≤?_           = _≤?_
   }
 
diff --git a/src/Relation/Binary/Properties/TotalOrder.agda b/src/Relation/Binary/Properties/TotalOrder.agda
index b2df3d9a38..de7984a4ef 100644
--- a/src/Relation/Binary/Properties/TotalOrder.agda
+++ b/src/Relation/Binary/Properties/TotalOrder.agda
@@ -30,7 +30,7 @@ decTotalOrder : Decidable _≈_ → DecTotalOrder _ _ _
 decTotalOrder ≈? = record
   { isDecTotalOrder = record
     { isTotalOrder = isTotalOrder
-    ; _≟_          = ≈?
+    ; _≈?_         = ≈?
     ; _≤?_         = total∧dec⇒dec reflexive antisym total ≈?
     }
   }
diff --git a/src/Relation/Binary/PropositionalEquality/Properties.agda b/src/Relation/Binary/PropositionalEquality/Properties.agda
index df0d1d59aa..3e0d897d7a 100644
--- a/src/Relation/Binary/PropositionalEquality/Properties.agda
+++ b/src/Relation/Binary/PropositionalEquality/Properties.agda
@@ -161,7 +161,7 @@ isEquivalence = record
 isDecEquivalence : DecidableEquality A → IsDecEquivalence _≡_
 isDecEquivalence _≈?_ = record
   { isEquivalence = isEquivalence
-  ; _≟_           = _≈?_
+  ; _≈?_          = _≈?_
   }
 
 setoid : Set a → Setoid _ _
diff --git a/src/Relation/Binary/Structures.agda b/src/Relation/Binary/Structures.agda
index 0bf02c900b..761a25382a 100644
--- a/src/Relation/Binary/Structures.agda
+++ b/src/Relation/Binary/Structures.agda
@@ -65,20 +65,15 @@ record IsDecEquivalence : Set (a ⊔ ℓ) where
   infix 4 _≈?_ _≟_
   field
     isEquivalence : IsEquivalence
-    _≟_           : Decidable _≈_
+    _≈?_          : Decidable _≈_
 
   open IsEquivalence isEquivalence public
 
-  -- v2.4: establish new name for public re-export and use
-  _≈?_ = _≟_
-  -- v3.0: change field name and export old name, now deprecated
-  {-
   _≟_ = _≈?_
   {-# WARNING_ON_USAGE _≟_
-  "Warning: _≟_ was deprecated in v3.0.
+  "Warning: _≟_ was deprecated in v2.4.
   Please use _≈?_ instead. "
   #-}
-  -}
 
 ------------------------------------------------------------------------
 -- Preorders
@@ -133,7 +128,7 @@ record IsTotalPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
 record IsDecPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
   field
     isPreorder : IsPreorder _≲_
-    _≟_        : Decidable _≈_
+    _≈?_       : Decidable _≈_
     _≲?_       : Decidable _≲_
 
   open IsPreorder isPreorder public
@@ -144,13 +139,13 @@ record IsDecPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
     isDecEquivalence : IsDecEquivalence
     isDecEquivalence = record
       { isEquivalence = isEquivalence
-      ; _≟_           = _≟_
+      ; _≈?_          = _≈?_
       }
 
     open IsDecEquivalence isDecEquivalence public
-      hiding (_≟_)
+      hiding (_≈?_)
 
-  open Eq public using (_≈?_)
+  open Eq public using (_≟_)
 
 
 ------------------------------------------------------------------------
@@ -171,10 +166,10 @@ record IsPartialOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
 
 
 record IsDecPartialOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
-  infix 4 _≟_ _≤?_
+  infix 4 _≈?_ _≤?_
   field
     isPartialOrder : IsPartialOrder _≤_
-    _≟_            : Decidable _≈_
+    _≈?_           : Decidable _≈_
     _≤?_           : Decidable _≤_
 
   open IsPartialOrder isPartialOrder public
@@ -183,14 +178,14 @@ record IsDecPartialOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) whe
   isDecPreorder : IsDecPreorder _≤_
   isDecPreorder = record
     { isPreorder = isPreorder
-    ; _≟_  = _≟_
+    ; _≈?_ = _≈?_
     ; _≲?_ = _≤?_
     }
 
   open IsDecPreorder isDecPreorder public
     using (module Eq)
 
-  open Eq public using (_≈?_)
+  open Eq public using (_≟_)
 
 
 record IsStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
@@ -213,10 +208,10 @@ record IsStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) wh
 
 
 record IsDecStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
-  infix 4 _≟_ _<?_
+  infix 4 _≈?_ _<?_
   field
     isStrictPartialOrder : IsStrictPartialOrder _<_
-    _≟_                  : Decidable _≈_
+    _≈?_                 : Decidable _≈_
     _<?_                 : Decidable _<_
 
   private
@@ -229,12 +224,12 @@ record IsDecStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂)
     isDecEquivalence : IsDecEquivalence
     isDecEquivalence = record
       { isEquivalence = SPO.isEquivalence
-      ; _≟_           = _≟_
+      ; _≈?_          = _≈?_
       }
 
     open IsDecEquivalence isDecEquivalence public
 
-  open Eq public using (_≈?_)
+  open Eq public using (_≟_)
 
 
 ------------------------------------------------------------------------
@@ -256,10 +251,10 @@ record IsTotalOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
 
 
 record IsDecTotalOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
-  infix 4 _≟_ _≤?_
+  infix 4 _≈?_ _≤?_
   field
     isTotalOrder : IsTotalOrder _≤_
-    _≟_          : Decidable _≈_
+    _≈?_         : Decidable _≈_
     _≤?_         : Decidable _≤_
 
   open IsTotalOrder isTotalOrder public
@@ -268,14 +263,14 @@ record IsDecTotalOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
   isDecPartialOrder : IsDecPartialOrder _≤_
   isDecPartialOrder = record
     { isPartialOrder = isPartialOrder
-    ; _≟_            = _≟_
+    ; _≈?_           = _≈?_
     ; _≤?_           = _≤?_
     }
 
   open IsDecPartialOrder isDecPartialOrder public
     using (isDecPreorder; module Eq)
 
-  open Eq public using (_≈?_)
+  open Eq public using (_≟_)
 
 
 -- Note that these orders are decidable. The current implementation
@@ -304,7 +299,7 @@ record IsStrictTotalOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) wher
   isDecStrictPartialOrder : IsDecStrictPartialOrder _<_
   isDecStrictPartialOrder = record
     { isStrictPartialOrder = isStrictPartialOrder
-    ; _≟_                  = _≈?_
+    ; _≈?_                  = _≈?_
     ; _<?_                 = _<?_
     }
 
@@ -314,17 +309,17 @@ record IsStrictTotalOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) wher
     isDecEquivalence : IsDecEquivalence
     isDecEquivalence = record
       { isEquivalence = isEquivalence
-      ; _≟_           = _≈?_
+      ; _≈?_          = _≈?_
       }
 
     open IsDecEquivalence isDecEquivalence public
 
-  open Eq public hiding (isDecEquivalence; _≈?_)
+  open Eq public using (_≟_)
 
   isDecEquivalence : IsDecEquivalence
   isDecEquivalence = record
-    { isEquivalence = Eq.isEquivalence
-    ; _≟_           = _≈?_
+    { isEquivalence = isEquivalence
+    ; _≈?_          = _≈?_
     }
   {-# WARNING_ON_USAGE isDecEquivalence
   "Warning: isDecEquivalence was deprecated in v2.0.