diff --git a/README/Data/Trie/NonDependent.agda b/README/Data/Trie/NonDependent.agda
index 2387a71242..974ce5c96d 100644
--- a/README/Data/Trie/NonDependent.agda
+++ b/README/Data/Trie/NonDependent.agda
@@ -62,7 +62,7 @@ open import Data.These       as These
 
 open import Function.Base using (case_of_; _$_; _∘′_; id; _on_)
 open import Relation.Nary
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary.Decidable using (¬?)
 
 open import Data.Trie Char.<-strictTotalOrder
diff --git a/README/Design/Hierarchies.agda b/README/Design/Hierarchies.agda
index 0a91586086..cc03919b85 100644
--- a/README/Design/Hierarchies.agda
+++ b/README/Design/Hierarchies.agda
@@ -10,7 +10,7 @@ module README.Design.Hierarchies where
 
 open import Data.Sum using (_⊎_)
 open import Level using (Level; _⊔_; suc)
-open import Relation.Binary using (_Preserves₂_⟶_⟶_)
+open import Relation.Binary.Core using (_Preserves₂_⟶_⟶_)
 
 private
   variable
diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda
index 7c3030f4a6..6f2626889c 100644
--- a/src/Algebra/Consequences/Propositional.agda
+++ b/src/Algebra/Consequences/Propositional.agda
@@ -11,7 +11,9 @@ module Algebra.Consequences.Propositional
   {a} {A : Set a} where
 
 open import Data.Sum.Base using (inj₁; inj₂)
-open import Relation.Binary using (Rel; Setoid; Symmetric; Total)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions using (Symmetric; Total)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary using (Pred)
 
diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
index 07b75806c2..444a9296b8 100644
--- a/src/Algebra/Consequences/Setoid.agda
+++ b/src/Algebra/Consequences/Setoid.agda
@@ -7,7 +7,10 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; Setoid; Substitutive; Symmetric; Total)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions
+  using (Substitutive; Symmetric; Total)
 
 module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where
 
diff --git a/src/Algebra/Construct/Initial.agda b/src/Algebra/Construct/Initial.agda
index e542446248..99d80b98a3 100644
--- a/src/Algebra/Construct/Initial.agda
+++ b/src/Algebra/Construct/Initial.agda
@@ -22,7 +22,10 @@ open import Algebra.Core using (Op₂)
 open import Algebra.Definitions using (Congruent₂)
 open import Algebra.Structures using (IsMagma; IsSemigroup; IsBand)
 open import Data.Empty.Polymorphic
-open import Relation.Binary using (Rel; Reflexive; Symmetric; Transitive; IsEquivalence)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Binary.Definitions
+  using (Reflexive; Symmetric; Transitive)
 
 
 ------------------------------------------------------------------------
diff --git a/src/Algebra/FunctionProperties/Consequences.agda b/src/Algebra/FunctionProperties/Consequences.agda
index 03c9113995..e77b0b6d4e 100644
--- a/src/Algebra/FunctionProperties/Consequences.agda
+++ b/src/Algebra/FunctionProperties/Consequences.agda
@@ -6,7 +6,10 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; Setoid; Substitutive; Symmetric; Total)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions
+  using (Substitutive; Symmetric; Total)
 
 module Algebra.FunctionProperties.Consequences
   {a ℓ} (S : Setoid a ℓ) where
diff --git a/src/Algebra/Lattice/Bundles/Raw.agda b/src/Algebra/Lattice/Bundles/Raw.agda
index 5ac79408a5..8b5501cb72 100644
--- a/src/Algebra/Lattice/Bundles/Raw.agda
+++ b/src/Algebra/Lattice/Bundles/Raw.agda
@@ -11,7 +11,7 @@ module Algebra.Lattice.Bundles.Raw where
 open import Algebra.Core
 open import Algebra.Bundles.Raw using (RawMagma)
 open import Level using (suc; _⊔_)
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 
 record RawLattice c ℓ : Set (suc (c ⊔ ℓ)) where
   infixr 7 _∧_
