diff --git a/CHANGELOG.md b/CHANGELOG.md
index e33d919313..de9f84ad7b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -889,6 +889,14 @@ Major improvements
 Deprecated modules
 ------------------
 
+### Moving `Relation.Binary.Construct.(Converse/Flip)`
+
+* The following files have been moved:
+  ```agda
+  Relation.Binary.Construct.Converse               ↦ Relation.Binary.Construct.Flip.EqAndOrd
+  Relation.Binary.Construct.Flip                   ↦ Relation.Binary.Construct.Flip.Ord
+  ```
+
 ### Deprecation of old function hierarchy
 
 * The module `Function.Related` has been deprecated in favour of `Function.Related.Propositional`
diff --git a/src/Algebra/Construct/NaturalChoice/Base.agda b/src/Algebra/Construct/NaturalChoice/Base.agda
index 901f7a5413..3ebd9b924f 100644
--- a/src/Algebra/Construct/NaturalChoice/Base.agda
+++ b/src/Algebra/Construct/NaturalChoice/Base.agda
@@ -11,7 +11,7 @@ open import Algebra.Core
 open import Level as L hiding (_⊔_)
 open import Function.Base using (flip)
 open import Relation.Binary
-open import Relation.Binary.Construct.Converse using ()
+open import Relation.Binary.Construct.Flip.EqAndOrd using ()
   renaming (totalPreorder to flipOrder)
 import Relation.Binary.Properties.TotalOrder as TotalOrderProperties
 
diff --git a/src/Algebra/Construct/NaturalChoice/Max.agda b/src/Algebra/Construct/NaturalChoice/Max.agda
index 592b887f6b..212a52602f 100644
--- a/src/Algebra/Construct/NaturalChoice/Max.agda
+++ b/src/Algebra/Construct/NaturalChoice/Max.agda
@@ -14,7 +14,7 @@ module Algebra.Construct.NaturalChoice.Max
 open import Algebra.Core
 open import Algebra.Definitions
 open import Algebra.Construct.NaturalChoice.Base
-open import Relation.Binary.Construct.Converse using ()
+open import Relation.Binary.Construct.Flip.EqAndOrd using ()
   renaming (totalOrder to flip)
 
 open TotalOrder totalOrder renaming (Carrier to A)
diff --git a/src/Algebra/Construct/NaturalChoice/MaxOp.agda b/src/Algebra/Construct/NaturalChoice/MaxOp.agda
index 28accb65b3..d6c7de61ba 100644
--- a/src/Algebra/Construct/NaturalChoice/MaxOp.agda
+++ b/src/Algebra/Construct/NaturalChoice/MaxOp.agda
@@ -12,7 +12,7 @@ open import Algebra.Construct.NaturalChoice.Base
 import Algebra.Construct.NaturalChoice.MinOp as MinOp
 open import Function.Base using (flip)
 open import Relation.Binary
-open import Relation.Binary.Construct.Converse using ()
+open import Relation.Binary.Construct.Flip.EqAndOrd using ()
   renaming (totalPreorder to flipOrder)
 
 module Algebra.Construct.NaturalChoice.MaxOp
diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda
index acd098be75..3c9bf54546 100644
--- a/src/Data/Fin/Induction.agda
+++ b/src/Data/Fin/Induction.agda
@@ -23,8 +23,8 @@ open import Induction.WellFounded as WF
 open import Level using (Level)
 open import Relation.Binary
   using (Rel; Decidable; IsPartialOrder; IsStrictPartialOrder; StrictPartialOrder)
-import Relation.Binary.Construct.Converse as Converse
-import Relation.Binary.Construct.Flip as Flip
+import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
+import Relation.Binary.Construct.Flip.Ord as Ord
 import Relation.Binary.Construct.NonStrictToStrict as ToStrict
 import Relation.Binary.Construct.On as On
 open import Relation.Binary.Definitions using (Tri; tri<; tri≈; tri>)
