diff --git a/CHANGELOG.md b/CHANGELOG.md
index f787065436..7975dcc77b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -797,6 +797,23 @@ Non-backwards compatible changes
   IO.Instances
   ```
 
+### (Issue #2096) Introduction of flipped relation symbol for `Relation.Binary.Bundles.Preorder`
+
+* Previously, the relation symbol `_∼_`  was (notationally) symmetric, so that its
+  converse relation could only be discussed *semantically* in terms of `flip _∼_`
+  in `Relation.Binary.Properties.Preorder`, `Relation.Binary.Construct.Flip.{Ord|EqAndOrd}`
+
+* Now, the symbol `_∼_` has been renamed to a new symbol `_≲_`, with `_≳_`
+  introduced as a definition in `Relation.Binary.Bundles.Preorder` whose properties
+  in `Relation.Binary.Properties.Preorder` now refer to it. Partial backwards compatible
+  has been achieved by redeclaring a deprecated version of the old name in the record.
+  Therefore, only _declarations_ of `PartialOrder` records will need their field names
+  updating.
+
+* NB (issues #1214 #2098) the corresponding situation regarding the `flip`ped
+  relation symbols `_≥_`, `_>_` (and their negated versions!) has not (yet)
+  been addressed.
+
 ### Standardisation of `insertAt`/`updateAt`/`removeAt`
 
 * Previously, the names and argument order of index-based insertion, update and removal functions for
@@ -840,7 +857,6 @@ Non-backwards compatible changes
   
 * The old names (and the names of all proofs about these functions) have been deprecated appropriately.
 
-
 ### Changes to triple reasoning interface
 
 * The module `Relation.Binary.Reasoning.Base.Triple` now takes an extra proof that the strict
@@ -1251,6 +1267,11 @@ Deprecated names
   push-function-into-if ↦ if-float
   ```
 
+* In `Data.Container.Related`:
+  ```
+  _∼[_]_  ↦  _≲[_]_
+  ```
+
 * In `Data.Fin.Base`: two new, hopefully more memorable, names `↑ˡ` `↑ʳ`
   for the 'left', resp. 'right' injection of a Fin m into a 'larger' type,
   `Fin (m + n)`, resp. `Fin (n + m)`, with argument order to reflect the
@@ -1661,6 +1682,16 @@ Deprecated names
   fromForeign ↦ Foreign.Haskell.Coerce.coerce
   ```
 
+* In `Relation.Binary.Bundles.Preorder`:
+  ```
+  _∼_  ↦  _≲_
+  ```
+
+* In `Relation.Binary.Indexed.Heterogeneous.Bundles.Preorder`:
+  ```
+  _∼_  ↦  _≲_
+  ```
+
 * In `Relation.Binary.Properties.Preorder`:
   ```
   invIsPreorder ↦ converse-isPreorder
diff --git a/src/Data/Container/Related.agda b/src/Data/Container/Related.agda
index a5af9e334f..1fc9dc5665 100644
--- a/src/Data/Container/Related.agda
+++ b/src/Data/Container/Related.agda
@@ -33,7 +33,23 @@ open Related public
                Setoid (s ⊔ p ⊔ ℓ) (p ⊔ ℓ)
 [ k ]-Equality C X = Related.InducedEquivalence₂ k (_∈_ {C = C} {X = X})
 
-infix 4 _∼[_]_
-_∼[_]_ : ∀ {s p x} {C : Container s p} {X : Set x} →
+infix 4 _≲[_]_
+_≲[_]_ : ∀ {s p x} {C : Container s p} {X : Set x} →
          ⟦ C ⟧ X → Kind → ⟦ C ⟧ X → Set (p ⊔ x)