diff --git a/src/Algebra/Lattice/Structures.agda b/src/Algebra/Lattice/Structures.agda
index b02787eee0..fc40c0c300 100644
--- a/src/Algebra/Lattice/Structures.agda
+++ b/src/Algebra/Lattice/Structures.agda
@@ -16,7 +16,9 @@
 open import Algebra.Core
 open import Data.Product.Base using (proj₁; proj₂)
 open import Level using (_⊔_)
-open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
 
 module Algebra.Lattice.Structures
   {a ℓ} {A : Set a}  -- The underlying set
diff --git a/src/Algebra/Lattice/Structures/Biased.agda b/src/Algebra/Lattice/Structures/Biased.agda
index fefe3bef67..b5e1e6c9fd 100644
--- a/src/Algebra/Lattice/Structures/Biased.agda
+++ b/src/Algebra/Lattice/Structures/Biased.agda
@@ -16,7 +16,9 @@ open import Algebra.Core
 open import Algebra.Consequences.Setoid
 open import Data.Product.Base using (proj₁; proj₂)
 open import Level using (_⊔_)
-open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
 
 module Algebra.Lattice.Structures.Biased
   {a ℓ} {A : Set a}  -- The underlying set
diff --git a/src/Algebra/Module/Consequences.agda b/src/Algebra/Module/Consequences.agda
index 4741349edc..2e53f96d76 100644
--- a/src/Algebra/Module/Consequences.agda
+++ b/src/Algebra/Module/Consequences.agda
@@ -14,7 +14,8 @@ open import Algebra.Module.Core using (Opₗ; Opᵣ)
 open import Algebra.Module.Definitions
 open import Function.Base using (flip)
 open import Level using (Level)
-open import Relation.Binary using (Rel; Setoid)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.Reasoning.Setoid as Rea
 
 private
diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda
index 4a0e40c17c..5b071b1a63 100644
--- a/src/Algebra/Module/Structures.agda
+++ b/src/Algebra/Module/Structures.agda
@@ -6,7 +6,9 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
 
 module Algebra.Module.Structures where
 
diff --git a/src/Algebra/Module/Structures/Biased.agda b/src/Algebra/Module/Structures/Biased.agda
index 74d825e335..99e48695ae 100644
--- a/src/Algebra/Module/Structures/Biased.agda
+++ b/src/Algebra/Module/Structures/Biased.agda
@@ -7,7 +7,9 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
 
 module Algebra.Module.Structures.Biased where
 
diff --git a/src/Algebra/Ordered/Bundles.agda b/src/Algebra/Ordered/Bundles.agda
index fd69b7145d..896f9d4d1f 100644
--- a/src/Algebra/Ordered/Bundles.agda
+++ b/src/Algebra/Ordered/Bundles.agda
@@ -16,7 +16,7 @@ open import Algebra.Core
 open import Algebra.Bundles
 open import Algebra.Ordered.Structures
 open import Level using (suc; _⊔_)
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Preorder; Poset)
 
 ------------------------------------------------------------------------
diff --git a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
index f07f898eb2..e92fa5170e 100644
--- a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
+++ b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
@@ -9,7 +9,7 @@
 open import Algebra using (CancellativeCommutativeSemiring)
 open import Algebra.Definitions using (AlmostRightCancellative)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Negation using (contradiction)
 
diff --git a/src/Algebra/Properties/Semiring/Primality.agda b/src/Algebra/Properties/Semiring/Primality.agda
index 2b0d226491..210d9fb1a0 100644
--- a/src/Algebra/Properties/Semiring/Primality.agda
+++ b/src/Algebra/Properties/Semiring/Primality.agda
@@ -9,7 +9,7 @@
 open import Algebra using (Semiring)
 open import Data.Sum.Base using (reduce)
 open import Function.Base using (flip)
-open import Relation.Binary using (Symmetric)
+open import Relation.Binary.Definitions using (Symmetric)
 
 module Algebra.Properties.Semiring.Primality
   {a ℓ} (R : Semiring a ℓ)
diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda
index bf066f7745..23e994821c 100644
--- a/src/Algebra/Solver/Monoid.agda
+++ b/src/Algebra/Solver/Monoid.agda
@@ -20,7 +20,7 @@ open import Data.Nat.Base using (ℕ)
 open import Data.Product
 open import Data.Vec.Base using (Vec; lookup)
 open import Function.Base using (_∘_; _$_)
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.Reflection
diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index eb9d49b2c9..4f9fc7fcb3 100644
--- a/src/Algebra/Structures.agda
+++ b/src/Algebra/Structures.agda
@@ -9,7 +9,9 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
 
 module Algebra.Structures
   {a ℓ} {A : Set a}  -- The underlying set
diff --git a/src/Algebra/Structures/Biased.agda b/src/Algebra/Structures/Biased.agda
index 0aa549c66c..c0c6994e3f 100644
--- a/src/Algebra/Structures/Biased.agda
+++ b/src/Algebra/Structures/Biased.agda
@@ -11,7 +11,9 @@ open import Algebra.Core
 open import Algebra.Consequences.Setoid
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Level using (_⊔_)
-open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
 
 module Algebra.Structures.Biased
   {a ℓ} {A : Set a}  -- The underlying set
diff --git a/src/Data/String.agda b/src/Data/String.agda
index fffe1ac300..7ff82dfac0 100644
--- a/src/Data/String.agda
+++ b/src/Data/String.agda
@@ -22,7 +22,7 @@ open import Data.Vec.Base as Vec using (Vec)
 open import Data.Char.Base as Char using (Char)
 import Data.Char.Properties as Char using (_≟_)
 open import Function
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Nullary.Decidable using (does)
 open import Relation.Unary using (Pred; Decidable)
diff --git a/src/Effect/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda
index 0751cb5b15..e6cfdd1c05 100644
--- a/src/Effect/Monad/Partiality.agda
+++ b/src/Effect/Monad/Partiality.agda
@@ -19,7 +19,13 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (Level; _⊔_)
-open import Relation.Binary as B hiding (Rel; _⇔_)
+open import Relation.Binary.Core as B hiding (Rel; _⇔_)
+open import Relation.Binary.Definitions
+  using (Decidable; Reflexive; Symmetric; Transitive)
+open import Relation.Binary.Structures
+  using (IsPreorder; IsEquivalence)
+open import Relation.Binary.Bundles
+  using (Preorder; Setoid; Poset)
 import Relation.Binary.Properties.Setoid as SetoidProperties
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as P
diff --git a/src/Function/Construct/Symmetry.agda b/src/Function/Construct/Symmetry.agda
index 86fa273c57..1974dee391 100644
--- a/src/Function/Construct/Symmetry.agda
+++ b/src/Function/Construct/Symmetry.agda
@@ -11,7 +11,9 @@ module Function.Construct.Symmetry where
 open import Data.Product.Base using (_,_; swap; proj₁; proj₂)
 open import Function
 open import Level using (Level)
-open import Relation.Binary hiding (_⇔_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Symmetric; Transitive)
+open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.PropositionalEquality
 
 private
diff --git a/src/Function/Indexed/Bundles.agda b/src/Function/Indexed/Bundles.agda
index 033cabd426..6cce0a3026 100644
--- a/src/Function/Indexed/Bundles.agda
+++ b/src/Function/Indexed/Bundles.agda
@@ -10,7 +10,7 @@ module Function.Indexed.Bundles where
 
 open import Relation.Unary using (Pred)
 open import Function.Bundles using (_⟶_; _↣_; _↠_; _⤖_; _⇔_; _↩_; _↪_; _↩↪_; _↔_)
-open import Relation.Binary hiding (_⇔_)
+open import Relation.Binary.Core hiding (_⇔_)
 open import Level using (Level)
 
 private
diff --git a/src/Relation/Binary/Construct/Closure/Transitive.agda b/src/Relation/Binary/Construct/Closure/Transitive.agda
index 551b6f5cb5..ed20e48bb0 100644
--- a/src/Relation/Binary/Construct/Closure/Transitive.agda
+++ b/src/Relation/Binary/Construct/Closure/Transitive.agda
@@ -12,7 +12,9 @@ open import Function.Base
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Induction.WellFounded
 open import Level