@@ -123,7 +123,7 @@ module _ {_≈_ : Rel (Fin n) ℓ} where
     pigeon : (xs : Vec (Fin n) n) → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_
     pigeon xs i∷xs↑ =
       let (i₁ , i₂ , i₁<i₂ , xs[i₁]≡xs[i₂]) = pigeonhole (n<1+n n) (Vec.lookup (i ∷ xs)) in
-      let xs[i₁]⊏xs[i₂] = Linkedₚ.lookup⁺ (Flip.transitive _⊏_ ⊏.trans) {xs = i ∷ xs} i∷xs↑ i₁<i₂ in
+      let xs[i₁]⊏xs[i₂] = Linkedₚ.lookup⁺ (Ord.transitive _⊏_ ⊏.trans) {xs = i ∷ xs} i∷xs↑ i₁<i₂ in
       let xs[i₁]⊏xs[i₁] = ⊏.<-respʳ-≈ (⊏.Eq.reflexive xs[i₁]≡xs[i₂]) xs[i₁]⊏xs[i₂] in
       contradiction xs[i₁]⊏xs[i₁] (⊏.irrefl ⊏.Eq.refl)
 
@@ -137,7 +137,7 @@ module _ {_≈_ : Rel (Fin n) ℓ} where
 
   spo-noetherian : ∀ {r} {_⊏_ : Rel (Fin n) r} →
                    IsStrictPartialOrder _≈_ _⊏_ → WellFounded (flip _⊏_)
-  spo-noetherian isSPO = spo-wellFounded (Converse.isStrictPartialOrder isSPO)
+  spo-noetherian isSPO = spo-wellFounded (EqAndOrd.isStrictPartialOrder isSPO)
 
   po-noetherian : ∀ {r} {_⊑_ : Rel (Fin n) r} → IsPartialOrder _≈_ _⊑_ →
                   WellFounded (flip (ToStrict._<_ _≈_ _⊑_))
diff --git a/src/Relation/Binary/Construct/Converse.agda b/src/Relation/Binary/Construct/Converse.agda
index e750283521..c1e2d177a7 100644
--- a/src/Relation/Binary/Construct/Converse.agda
+++ b/src/Relation/Binary/Construct/Converse.agda
@@ -1,195 +1,17 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Many properties which hold for `∼` also hold for `flip ∼`. Unlike
--- the module `Relation.Binary.Construct.Flip` this module does not
--- flip the underlying equality.
+-- This module is DEPRECATED. Please use
+-- `Relation.Binary.Construct.Flip.EqAndOrd` instead.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary
-
 module Relation.Binary.Construct.Converse where
 