-_∼[_]_ {C = C} {X} xs k ys = Preorder._∼_ ([ k ]-Order C X) xs ys
+_≲[_]_ {C = C} {X} xs k ys = Preorder._≲_ ([ k ]-Order C X) xs ys
+
+
+
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+infix 4 _∼[_]_
+_∼[_]_ = _≲[_]_
+{-# WARNING_ON_USAGE _∼[_]_
+"Warning: _∼[_]_ was deprecated in v2.0. Please use _≲[_]_ instead. "
+#-}
diff --git a/src/Data/Container/Relation/Unary/Any/Properties.agda b/src/Data/Container/Relation/Unary/Any/Properties.agda
index 7bf97642a4..d3265acefb 100644
--- a/src/Data/Container/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Container/Relation/Unary/Any/Properties.agda
@@ -64,7 +64,7 @@ module _ {s p} {C : Container s p} {x} {X : Set x}
 -- ◇ is a congruence for bag and set equality and related preorders.
 
   cong : ∀ {k} {xs₁ xs₂ : ⟦ C ⟧ X} →
-         (∀ x → Related k (P₁ x) (P₂ x)) → xs₁ ∼[ k ] xs₂ →
+         (∀ x → Related k (P₁ x) (P₂ x)) → xs₁ ≲[ k ] xs₂ →
          Related k (◇ C P₁ xs₁) (◇ C P₂ xs₂)
   cong {k} {xs₁} {xs₂} P₁↔P₂ xs₁≈xs₂ =
     ◇ C P₁ xs₁               ↔⟨ ↔∈ C ⟩
@@ -185,8 +185,8 @@ module _ {s p} (C : Container s p) {x y} {X : Set x} {Y : Set y}
          {ℓ} (P : Pred Y ℓ) where
 
   map-cong : ∀ {k} {f₁ f₂ : X → Y} {xs₁ xs₂ : ⟦ C ⟧ X} →
-             f₁ ≗ f₂ → xs₁ ∼[ k ] xs₂ →
-             map f₁ xs₁ ∼[ k ] map f₂ xs₂
+             f₁ ≗ f₂ → xs₁ ≲[ k ] xs₂ →
+             map f₁ xs₁ ≲[ k ] map f₂ xs₂
   map-cong {f₁ = f₁} {f₂} {xs₁} {xs₂} f₁≗f₂ xs₁≈xs₂ {x} =
     x ∈ map f₁ xs₁           ↔⟨ map↔∘ C (_≡_ x) f₁ ⟩
     ◇ C (λ y → x ≡ f₁ y) xs₁ ∼⟨ cong (Related.↔⇒ ∘ helper) xs₁≈xs₂ ⟩
@@ -286,7 +286,7 @@ module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s
 
 module _ {s p} {C : Container s p} {x} {X : Set x} where
 
-  linear-identity : ∀ {xs : ⟦ C ⟧ X} (m : C ⊸ C) → ⟪ m ⟫⊸ xs ∼[ bag ] xs
+  linear-identity : ∀ {xs : ⟦ C ⟧ X} (m : C ⊸ C) → ⟪ m ⟫⊸ xs ≲[ bag ] xs
   linear-identity {xs} m {x} =
     x ∈ ⟪ m ⟫⊸ xs  ↔⟨ remove-linear (_≡_ x) m ⟩
     x ∈        xs  ∎
diff --git a/src/Data/List/Relation/Binary/BagAndSetEquality.agda b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
index 982f018367..889efe96d9 100644
--- a/src/Data/List/Relation/Binary/BagAndSetEquality.agda
+++ b/src/Data/List/Relation/Binary/BagAndSetEquality.agda
@@ -72,8 +72,8 @@ open Related public using (Kind; SymmetricKind) renaming
 
 infix 4 _∼[_]_
 
-_∼[_]_ : List A → Kind → List A → Set _
-_∼[_]_ {A = A} xs k ys = Preorder._∼_ ([ k ]-Order A) xs ys
+_∼[_]_ : ∀ {a} {A : Set a} → List A → Kind → List A → Set _
+_∼[_]_ {A = A} xs k ys = Preorder._≲_ ([ k ]-Order A) xs ys
 
 private
   module Eq  {k a} {A : Set a} = Setoid ([ k ]-Equality A)
diff --git a/src/Effect/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda
index ed0e3efbc1..44cf13464d 100644
--- a/src/Effect/Monad/Partiality.agda
+++ b/src/Effect/Monad/Partiality.agda
@@ -301,7 +301,7 @@ module _ {A : Set a} {_∼_ : A → A → Set ℓ} where
   preorder pre k = record
     { Carrier    = A ⊥
     ; _≈_        = _≡_
-    ; _∼_        = Rel k
+    ; _≲_        = Rel k
     ; isPreorder = record
       { isEquivalence = P.isEquivalence
       ; reflexive     = refl′
diff --git a/src/Function/Related.agda b/src/Function/Related.agda
index ce67d9580b..9846b4d034 100644
--- a/src/Function/Related.agda
+++ b/src/Function/Related.agda
@@ -404,7 +404,7 @@ InducedPreorder₁ : Kind → ∀ {a s} {A : Set a} →
                    (A → Set s) → Preorder _ _ _
 InducedPreorder₁ k S = record
   { _≈_        = _≡_
-  ; _∼_        = InducedRelation₁ k S
+  ; _≲_        = InducedRelation₁ k S
   ; isPreorder = record
     { isEquivalence = P.isEquivalence
     ; reflexive     = reflexive ∘
@@ -437,7 +437,7 @@ InducedPreorder₂ : Kind → ∀ {a b s} {A : Set a} {B : Set b} →
                    (A → B → Set s) → Preorder _ _ _
 InducedPreorder₂ k _S_ = record
   { _≈_        = _≡_
-  ; _∼_        = InducedRelation₂ k _S_
+  ; _≲_        = InducedRelation₂ k _S_
   ; isPreorder = record
     { isEquivalence = P.isEquivalence
     ; reflexive     = λ x≡y {z} →
diff --git a/src/Function/Related/Propositional.agda b/src/Function/Related/Propositional.agda
index 2eb6aa91c9..ad6054af46 100644
--- a/src/Function/Related/Propositional.agda
+++ b/src/Function/Related/Propositional.agda
@@ -339,7 +339,7 @@ InducedRelation₁ k P = λ x y → P x ∼[ k ] P y
 InducedPreorder₁ : Kind → (P : A → Set p) → Preorder _ _ _
 InducedPreorder₁ k P = record
   { _≈_        = _≡_
-  ; _∼_        = InducedRelation₁ k P
+  ; _≲_        = InducedRelation₁ k P
   ; isPreorder = record
     { isEquivalence = P.isEquivalence
     ; reflexive     = reflexive ∘
@@ -369,7 +369,7 @@ InducedRelation₂ k _S_ = λ x y → ∀ {z} → (z S x) ∼[ k ] (z S y)
 InducedPreorder₂ : Kind → ∀ {s} → (A → B → Set s) → Preorder _ _ _
 InducedPreorder₂ k _S_ = record
   { _≈_        = _≡_
-  ; _∼_        = InducedRelation₂ k _S_
+  ; _≲_        = InducedRelation₂ k _S_
   ; isPreorder = record
     { isEquivalence = P.isEquivalence
     ; reflexive     = λ x≡y {z} →
diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda
index a774d45d69..968cb78b2e 100644
--- a/src/Relation/Binary/Bundles.agda
+++ b/src/Relation/Binary/Bundles.agda
@@ -10,6 +10,7 @@
 
 module Relation.Binary.Bundles where
 
+open import Function.Base using (flip)
 open import Level
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Binary.Core
@@ -73,12 +74,12 @@ record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where
 ------------------------------------------------------------------------
 
 record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
-  infix 4 _≈_ _∼_
+  infix 4 _≈_ _≲_
   field
     Carrier    : Set c
     _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
-    _∼_        : Rel Carrier ℓ₂  -- The relation.
-    isPreorder : IsPreorder _≈_ _∼_
+    _≲_        : Rel Carrier ℓ₂  -- The relation.
+    isPreorder : IsPreorder _≈_ _≲_
 
   open IsPreorder isPreorder public
     hiding (module Eq)
@@ -91,6 +92,12 @@ record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
 
     open Setoid setoid public
 
+  infix 4 _≳_
+  _≳_ = flip _≲_
+
+  infix 4 _∼_ -- for deprecation
+  _∼_ = _≲_
+
 
 record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix 4 _≈_ _≲_
@@ -107,7 +114,7 @@ record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   preorder = record { isPreorder = isPreorder }
 
   open Preorder preorder public
-    using (module Eq)
+    using (module Eq; _≳_)
 
 
 ------------------------------------------------------------------------
@@ -331,3 +338,18 @@ record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) w
     isApartnessRelation : IsApartnessRelation _≈_ _#_
 
   open IsApartnessRelation isApartnessRelation public
+
+
+
+
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+{-# WARNING_ON_USAGE Preorder._∼_
+"Warning: Preorder._∼_ was deprecated in v2.0. Please use Preorder._≲_ instead. "
+#-}
diff --git a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda
index b2c173c190..f3912de253 100644
--- a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda
+++ b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda
@@ -104,7 +104,7 @@ module _ {i t} {I : Set i} (T : Rel I t) where
   preorder : Preorder _ _ _
   preorder = record
     { _≈_        = _≡_
-    ; _∼_        = Star T
+    ; _≲_        = Star T
     ; isPreorder = isPreorder
     }
 
diff --git a/src/Relation/Binary/HeterogeneousEquality.agda b/src/Relation/Binary/HeterogeneousEquality.agda
index 8c7d26cb2a..fc073add44 100644
--- a/src/Relation/Binary/HeterogeneousEquality.agda
+++ b/src/Relation/Binary/HeterogeneousEquality.agda
@@ -219,7 +219,7 @@ preorder : Set ℓ → Preorder ℓ ℓ ℓ
 preorder A = record
   { Carrier    = A
   ; _≈_        = _≡_
-  ; _∼_        = λ x y → x ≅ y
+  ; _≲_        = λ x y → x ≅ y
   ; isPreorder = isPreorder-≡
   }
 
diff --git a/src/Relation/Binary/Indexed/Heterogeneous/Bundles.agda b/src/Relation/Binary/Indexed/Heterogeneous/Bundles.agda
index 86dc3ccdaa..29d4db5253 100644
--- a/src/Relation/Binary/Indexed/Heterogeneous/Bundles.agda
+++ b/src/Relation/Binary/Indexed/Heterogeneous/Bundles.agda
@@ -33,11 +33,28 @@ record IndexedSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
 
 record IndexedPreorder {i} (I : Set i) c ℓ₁ ℓ₂ :
                        Set (suc (i ⊔ c ⊔ ℓ₁ ⊔ ℓ₂)) where
-  infix 4 _≈_ _∼_
+  infix 4 _≈_ _≲_
   field
     Carrier    : I → Set c
     _≈_        : IRel Carrier ℓ₁  -- The underlying equality.
-    _∼_        : IRel Carrier ℓ₂  -- The relation.
-    isPreorder : IsIndexedPreorder Carrier _≈_ _∼_
+    _≲_        : IRel Carrier ℓ₂  -- The relation.
+    isPreorder : IsIndexedPreorder Carrier _≈_ _≲_
 
   open IsIndexedPreorder isPreorder public
+
+  infix 4 _∼_
+  _∼_ = _≲_
+
+
+
+------------------------------------------------------------------------
+-- DEPRECATED
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.0
+
+{-# WARNING_ON_USAGE IndexedPreorder._∼_
+"Warning: IndexedPreorder._∼_ was deprecated in v2.0. Please use IndexedPreorder._≲_ instead. "
+#-}
diff --git a/src/Relation/Binary/Indexed/Heterogeneous/Construct/At.agda b/src/Relation/Binary/Indexed/Heterogeneous/Construct/At.agda
index 2bd79000e8..441ef849bc 100644
--- a/src/Relation/Binary/Indexed/Heterogeneous/Construct/At.agda
+++ b/src/Relation/Binary/Indexed/Heterogeneous/Construct/At.agda
@@ -27,9 +27,9 @@ module _ {a i} {I : Set i} {A : I → Set a} where
     }
     where open IsIndexedEquivalence isEq
 
-  isPreorder : ∀ {ℓ₁ ℓ₂} {_≈_ : IRel A ℓ₁} {_∼_ : IRel A ℓ₂} →
-               IsIndexedPreorder A _≈_ _∼_ →
-               (index : I) → IsPreorder (_≈_ {index}) _∼_
+  isPreorder : ∀ {ℓ₁ ℓ₂} {_≈_ : IRel A ℓ₁} {_≲_ : IRel A ℓ₂} →
+               IsIndexedPreorder A _≈_ _≲_ →
+               (index : I) → IsPreorder (_≈_ {index}) _≲_
   isPreorder isPreorder index = record
     { isEquivalence = isEquivalence O.isEquivalence index
     ; reflexive     = O.reflexive
@@ -54,7 +54,7 @@ module _ {a i} {I : Set i} where
   preorder O index = record
     { Carrier    = O.Carrier index
     ; _≈_        = O._≈_
-    ; _∼_        = O._∼_
+    ; _≲_        = O._≲_
     ; isPreorder = isPreorder O.isPreorder index
     }
     where module O = IndexedPreorder O
diff --git a/src/Relation/Binary/Indexed/Heterogeneous/Structures.agda b/src/Relation/Binary/Indexed/Heterogeneous/Structures.agda
index 7e27aab07f..4569ef2fb0 100644
--- a/src/Relation/Binary/Indexed/Heterogeneous/Structures.agda
+++ b/src/Relation/Binary/Indexed/Heterogeneous/Structures.agda
@@ -34,13 +34,13 @@ record IsIndexedEquivalence : Set (i ⊔ a ⊔ ℓ) where
   reflexive P.refl = refl
 
 
-record IsIndexedPreorder {ℓ₂} (_∼_ : IRel A ℓ₂) : Set (i ⊔ a ⊔ ℓ ⊔ ℓ₂) where
+record IsIndexedPreorder {ℓ₂} (_≲_ : IRel A ℓ₂) : Set (i ⊔ a ⊔ ℓ ⊔ ℓ₂) where
   field
     isEquivalence : IsIndexedEquivalence
-    reflexive     : ∀ {i j} → (_≈_ {i} {j}) ⟨ _⇒_ ⟩ _∼_
-    trans         : Transitive A _∼_
+    reflexive     : ∀ {i j} → (_≈_ {i} {j}) ⟨ _⇒_ ⟩ _≲_
+    trans         : Transitive A _≲_
 
   module Eq = IsIndexedEquivalence isEquivalence
 
-  refl : Reflexive A _∼_
+  refl : Reflexive A _≲_
   refl = reflexive Eq.refl
diff --git a/src/Relation/Binary/Morphism/Bundles.agda b/src/Relation/Binary/Morphism/Bundles.agda
index e8c1c84041..8cd52d3341 100644
--- a/src/Relation/Binary/Morphism/Bundles.agda
+++ b/src/Relation/Binary/Morphism/Bundles.agda
@@ -70,7 +70,7 @@ record PreorderHomomorphism (S₁ : Preorder ℓ₁ ℓ₂ ℓ₃)
   open Preorder
   field
     ⟦_⟧                 : Carrier S₁ → Carrier S₂
-    isOrderHomomorphism : IsOrderHomomorphism (_≈_ S₁) (_≈_ S₂) (_∼_ S₁) (_∼_ S₂) ⟦_⟧
+    isOrderHomomorphism : IsOrderHomomorphism (_≈_ S₁) (_≈_ S₂) (_≲_ S₁) (_≲_ S₂) ⟦_⟧
 
   open IsOrderHomomorphism isOrderHomomorphism public
 
diff --git a/src/Relation/Binary/Morphism/OrderMonomorphism.agda b/src/Relation/Binary/Morphism/OrderMonomorphism.agda
index 49d7c4e2e3..ca3ce3677a 100644
--- a/src/Relation/Binary/Morphism/OrderMonomorphism.agda
+++ b/src/Relation/Binary/Morphism/OrderMonomorphism.agda
@@ -23,9 +23,9 @@ import Relation.Binary.Morphism.RelMonomorphism as RawRelation
 module Relation.Binary.Morphism.OrderMonomorphism
   {a b ℓ₁ ℓ₂ ℓ₃ ℓ₄} {A : Set a} {B : Set b}
   {_≈₁_ : Rel A ℓ₁} {_≈₂_ : Rel B ℓ₃}
-  {_∼₁_ : Rel A ℓ₂} {_∼₂_ : Rel B ℓ₄}
+  {_≲₁_ : Rel A ℓ₂} {_≲₂_ : Rel B ℓ₄}
   {⟦_⟧ : A → B}
-  (isOrderMonomorphism : IsOrderMonomorphism _≈₁_ _≈₂_ _∼₁_ _∼₂_ ⟦_⟧)
+  (isOrderMonomorphism : IsOrderMonomorphism _≈₁_ _≈₂_ _≲₁_ _≲₂_ ⟦_⟧)
   where
 
 open IsOrderMonomorphism isOrderMonomorphism
@@ -40,61 +40,61 @@ open RawRelation isRelMonomorphism public
 ------------------------------------------------------------------------
 -- Properties
 
-reflexive : _≈₂_ ⇒ _∼₂_ → _≈₁_ ⇒ _∼₁_
+reflexive : _≈₂_ ⇒ _≲₂_ → _≈₁_ ⇒ _≲₁_
 reflexive refl x≈y = cancel (refl (cong x≈y))
 
-irrefl : Irreflexive _≈₂_ _∼₂_ → Irreflexive _≈₁_ _∼₁_
+irrefl : Irreflexive _≈₂_ _≲₂_ → Irreflexive _≈₁_ _≲₁_
 irrefl irrefl x≈y x∼y = irrefl (cong x≈y) (mono x∼y)
 
-antisym : Antisymmetric _≈₂_ _∼₂_ → Antisymmetric _≈₁_ _∼₁_
+antisym : Antisymmetric _≈₂_ _≲₂_ → Antisymmetric _≈₁_ _≲₁_
 antisym antisym x∼y y∼x = injective (antisym (mono x∼y) (mono y∼x))
 
-compare : Trichotomous _≈₂_ _∼₂_ → Trichotomous _≈₁_ _∼₁_
+compare : Trichotomous _≈₂_ _≲₂_ → Trichotomous _≈₁_ _≲₁_
 compare compare x y with compare ⟦ x ⟧ ⟦ y ⟧
 ... | tri< a ¬b ¬c = tri< (cancel a) (¬b ∘ cong) (¬c ∘ mono)
 ... | tri≈ ¬a b ¬c = tri≈ (¬a ∘ mono) (injective b) (¬c ∘ mono)
 ... | tri> ¬a ¬b c = tri> (¬a ∘ mono) (¬b ∘ cong) (cancel c)
 
-respˡ : _∼₂_ Respectsˡ _≈₂_ → _∼₁_ Respectsˡ _≈₁_
+respˡ : _≲₂_ Respectsˡ _≈₂_ → _≲₁_ Respectsˡ _≈₁_
 respˡ resp x≈y x∼z = cancel (resp (cong x≈y) (mono x∼z))
 
-respʳ : _∼₂_ Respectsʳ _≈₂_ → _∼₁_ Respectsʳ _≈₁_
+respʳ : _≲₂_ Respectsʳ _≈₂_ → _≲₁_ Respectsʳ _≈₁_
 respʳ resp x≈y y∼z = cancel (resp (cong x≈y) (mono y∼z))
 
-resp : _∼₂_ Respects₂ _≈₂_ → _∼₁_ Respects₂ _≈₁_
+resp : _≲₂_ Respects₂ _≈₂_ → _≲₁_ Respects₂ _≈₁_
 resp = map respʳ respˡ
 
 ------------------------------------------------------------------------
 -- Structures
 
-isPreorder : IsPreorder _≈₂_ _∼₂_ → IsPreorder _≈₁_ _∼₁_
+isPreorder : IsPreorder _≈₂_ _≲₂_ → IsPreorder _≈₁_ _≲₁_
 isPreorder O = record
   { isEquivalence = EqM.isEquivalence O.isEquivalence
   ; reflexive     = reflexive O.reflexive
   ; trans         = trans O.trans
   } where module O = IsPreorder O
 
-isPartialOrder : IsPartialOrder _≈₂_ _∼₂_ → IsPartialOrder _≈₁_ _∼₁_
+isPartialOrder : IsPartialOrder _≈₂_ _≲₂_ → IsPartialOrder _≈₁_ _≲₁_
 isPartialOrder O = record
   { isPreorder = isPreorder O.isPreorder
   ; antisym    = antisym O.antisym
   } where module O = IsPartialOrder O
 
-isTotalOrder : IsTotalOrder _≈₂_ _∼₂_ → IsTotalOrder _≈₁_ _∼₁_
+isTotalOrder : IsTotalOrder _≈₂_ _≲₂_ → IsTotalOrder _≈₁_ _≲₁_
 isTotalOrder O = record
   { isPartialOrder = isPartialOrder O.isPartialOrder
   ; total          = total O.total
   } where module O = IsTotalOrder O
 
-isDecTotalOrder : IsDecTotalOrder _≈₂_ _∼₂_ → IsDecTotalOrder _≈₁_ _∼₁_
+isDecTotalOrder : IsDecTotalOrder _≈₂_ _≲₂_ → IsDecTotalOrder _≈₁_ _≲₁_
 isDecTotalOrder O = record
   { isTotalOrder = isTotalOrder O.isTotalOrder
   ; _≟_          = EqM.dec O._≟_
   ; _≤?_         = dec O._≤?_
   } where module O = IsDecTotalOrder O
 
-isStrictPartialOrder : IsStrictPartialOrder _≈₂_ _∼₂_ →
-                       IsStrictPartialOrder _≈₁_ _∼₁_
+isStrictPartialOrder : IsStrictPartialOrder _≈₂_ _≲₂_ →
+                       IsStrictPartialOrder _≈₁_ _≲₁_
 isStrictPartialOrder O = record
   { isEquivalence = EqM.isEquivalence O.isEquivalence
   ; irrefl        = irrefl O.irrefl
@@ -102,8 +102,8 @@ isStrictPartialOrder O = record
   ; <-resp-≈      = resp O.<-resp-≈
   } where module O = IsStrictPartialOrder O
 
-isStrictTotalOrder : IsStrictTotalOrder _≈₂_ _∼₂_ →
-                     IsStrictTotalOrder _≈₁_ _∼₁_
+isStrictTotalOrder : IsStrictTotalOrder _≈₂_ _≲₂_ →
+                     IsStrictTotalOrder _≈₁_ _≲₁_
 isStrictTotalOrder O = record
   { isEquivalence = EqM.isEquivalence O.isEquivalence
   ; trans         = trans O.trans
diff --git a/src/Relation/Binary/Morphism/Structures.agda b/src/Relation/Binary/Morphism/Structures.agda
index 86eceac6e4..081008fbd1 100644
--- a/src/Relation/Binary/Morphism/Structures.agda
+++ b/src/Relation/Binary/Morphism/Structures.agda
@@ -57,29 +57,29 @@ record IsRelIsomorphism (_∼₁_ : Rel A ℓ₁) (_∼₂_ : Rel B ℓ₂)
 ------------------------------------------------------------------------
 
 record IsOrderHomomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
-                           (_∼₁_ : Rel A ℓ₃) (_∼₂_ : Rel B ℓ₄)
+                           (_≲₁_ : Rel A ℓ₃) (_≲₂_ : Rel B ℓ₄)
                            (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
                            where
   field
     cong  : Homomorphic₂ _≈₁_ _≈₂_ ⟦_⟧
-    mono  : Homomorphic₂ _∼₁_ _∼₂_ ⟦_⟧
+    mono  : Homomorphic₂ _≲₁_ _≲₂_ ⟦_⟧
 
   module Eq where
     isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
     isRelHomomorphism = record { cong = cong }
 
-  isRelHomomorphism : IsRelHomomorphism _∼₁_ _∼₂_ ⟦_⟧
+  isRelHomomorphism : IsRelHomomorphism _≲₁_ _≲₂_ ⟦_⟧
   isRelHomomorphism = record { cong = mono }
 
 
 record IsOrderMonomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
-                           (_∼₁_ : Rel A ℓ₃) (_∼₂_ : Rel B ℓ₄)
+                           (_≲₁_ : Rel A ℓ₃) (_≲₂_ : Rel B ℓ₄)
                            (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
                            where
   field
-    isOrderHomomorphism : IsOrderHomomorphism _≈₁_ _≈₂_ _∼₁_ _∼₂_ ⟦_⟧
+    isOrderHomomorphism : IsOrderHomomorphism _≈₁_ _≈₂_ _≲₁_ _≲₂_ ⟦_⟧
     injective           : Injective _≈₁_ _≈₂_ ⟦_⟧
-    cancel              : Injective _∼₁_ _∼₂_ ⟦_⟧
+    cancel              : Injective _≲₁_ _≲₂_ ⟦_⟧
 
   open IsOrderHomomorphism isOrderHomomorphism public
     hiding (module Eq)
@@ -91,7 +91,7 @@ record IsOrderMonomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
       ; injective      = injective
       }
 
-  isRelMonomorphism : IsRelMonomorphism _∼₁_ _∼₂_ ⟦_⟧
+  isRelMonomorphism : IsRelMonomorphism _≲₁_ _≲₂_ ⟦_⟧
   isRelMonomorphism = record
     { isHomomorphism = isRelHomomorphism
     ; injective      = cancel
@@ -99,11 +99,11 @@ record IsOrderMonomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
 
 
 record IsOrderIsomorphism (_≈₁_ : Rel A ℓ₁) (_≈₂_ : Rel B ℓ₂)
-                          (_∼₁_ : Rel A ℓ₃) (_∼₂_ : Rel B ℓ₄)
+                          (_≲₁_ : Rel A ℓ₃) (_≲₂_ : Rel B ℓ₄)
                           (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄)
                           where
   field
-    isOrderMonomorphism : IsOrderMonomorphism _≈₁_ _≈₂_ _∼₁_ _∼₂_ ⟦_⟧
+    isOrderMonomorphism : IsOrderMonomorphism _≈₁_ _≈₂_ _≲₁_ _≲₂_ ⟦_⟧
     surjective          : Surjective _≈₁_ _≈₂_ ⟦_⟧
 
   open IsOrderMonomorphism isOrderMonomorphism public
diff --git a/src/Relation/Binary/Properties/Preorder.agda b/src/Relation/Binary/Properties/Preorder.agda
index dc9bd2913b..b2be296828 100644
--- a/src/Relation/Binary/Properties/Preorder.agda
+++ b/src/Relation/Binary/Properties/Preorder.agda
@@ -18,10 +18,11 @@ import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
 
 open Preorder P
 
+
 ------------------------------------------------------------------------
--- The inverse relation is also a preorder.
+-- The converse relation is also a preorder.
 
-converse-isPreorder : IsPreorder _≈_ (flip _∼_)
+converse-isPreorder : IsPreorder _≈_ _≳_
 converse-isPreorder = EqAndOrd.isPreorder isPreorder
 
 converse-preorder : Preorder p₁ p₂ p₃
@@ -32,7 +33,7 @@ converse-preorder = EqAndOrd.preorder P
 
 InducedEquivalence : Setoid _ _
 InducedEquivalence = record
-  { _≈_           = λ x y → x ∼ y × y ∼ x
+  { _≈_           = λ x y → x ≲ y × x ≳ y
   ; isEquivalence = record
     { refl  = (refl , refl)
     ; sym   = swap
diff --git a/src/Relation/Binary/Structures.agda b/src/Relation/Binary/Structures.agda
index 5b59e900be..751c774da3 100644
--- a/src/Relation/Binary/Structures.agda
+++ b/src/Relation/Binary/Structures.agda
@@ -73,25 +73,25 @@ record IsDecEquivalence : Set (a ⊔ ℓ) where
 -- Preorders
 ------------------------------------------------------------------------
 
-record IsPreorder (_∼_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+record IsPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
   field
     isEquivalence : IsEquivalence
     -- Reflexivity is expressed in terms of the underlying equality:
-    reflexive     : _≈_ ⇒ _∼_
-    trans         : Transitive _∼_
+    reflexive     : _≈_ ⇒ _≲_
+    trans         : Transitive _≲_
 
   module Eq = IsEquivalence isEquivalence
 
-  refl : Reflexive _∼_
+  refl : Reflexive _≲_
   refl = reflexive Eq.refl
 
-  ∼-respˡ-≈ : _∼_ Respectsˡ _≈_
+  ∼-respˡ-≈ : _≲_ Respectsˡ _≈_
   ∼-respˡ-≈ x≈y x∼z = trans (reflexive (Eq.sym x≈y)) x∼z
 
-  ∼-respʳ-≈ : _∼_ Respectsʳ _≈_
+  ∼-respʳ-≈ : _≲_ Respectsʳ _≈_
   ∼-respʳ-≈ x≈y z∼x = trans z∼x (reflexive x≈y)
 
-  ∼-resp-≈ : _∼_ Respects₂ _≈_
+  ∼-resp-≈ : _≲_ Respects₂ _≈_
   ∼-resp-≈ = ∼-respʳ-≈ , ∼-respˡ-≈