-open import Relation.Binary hiding (_⇔_)
+open import Relation.Binary.Core using (Rel; _=[_]⇒_; _⇒_)
+open import Relation.Binary.Definitions
+  using (Reflexive; Symmetric; Transitive)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 private
diff --git a/src/Relation/Binary/Indexed/Heterogeneous/Bundles.agda b/src/Relation/Binary/Indexed/Heterogeneous/Bundles.agda
index 089cad70ab..86dc3ccdaa 100644
--- a/src/Relation/Binary/Indexed/Heterogeneous/Bundles.agda
+++ b/src/Relation/Binary/Indexed/Heterogeneous/Bundles.agda
@@ -13,7 +13,7 @@ module Relation.Binary.Indexed.Heterogeneous.Bundles where
 
 open import Function.Base
 open import Level using (suc; _⊔_)
-open import Relation.Binary using (_⇒_)
+open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Binary.Indexed.Heterogeneous.Core
 open import Relation.Binary.Indexed.Heterogeneous.Structures
diff --git a/src/Relation/Binary/Indexed/Heterogeneous/Structures.agda b/src/Relation/Binary/Indexed/Heterogeneous/Structures.agda
index c61022d362..7e27aab07f 100644
--- a/src/Relation/Binary/Indexed/Heterogeneous/Structures.agda
+++ b/src/Relation/Binary/Indexed/Heterogeneous/Structures.agda
@@ -17,7 +17,7 @@ module Relation.Binary.Indexed.Heterogeneous.Structures
 
 open import Function.Base
 open import Level using (suc; _⊔_)
-open import Relation.Binary using (_⇒_)
+open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Binary.Indexed.Heterogeneous.Definitions
 
diff --git a/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda b/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda
index 5ed814cdc1..1f218cfc01 100644
--- a/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda
+++ b/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda
@@ -14,7 +14,8 @@ module Relation.Binary.Indexed.Homogeneous.Bundles where
 open import Data.Product using (_,_)
 open import Function.Base using (_⟨_⟩_)
 open import Level using (Level; _⊔_; suc)
-open import Relation.Binary as B using (_⇒_)
+open import Relation.Binary.Core using (_⇒_; Rel)
+open import Relation.Binary.Bundles as B
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Binary.Indexed.Homogeneous.Core
@@ -41,10 +42,10 @@ record IndexedSetoid {i} (I : Set i) c ℓ : Set (suc (i ⊔ c ⊔ ℓ)) where
 
   infix 4 _≉_
 
-  _≈_ : B.Rel Carrier _
+  _≈_ : Rel Carrier _
   _≈_ = Lift Carrierᵢ _≈ᵢ_
 
-  _≉_ : B.Rel Carrier _
+  _≉_ : Rel Carrier _
   x ≉ y = ¬ (x ≈ y)
 
   setoid : B.Setoid _ _
@@ -89,10 +90,10 @@ record IndexedPreorder {i} (I : Set i) c ℓ₁ ℓ₂ :
   Carrier : Set _
   Carrier = ∀ i → Carrierᵢ i
 
-  _≈_ : B.Rel Carrier _
+  _≈_ : Rel Carrier _
   x ≈ y = ∀ i → x i ≈ᵢ y i
 
-  _∼_ : B.Rel Carrier _
+  _∼_ : Rel Carrier _
   x ∼ y = ∀ i → x i ∼ᵢ y i
 
   preorder : B.Preorder _ _ _
diff --git a/src/Relation/Binary/Indexed/Homogeneous/Core.agda b/src/Relation/Binary/Indexed/Homogeneous/Core.agda
index 6dc2e03f82..7281652597 100644
--- a/src/Relation/Binary/Indexed/Homogeneous/Core.agda
+++ b/src/Relation/Binary/Indexed/Homogeneous/Core.agda
@@ -13,7 +13,7 @@ module Relation.Binary.Indexed.Homogeneous.Core where
 
 open import Level using (Level; _⊔_)
 open import Data.Product using (_×_)