-open import Data.Product
-open import Function.Base using (flip; _∘_)
-open import Level using (Level)
-
-private
-  variable
-    a b p ℓ ℓ₁ ℓ₂ : Level
-    A B : Set a
-    ≈ ∼ ≤ < : Rel A ℓ
-
-------------------------------------------------------------------------
--- Properties
-
-module _ (∼ : Rel A ℓ) where
-
-  refl : Reflexive ∼ → Reflexive (flip ∼)
-  refl refl = refl
-
-  sym : Symmetric ∼ → Symmetric (flip ∼)
-  sym sym = sym
-
-  trans : Transitive ∼ → Transitive (flip ∼)
-  trans trans = flip trans
-
-  asym : Asymmetric ∼ → Asymmetric (flip ∼)
-  asym asym = asym
-
-  total : Total ∼ → Total (flip ∼)
-  total total x y = total y x
-
-  resp : ∀ {p} (P : A → Set p) → Symmetric ∼ →
-             P Respects ∼ → P Respects (flip ∼)
-  resp _ sym resp ∼ = resp (sym ∼)
-
-  max : ∀ {⊥} → Minimum ∼ ⊥ → Maximum (flip ∼) ⊥
-  max min = min
-
-  min : ∀ {⊤} → Maximum ∼ ⊤ → Minimum (flip ∼) ⊤
-  min max = max
-
-module _ {≈ : Rel A ℓ₁} (∼ : Rel A ℓ₂) where
-
-  reflexive : Symmetric ≈ → (≈ ⇒ ∼) → (≈ ⇒ flip ∼)
-  reflexive sym impl = impl ∘ sym
-
-  irrefl : Symmetric ≈ → Irreflexive ≈ ∼ → Irreflexive ≈ (flip ∼)
-  irrefl sym irrefl x≈y y∼x = irrefl (sym x≈y) y∼x
-
-  antisym : Antisymmetric ≈ ∼ → Antisymmetric ≈ (flip ∼)
-  antisym antisym = flip antisym
-
-  compare : Trichotomous ≈ ∼ → Trichotomous ≈ (flip ∼)
-  compare cmp x y with cmp x y
-  ... | tri< x<y x≉y y≮x = tri> y≮x x≉y x<y
-  ... | tri≈ x≮y x≈y y≮x = tri≈ y≮x x≈y x≮y
-  ... | tri> x≮y x≉y y<x = tri< y<x x≉y x≮y
-
-module _ (∼₁ : Rel A ℓ₁) (∼₂ : Rel A ℓ₂) where
-
-  resp₂ : ∼₁ Respects₂ ∼₂ → (flip ∼₁) Respects₂ ∼₂
-  resp₂ (resp₁ , resp₂) = resp₂ , resp₁
-
-module _ (∼ : REL A B ℓ) where
-
-  dec : Decidable ∼ → Decidable (flip ∼)
-  dec dec = flip dec
-
-------------------------------------------------------------------------
--- Structures
-
-isEquivalence : IsEquivalence ≈ → IsEquivalence (flip ≈)
-isEquivalence {≈ = ≈} eq = record
-  { refl  = refl  ≈ Eq.refl
-  ; sym   = sym   ≈ Eq.sym
-  ; trans = trans ≈ Eq.trans
-  } where module Eq = IsEquivalence eq
-
-isDecEquivalence : IsDecEquivalence ≈ → IsDecEquivalence (flip ≈)
-isDecEquivalence {≈ = ≈} eq = record
-  { isEquivalence = isEquivalence Dec.isEquivalence
-  ; _≟_           = dec ≈ Dec._≟_
-  } where module Dec = IsDecEquivalence eq
-
-isPreorder : IsPreorder ≈ ∼ → IsPreorder ≈ (flip ∼)
-isPreorder {≈ = ≈} {∼ = ∼} O = record
-  { isEquivalence = O.isEquivalence
-  ; reflexive     = reflexive ∼ O.Eq.sym O.reflexive
-  ; trans         = trans ∼ O.trans
-  } where module O = IsPreorder O
-
-isTotalPreorder : IsTotalPreorder ≈ ∼ → IsTotalPreorder ≈ (flip ∼)
-isTotalPreorder O = record
-  { isPreorder = isPreorder O.isPreorder
-  ; total      = total _ O.total
-  } where module O = IsTotalPreorder O
-
-isPartialOrder : IsPartialOrder ≈ ≤ → IsPartialOrder ≈ (flip ≤)
-isPartialOrder {≤ = ≤} O = record
-  { isPreorder = isPreorder O.isPreorder
-  ; antisym    = antisym ≤ O.antisym
-  } where module O = IsPartialOrder O
-
-isTotalOrder : IsTotalOrder ≈ ≤ → IsTotalOrder ≈ (flip ≤)
-isTotalOrder O = record
-  { isPartialOrder = isPartialOrder O.isPartialOrder
-  ; total          = total _ O.total
-  } where module O = IsTotalOrder O
-
-isDecTotalOrder : IsDecTotalOrder ≈ ≤ → IsDecTotalOrder ≈ (flip ≤)
-isDecTotalOrder O = record
-  { isTotalOrder = isTotalOrder O.isTotalOrder
-  ; _≟_          = O._≟_
-  ; _≤?_         = dec _ O._≤?_
-  } where module O = IsDecTotalOrder O
-
-isStrictPartialOrder : IsStrictPartialOrder ≈ < →
-                       IsStrictPartialOrder ≈ (flip <)
-isStrictPartialOrder {< = <} O = record
-  { isEquivalence = O.isEquivalence
-  ; irrefl        = irrefl < O.Eq.sym O.irrefl
-  ; trans         = trans < O.trans
-  ; <-resp-≈      = resp₂ _ _ O.<-resp-≈
-  } where module O = IsStrictPartialOrder O
-
-isStrictTotalOrder : IsStrictTotalOrder ≈ < →
-                     IsStrictTotalOrder ≈ (flip <)
-isStrictTotalOrder {< = <} O = record
-  { isEquivalence = O.isEquivalence
-  ; trans         = trans < O.trans
-  ; compare       = compare _ O.compare
-  } where module O = IsStrictTotalOrder O
-
-------------------------------------------------------------------------
--- Bundles
-
-setoid : Setoid a ℓ → Setoid a ℓ
-setoid S = record
-  { isEquivalence = isEquivalence S.isEquivalence
-  } where module S = Setoid S
-
-decSetoid : DecSetoid a ℓ → DecSetoid a ℓ
-decSetoid S = record
-  { isDecEquivalence = isDecEquivalence S.isDecEquivalence
-  } where module S = DecSetoid S
-
-preorder : Preorder a ℓ₁ ℓ₂ → Preorder a ℓ₁ ℓ₂
-preorder O = record
-  { isPreorder = isPreorder O.isPreorder
-  } where module O = Preorder O
-
-totalPreorder : TotalPreorder a ℓ₁ ℓ₂ → TotalPreorder a ℓ₁ ℓ₂
-totalPreorder O = record
-  { isTotalPreorder = isTotalPreorder O.isTotalPreorder
-  } where module O = TotalPreorder O
-
-poset : Poset a ℓ₁ ℓ₂ → Poset a ℓ₁ ℓ₂
-poset O = record
-  { isPartialOrder = isPartialOrder O.isPartialOrder
-  } where module O = Poset O
-
-totalOrder : TotalOrder a ℓ₁ ℓ₂ → TotalOrder a ℓ₁ ℓ₂
-totalOrder O = record
-  { isTotalOrder = isTotalOrder O.isTotalOrder
-  } where module O = TotalOrder O
-
-decTotalOrder : DecTotalOrder a ℓ₁ ℓ₂ → DecTotalOrder a ℓ₁ ℓ₂
-decTotalOrder O = record
-  { isDecTotalOrder = isDecTotalOrder O.isDecTotalOrder
-  } where module O = DecTotalOrder O
-
-strictPartialOrder : StrictPartialOrder a ℓ₁ ℓ₂ →
-                     StrictPartialOrder a ℓ₁ ℓ₂
-strictPartialOrder O = record
-  { isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder
-  } where module O = StrictPartialOrder O
+open import Relation.Binary.Construct.Flip.EqAndOrd public
 
-strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂ →
-                   StrictTotalOrder a ℓ₁ ℓ₂
-strictTotalOrder O = record
-  { isStrictTotalOrder = isStrictTotalOrder O.isStrictTotalOrder
-  } where module O = StrictTotalOrder O
+{-# WARNING_ON_IMPORT
+"Relation.Binary.Construct.Converse was deprecated in v2.0.
+Use Relation.Binary.Construct.Flip.EqAndOrd instead."
+#-}
diff --git a/src/Relation/Binary/Construct/Flip.Agda b/src/Relation/Binary/Construct/Flip.Agda
new file mode 100644
index 0000000000..cbae1e8867
--- /dev/null
+++ b/src/Relation/Binary/Construct/Flip.Agda
@@ -0,0 +1,17 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module is DEPRECATED. Please use
+-- `Relation.Binary.Construct.Flip.Ord` instead.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Construct.Flip where
+
+open import Relation.Binary.Construct.Flip.Ord public
+
+{-# WARNING_ON_IMPORT
+"Relation.Binary.Construct.Flip was deprecated in v2.0.
+Use Relation.Binary.Construct.Flip.Ord instead."
+#-}
diff --git a/src/Relation/Binary/Construct/Flip/EqAndOrd.agda b/src/Relation/Binary/Construct/Flip/EqAndOrd.agda
new file mode 100644
index 0000000000..1d3e9430d9
--- /dev/null
+++ b/src/Relation/Binary/Construct/Flip/EqAndOrd.agda
@@ -0,0 +1,195 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Many properties which hold for `∼` also hold for `flip ∼`. Unlike
+-- the module `Relation.Binary.Construct.Flip.Ord` this module does not
+-- flip the underlying equality.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Relation.Binary
+
+module Relation.Binary.Construct.Flip.EqAndOrd where
+
+open import Data.Product
+open import Function.Base using (flip; _∘_)
+open import Level using (Level)
+
+private
+  variable
+    a b p ℓ ℓ₁ ℓ₂ : Level
+    A B : Set a
+    ≈ ∼ ≤ < : Rel A ℓ
+
+------------------------------------------------------------------------
+-- Properties
+
+module _ (∼ : Rel A ℓ) where
+
+  refl : Reflexive ∼ → Reflexive (flip ∼)
+  refl refl = refl
+
+  sym : Symmetric ∼ → Symmetric (flip ∼)
+  sym sym = sym
+
+  trans : Transitive ∼ → Transitive (flip ∼)
+  trans trans = flip trans
+
+  asym : Asymmetric ∼ → Asymmetric (flip ∼)
+  asym asym = asym
+
+  total : Total ∼ → Total (flip ∼)
+  total total x y = total y x
+
+  resp : ∀ {p} (P : A → Set p) → Symmetric ∼ →
+             P Respects ∼ → P Respects (flip ∼)
+  resp _ sym resp ∼ = resp (sym ∼)
+
+  max : ∀ {⊥} → Minimum ∼ ⊥ → Maximum (flip ∼) ⊥
+  max min = min
+
+  min : ∀ {⊤} → Maximum ∼ ⊤ → Minimum (flip ∼) ⊤
+  min max = max
+
+module _ {≈ : Rel A ℓ₁} (∼ : Rel A ℓ₂) where
+
+  reflexive : Symmetric ≈ → (≈ ⇒ ∼) → (≈ ⇒ flip ∼)
+  reflexive sym impl = impl ∘ sym
+
+  irrefl : Symmetric ≈ → Irreflexive ≈ ∼ → Irreflexive ≈ (flip ∼)
+  irrefl sym irrefl x≈y y∼x = irrefl (sym x≈y) y∼x
+
+  antisym : Antisymmetric ≈ ∼ → Antisymmetric ≈ (flip ∼)
+  antisym antisym = flip antisym
+
+  compare : Trichotomous ≈ ∼ → Trichotomous ≈ (flip ∼)
+  compare cmp x y with cmp x y
+  ... | tri< x<y x≉y y≮x = tri> y≮x x≉y x<y
+  ... | tri≈ x≮y x≈y y≮x = tri≈ y≮x x≈y x≮y
+  ... | tri> x≮y x≉y y<x = tri< y<x x≉y x≮y
+
+module _ (∼₁ : Rel A ℓ₁) (∼₂ : Rel A ℓ₂) where
+
+  resp₂ : ∼₁ Respects₂ ∼₂ → (flip ∼₁) Respects₂ ∼₂
+  resp₂ (resp₁ , resp₂) = resp₂ , resp₁
+
+module _ (∼ : REL A B ℓ) where
+
+  dec : Decidable ∼ → Decidable (flip ∼)
+  dec dec = flip dec
+
+------------------------------------------------------------------------
+-- Structures
+
+isEquivalence : IsEquivalence ≈ → IsEquivalence (flip ≈)
+isEquivalence {≈ = ≈} eq = record
+  { refl  = refl  ≈ Eq.refl
+  ; sym   = sym   ≈ Eq.sym
+  ; trans = trans ≈ Eq.trans
+  } where module Eq = IsEquivalence eq
+
+isDecEquivalence : IsDecEquivalence ≈ → IsDecEquivalence (flip ≈)
+isDecEquivalence {≈ = ≈} eq = record
+  { isEquivalence = isEquivalence Dec.isEquivalence
+  ; _≟_           = dec ≈ Dec._≟_
+  } where module Dec = IsDecEquivalence eq
+
+isPreorder : IsPreorder ≈ ∼ → IsPreorder ≈ (flip ∼)
+isPreorder {≈ = ≈} {∼ = ∼} O = record
+  { isEquivalence = O.isEquivalence
+  ; reflexive     = reflexive ∼ O.Eq.sym O.reflexive
+  ; trans         = trans ∼ O.trans
+  } where module O = IsPreorder O
+
+isTotalPreorder : IsTotalPreorder ≈ ∼ → IsTotalPreorder ≈ (flip ∼)
+isTotalPreorder O = record
+  { isPreorder = isPreorder O.isPreorder
+  ; total      = total _ O.total
+  } where module O = IsTotalPreorder O
+
+isPartialOrder : IsPartialOrder ≈ ≤ → IsPartialOrder ≈ (flip ≤)
+isPartialOrder {≤ = ≤} O = record
+  { isPreorder = isPreorder O.isPreorder
+  ; antisym    = antisym ≤ O.antisym
+  } where module O = IsPartialOrder O
+
+isTotalOrder : IsTotalOrder ≈ ≤ → IsTotalOrder ≈ (flip ≤)
+isTotalOrder O = record
+  { isPartialOrder = isPartialOrder O.isPartialOrder
+  ; total          = total _ O.total
+  } where module O = IsTotalOrder O
+
+isDecTotalOrder : IsDecTotalOrder ≈ ≤ → IsDecTotalOrder ≈ (flip ≤)
+isDecTotalOrder O = record
+  { isTotalOrder = isTotalOrder O.isTotalOrder
+  ; _≟_          = O._≟_
+  ; _≤?_         = dec _ O._≤?_
+  } where module O = IsDecTotalOrder O
+
+isStrictPartialOrder : IsStrictPartialOrder ≈ < →
+                       IsStrictPartialOrder ≈ (flip <)
+isStrictPartialOrder {< = <} O = record
+  { isEquivalence = O.isEquivalence
+  ; irrefl        = irrefl < O.Eq.sym O.irrefl
+  ; trans         = trans < O.trans
+  ; <-resp-≈      = resp₂ _ _ O.<-resp-≈
+  } where module O = IsStrictPartialOrder O
+
+isStrictTotalOrder : IsStrictTotalOrder ≈ < →
+                     IsStrictTotalOrder ≈ (flip <)
+isStrictTotalOrder {< = <} O = record
+  { isEquivalence = O.isEquivalence
+  ; trans         = trans < O.trans
+  ; compare       = compare _ O.compare
+  } where module O = IsStrictTotalOrder O
+
+------------------------------------------------------------------------
+-- Bundles
+
+setoid : Setoid a ℓ → Setoid a ℓ
+setoid S = record
+  { isEquivalence = isEquivalence S.isEquivalence
+  } where module S = Setoid S
+
+decSetoid : DecSetoid a ℓ → DecSetoid a ℓ
+decSetoid S = record
+  { isDecEquivalence = isDecEquivalence S.isDecEquivalence
+  } where module S = DecSetoid S
+
+preorder : Preorder a ℓ₁ ℓ₂ → Preorder a ℓ₁ ℓ₂
+preorder O = record
+  { isPreorder = isPreorder O.isPreorder
+  } where module O = Preorder O
+
+totalPreorder : TotalPreorder a ℓ₁ ℓ₂ → TotalPreorder a ℓ₁ ℓ₂
+totalPreorder O = record
+  { isTotalPreorder = isTotalPreorder O.isTotalPreorder
+  } where module O = TotalPreorder O
+
+poset : Poset a ℓ₁ ℓ₂ → Poset a ℓ₁ ℓ₂
+poset O = record
+  { isPartialOrder = isPartialOrder O.isPartialOrder
+  } where module O = Poset O
+
+totalOrder : TotalOrder a ℓ₁ ℓ₂ → TotalOrder a ℓ₁ ℓ₂
+totalOrder O = record
+  { isTotalOrder = isTotalOrder O.isTotalOrder
+  } where module O = TotalOrder O
+
+decTotalOrder : DecTotalOrder a ℓ₁ ℓ₂ → DecTotalOrder a ℓ₁ ℓ₂
+decTotalOrder O = record
+  { isDecTotalOrder = isDecTotalOrder O.isDecTotalOrder
+  } where module O = DecTotalOrder O
+
+strictPartialOrder : StrictPartialOrder a ℓ₁ ℓ₂ →
+                     StrictPartialOrder a ℓ₁ ℓ₂
+strictPartialOrder O = record
+  { isStrictPartialOrder = isStrictPartialOrder O.isStrictPartialOrder
+  } where module O = StrictPartialOrder O
+
+strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂ →
+                   StrictTotalOrder a ℓ₁ ℓ₂
+strictTotalOrder O = record
+  { isStrictTotalOrder = isStrictTotalOrder O.isStrictTotalOrder
+  } where module O = StrictTotalOrder O
diff --git a/src/Relation/Binary/Construct/Flip.agda b/src/Relation/Binary/Construct/Flip/Ord.agda
similarity index 97%
rename from src/Relation/Binary/Construct/Flip.agda
rename to src/Relation/Binary/Construct/Flip/Ord.agda
index 2f7145be9e..ecfc4b6df4 100644
--- a/src/Relation/Binary/Construct/Flip.agda
+++ b/src/Relation/Binary/Construct/Flip/Ord.agda
@@ -2,15 +2,15 @@
 -- The Agda standard library
 --
 -- Many properties which hold for `∼` also hold for `flip ∼`. Unlike
--- the module `Relation.Binary.Construct.Converse` this module flips
--- both the relation and the underlying equality.
+-- the module `Relation.Binary.Construct.Flip.EqAndOrd` this module
+-- flips both the relation and the underlying equality.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary
 
-module Relation.Binary.Construct.Flip where
+module Relation.Binary.Construct.Flip.Ord where
 
 open import Data.Product
 open import Function.Base using (flip; _∘_)
diff --git a/src/Relation/Binary/Properties/DecTotalOrder.agda b/src/Relation/Binary/Properties/DecTotalOrder.agda
index 3a84300690..386bb2189b 100644
--- a/src/Relation/Binary/Properties/DecTotalOrder.agda
+++ b/src/Relation/Binary/Properties/DecTotalOrder.agda
@@ -13,7 +13,7 @@ module Relation.Binary.Properties.DecTotalOrder
 
 open DecTotalOrder DT hiding (trans)
 
-import Relation.Binary.Construct.Converse as Converse
+import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
 import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict
 import Relation.Binary.Properties.TotalOrder totalOrder as TotalOrderProperties
 open import Relation.Nullary.Negation using (¬_)
@@ -38,7 +38,7 @@ open TotalOrderProperties public
   )
 
 ≥-isDecTotalOrder : IsDecTotalOrder _≈_ _≥_
-≥-isDecTotalOrder = Converse.isDecTotalOrder isDecTotalOrder
+≥-isDecTotalOrder = EqAndOrd.isDecTotalOrder isDecTotalOrder
 
 ≥-decTotalOrder : DecTotalOrder _ _ _
 ≥-decTotalOrder = record
diff --git a/src/Relation/Binary/Properties/Preorder.agda b/src/Relation/Binary/Properties/Preorder.agda
index a6a8c196a0..1a215b639c 100644
--- a/src/Relation/Binary/Properties/Preorder.agda
+++ b/src/Relation/Binary/Properties/Preorder.agda
@@ -13,7 +13,7 @@ module Relation.Binary.Properties.Preorder
 
 open import Function.Base
 open import Data.Product as Prod
-import Relation.Binary.Construct.Converse as Converse
+import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
 
 open Preorder P
 
@@ -21,10 +21,10 @@ open Preorder P
 -- The inverse relation is also a preorder.
 
 converse-isPreorder : IsPreorder _≈_ (flip _∼_)
-converse-isPreorder = Converse.isPreorder isPreorder
+converse-isPreorder = EqAndOrd.isPreorder isPreorder
 
 converse-preorder : Preorder p₁ p₂ p₃
-converse-preorder = Converse.preorder P
+converse-preorder = EqAndOrd.preorder P
 
 ------------------------------------------------------------------------
 -- For every preorder there is an induced equivalence
diff --git a/src/Relation/Binary/Properties/StrictPartialOrder.agda b/src/Relation/Binary/Properties/StrictPartialOrder.agda
index d907fd75d4..7b6043af77 100644
--- a/src/Relation/Binary/Properties/StrictPartialOrder.agda
+++ b/src/Relation/Binary/Properties/StrictPartialOrder.agda
@@ -11,7 +11,7 @@ open import Relation.Binary
 module Relation.Binary.Properties.StrictPartialOrder
        {s₁ s₂ s₃} (SPO : StrictPartialOrder s₁ s₂ s₃) where
 
-import Relation.Binary.Construct.Converse as Converse
+import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
 import Relation.Binary.Construct.StrictToNonStrict
 
 open Relation.Binary.StrictPartialOrder SPO
@@ -20,7 +20,7 @@ open Relation.Binary.StrictPartialOrder SPO
 -- The inverse relation is also a strict partial order.
 
 >-strictPartialOrder : StrictPartialOrder s₁ s₂ s₃
->-strictPartialOrder = Converse.strictPartialOrder SPO
+>-strictPartialOrder = EqAndOrd.strictPartialOrder SPO
 
 open StrictPartialOrder >-strictPartialOrder public
   using ()
diff --git a/src/Relation/Binary/Properties/TotalOrder.agda b/src/Relation/Binary/Properties/TotalOrder.agda
index 58964e71a3..da4f316892 100644
--- a/src/Relation/Binary/Properties/TotalOrder.agda
+++ b/src/Relation/Binary/Properties/TotalOrder.agda
@@ -15,7 +15,7 @@ open TotalOrder T
 
 open import Data.Product using (proj₁)
 open import Data.Sum.Base using (inj₁; inj₂)
-import Relation.Binary.Construct.Converse as Converse
+import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
 import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict
 import Relation.Binary.Properties.Poset poset as PosetProperties
 open import Relation.Binary.Consequences
@@ -51,7 +51,7 @@ open PosetProperties public
   )
 
 ≥-isTotalOrder : IsTotalOrder _≈_ _≥_
-≥-isTotalOrder = Converse.isTotalOrder isTotalOrder
+≥-isTotalOrder = EqAndOrd.isTotalOrder isTotalOrder
 
 ≥-totalOrder : TotalOrder _ _ _
 ≥-totalOrder = record