-open import Relation.Binary as B using (REL; Rel)
+open import Relation.Binary.Core as B using (REL; Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 import Relation.Binary.Indexed.Heterogeneous as I
 open import Relation.Unary.Indexed using (IPred)
diff --git a/src/Relation/Binary/Indexed/Homogeneous/Structures.agda b/src/Relation/Binary/Indexed/Homogeneous/Structures.agda
index 38db83929a..0ccad66a6f 100644
--- a/src/Relation/Binary/Indexed/Homogeneous/Structures.agda
+++ b/src/Relation/Binary/Indexed/Homogeneous/Structures.agda
@@ -20,7 +20,9 @@ module Relation.Binary.Indexed.Homogeneous.Structures
 open import Data.Product using (_,_)
 open import Function.Base using (_⟨_⟩_)
 open import Level using (Level; _⊔_; suc)
-open import Relation.Binary as B using (_⇒_)
+open import Relation.Binary.Core using (_⇒_)
+import Relation.Binary.Definitions as B
+import Relation.Binary.Structures as B
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Binary.Indexed.Homogeneous.Definitions
 
@@ -97,7 +99,7 @@ record IsIndexedPreorder {ℓ₂} (_∼ᵢ_ : IRel A ℓ₂)
 
   -- Lifted properties
 
-  reflexive : Lift A _≈ᵢ_ B.⇒ Lift A _∼ᵢ_
+  reflexive : Lift A _≈ᵢ_ ⇒ Lift A _∼ᵢ_
   reflexive x≈y i = reflexiveᵢ (x≈y i)
 
   refl : B.Reflexive (Lift A _∼ᵢ_)
diff --git a/src/Relation/Binary/Lattice/Properties/BoundedLattice.agda b/src/Relation/Binary/Lattice/Properties/BoundedLattice.agda
index 95bf238945..1f3477b19d 100644
--- a/src/Relation/Binary/Lattice/Properties/BoundedLattice.agda
+++ b/src/Relation/Binary/Lattice/Properties/BoundedLattice.agda
@@ -15,7 +15,7 @@ open BoundedLattice L
 
 open import Algebra.Definitions _≈_
 open import Data.Product using (_,_)
-open import Relation.Binary using (Setoid)
+open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Lattice.Properties.MeetSemilattice meetSemilattice
 open import Relation.Binary.Lattice.Properties.JoinSemilattice joinSemilattice
 
diff --git a/src/Relation/Nullary/Universe.agda b/src/Relation/Nullary/Universe.agda
index 68394c051c..74b34607a6 100644
--- a/src/Relation/Nullary/Universe.agda
+++ b/src/Relation/Nullary/Universe.agda
@@ -10,7 +10,8 @@ module Relation.Nullary.Universe where
 
 open import Relation.Nullary
 open import Relation.Nullary.Negation
-open import Relation.Binary hiding (_⇒_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.Construct.Always as Always
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 import Relation.Binary.PropositionalEquality.Properties as PropEq
diff --git a/src/Relation/Unary/PredicateTransformer.agda b/src/Relation/Unary/PredicateTransformer.agda
index 518552d0d8..b6df4f2b8a 100644
--- a/src/Relation/Unary/PredicateTransformer.agda
+++ b/src/Relation/Unary/PredicateTransformer.agda
@@ -13,7 +13,7 @@ open import Function
 open import Level hiding (_⊔_)
 open import Relation.Nullary
 open import Relation.Unary
-open import Relation.Binary using (REL)
+open import Relation.Binary.Core using (REL)
 
 private
   variable
diff --git a/src/Text/Regex.agda b/src/Text/Regex.agda
index b6454f36ae..9b818d15b5 100644
--- a/src/Text/Regex.agda
+++ b/src/Text/Regex.agda
@@ -10,7 +10,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (DecPoset)
+open import Relation.Binary.Bundles using (DecPoset)
 
 module Text.Regex {a e r} (decPoset : DecPoset a e r) where
 
diff --git a/src/Text/Regex/Base.agda b/src/Text/Regex/Base.agda
index 839bad4181..e5cc2c24a4 100644
--- a/src/Text/Regex/Base.agda
+++ b/src/Text/Regex/Base.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Preorder)
+open import Relation.Binary.Bundles using (Preorder)
 
 module Text.Regex.Base {a e r} (P : Preorder a e r) where
 
diff --git a/src/Text/Regex/Derivative/Brzozowski.agda b/src/Text/Regex/Derivative/Brzozowski.agda
index d368bfc70d..9c66c831a4 100644
--- a/src/Text/Regex/Derivative/Brzozowski.agda
+++ b/src/Text/Regex/Derivative/Brzozowski.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (DecPoset)
+open import Relation.Binary.Bundles using (DecPoset)
 
 module Text.Regex.Derivative.Brzozowski {a e r} (P? : DecPoset a e r) where
 
@@ -18,7 +18,7 @@ open import Function.Base using (_$_; _∘′_; case_of_)
 open import Relation.Nullary.Decidable using (Dec; yes; no)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Nullary.Decidable using (map′; ¬?)
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
 open DecPoset P? using (preorder) renaming (Carrier to A)
diff --git a/src/Text/Regex/Properties.agda b/src/Text/Regex/Properties.agda
index cf807ca3f3..815bf04471 100644
--- a/src/Text/Regex/Properties.agda
+++ b/src/Text/Regex/Properties.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (DecPoset)
+open import Relation.Binary.Bundles using (DecPoset)
 
 module Text.Regex.Properties {a e r} (P? : DecPoset a e r) where
 
@@ -23,7 +23,7 @@ open import Relation.Nullary.Negation
   using (¬_; contradiction)
 
 import Relation.Unary  as U
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 
 open DecPoset P? renaming (Carrier to A)
 open import Text.Regex.Base preorder
diff --git a/src/Text/Regex/Properties/Core.agda b/src/Text/Regex/Properties/Core.agda
index 64faba7029..e1916fb5cf 100644
--- a/src/Text/Regex/Properties/Core.agda
+++ b/src/Text/Regex/Properties/Core.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Preorder)
+open import Relation.Binary.Bundles using (Preorder)
 
 module Text.Regex.Properties.Core {a e r} (P : Preorder a e r) where
 
diff --git a/src/Text/Regex/Search.agda b/src/Text/Regex/Search.agda
index f5c8c780c3..b96fb3847c 100644
--- a/src/Text/Regex/Search.agda
+++ b/src/Text/Regex/Search.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (DecPoset)
+open import Relation.Binary.Bundles using (DecPoset)
 
 module Text.Regex.Search {a e r} (P? : DecPoset a e r) where
 
@@ -29,7 +29,8 @@ open import Data.List.Relation.Binary.Suffix.Heterogeneous
 open import Relation.Nullary using (Dec; ¬_; yes; no)
 open import Relation.Nullary.Decidable using (map′)
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Binary using (Rel; Decidable; _⇒_)
+open import Relation.Binary.Core using (Rel; _⇒_)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality.Core
 
 open DecPoset P? using (preorder) renaming (Carrier to A)
diff --git a/src/Text/Regex/SmartConstructors.agda b/src/Text/Regex/SmartConstructors.agda
index afe9d3f936..3269d22da5 100644
--- a/src/Text/Regex/SmartConstructors.agda
+++ b/src/Text/Regex/SmartConstructors.agda
@@ -9,7 +9,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Preorder)
+open import Relation.Binary.Bundles using (Preorder)
 
 module Text.Regex.SmartConstructors {a e r} (P : Preorder a e r) where
 
diff --git a/src/Text/Regex/String/Unsafe.agda b/src/Text/Regex/String/Unsafe.agda
index a46fcd5655..118b48505a 100644
--- a/src/Text/Regex/String/Unsafe.agda
+++ b/src/Text/Regex/String/Unsafe.agda
@@ -12,7 +12,8 @@ open import Data.String.Base using (String; toList; fromList)
 import Data.String.Unsafe as Stringₚ
 open import Function.Base using (_on_; id)
 open import Level using (0ℓ)
-open import Relation.Binary using (Rel; Decidable)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; sym; subst)
 open import Relation.Nullary.Decidable using (map′)
 
diff --git a/tests/data/trie/Main.agda b/tests/data/trie/Main.agda
index 9dfac5cb26..3ce2ad3ecb 100644
--- a/tests/data/trie/Main.agda
+++ b/tests/data/trie/Main.agda
@@ -18,7 +18,7 @@ open import Data.These        as These
 
 open import Function.Base using (case_of_; _$_; _∘′_; id; _on_)
 open import Relation.Nary
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary.Decidable using (¬?)
 
 open import Data.Trie Char.<-strictTotalOrder