diff --git a/README/Nary.agda b/README/Nary.agda
index 16e50392b3..932a9f92c3 100644
--- a/README/Nary.agda
+++ b/README/Nary.agda
@@ -19,7 +19,7 @@ open import Data.Product using (_×_; _,_)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (id; flip; _∘′_)
 open import Relation.Nullary
-open import Relation.Binary using (module Tri); open Tri
+open import Relation.Binary.Definitions using (module Tri); open Tri
 open import Relation.Binary.PropositionalEquality
 
 private
diff --git a/src/Data/AVL.agda b/src/Data/AVL.agda
index ca0015925b..14c695d0d4 100644
--- a/src/Data/AVL.agda
+++ b/src/Data/AVL.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.AVL
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
diff --git a/src/Data/AVL/Indexed.agda b/src/Data/AVL/Indexed.agda
index a4ee4a1d96..9efe5e7500 100644
--- a/src/Data/AVL/Indexed.agda
+++ b/src/Data/AVL/Indexed.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.AVL.Indexed
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) where
diff --git a/src/Data/AVL/NonEmpty/Propositional.agda b/src/Data/AVL/NonEmpty/Propositional.agda
index 70087c1f88..0318537f0e 100644
--- a/src/Data/AVL/NonEmpty/Propositional.agda
+++ b/src/Data/AVL/NonEmpty/Propositional.agda
@@ -6,7 +6,9 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; IsStrictTotalOrder; StrictTotalOrder)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Structures using (IsStrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
 
 module Data.AVL.NonEmpty.Propositional
diff --git a/src/Data/List/Extrema.agda b/src/Data/List/Extrema.agda
index 5abc5edee9..16e38db5bb 100644
--- a/src/Data/List/Extrema.agda
+++ b/src/Data/List/Extrema.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (TotalOrder; Setoid)
+open import Relation.Binary.Bundles using (TotalOrder; Setoid)
 
 module Data.List.Extrema
   {b ℓ₁ ℓ₂} (totalOrder : TotalOrder b ℓ₁ ℓ₂) where
diff --git a/src/Data/List/Fresh/Properties.agda b/src/Data/List/Fresh/Properties.agda
index b22347f92e..6619fbb18d 100644
--- a/src/Data/List/Fresh/Properties.agda
+++ b/src/Data/List/Fresh/Properties.agda
@@ -12,7 +12,8 @@ open import Level using (Level; _⊔_; Lift)
 open import Data.Product.Base using (_,_)
 open import Relation.Nullary
 open import Relation.Unary as U using (Pred)
-open import Relation.Binary as B using (Rel)
+import Relation.Binary.Definitions as B
+open import Relation.Binary.Core using (Rel)
 
 open import Data.List.Fresh
 
diff --git a/src/Data/List/Membership/DecPropositional.agda b/src/Data/List/Membership/DecPropositional.agda
index a59ce42c67..71cb595375 100644
--- a/src/Data/List/Membership/DecPropositional.agda
+++ b/src/Data/List/Membership/DecPropositional.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality using (_≡_)
 open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
diff --git a/src/Data/List/Membership/DecSetoid.agda b/src/Data/List/Membership/DecSetoid.agda
index 3d798abc5b..8f34aab9f6 100644
--- a/src/Data/List/Membership/DecSetoid.agda
+++ b/src/Data/List/Membership/DecSetoid.agda
@@ -6,7 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Decidable; DecSetoid)
+open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Binary.Bundles using (DecSetoid)
 open import Relation.Nullary.Decidable using (¬?)
 
 module Data.List.Membership.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 454ee4b211..3a33b2b1dc 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -34,10 +34,10 @@ open import Data.Fin.Properties using (toℕ-cast)
 open import Function.Base using (id; _∘_; _∘′_; _∋_; _-⟨_∣; ∣_⟩-_; _$_; const; flip)
 open import Function.Definitions using (Injective)
 open import Level using (Level)
-open import Relation.Binary as B using (DecidableEquality)
+open import Relation.Binary.Definitions as B using (DecidableEquality)
 import Relation.Binary.Reasoning.Setoid as EqR
 open import Relation.Binary.PropositionalEquality as P hiding ([_])
-open import Relation.Binary as B using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no; contradiction)
 open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋; ¬?; _×-dec_)
diff --git a/src/Data/List/Relation/Binary/Equality/DecSetoid.agda b/src/Data/List/Relation/Binary/Equality/DecSetoid.agda
index 45f73c0902..ec82d91dcf 100644
--- a/src/Data/List/Relation/Binary/Equality/DecSetoid.agda
+++ b/src/Data/List/Relation/Binary/Equality/DecSetoid.agda
@@ -14,7 +14,7 @@ module Data.List.Relation.Binary.Equality.DecSetoid
 import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
 import Data.List.Relation.Binary.Pointwise as PW
 open import Level
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 open DecSetoid DS
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Relation/Binary/Equality/Setoid.agda b/src/Data/List/Relation/Binary/Equality/Setoid.agda
index f1ed5f457c..fc6842c38d 100644
--- a/src/Data/List/Relation/Binary/Equality/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Equality/Setoid.agda
@@ -7,7 +7,9 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Core using (Op₂)
-open import Relation.Binary using (Setoid)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions using (Transitive; Symmetric; Reflexive; _Respects_)
+open import Relation.Binary.Structures using (IsEquivalence)
 
 module Data.List.Relation.Binary.Equality.Setoid {a ℓ} (S : Setoid a ℓ) where
 
@@ -17,7 +19,7 @@ open import Data.List.Relation.Binary.Pointwise as PW using (Pointwise)
 open import Data.List.Relation.Unary.Unique.Setoid S using (Unique)
 open import Function.Base using (_∘_)
 open import Level
-open import Relation.Binary renaming (Rel to Rel₂)
+open import Relation.Binary.Core renaming (Rel to Rel₂)
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Binary.Properties.Setoid S using (≉-resp₂)
 open import Relation.Unary as U using (Pred)
diff --git a/src/Data/List/Relation/Binary/Infix/Heterogeneous.agda b/src/Data/List/Relation/Binary/Infix/Heterogeneous.agda
index c9668fa1ec..b09af201e0 100644
--- a/src/Data/List/Relation/Binary/Infix/Heterogeneous.agda
+++ b/src/Data/List/Relation/Binary/Infix/Heterogeneous.agda
@@ -9,7 +9,7 @@
 module Data.List.Relation.Binary.Infix.Heterogeneous where
 
 open import Level
-open import Relation.Binary using (REL; _⇒_)
+open import Relation.Binary.Core using (REL; _⇒_)
 open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.List.Relation.Binary.Pointwise
   using (Pointwise)
diff --git a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
index cc067dc846..9af0162ded 100644
--- a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
@@ -20,7 +20,8 @@ open import Function.Base using (case_of_; _$′_)
 open import Relation.Nullary.Decidable using (yes; no; does; map′; _⊎-dec_)
 open import Relation.Nullary.Negation using (¬_; contradiction)
 open import Relation.Unary as U using (Pred)
-open import Relation.Binary using (REL; _⇒_; Decidable; Trans; Antisym)
+open import Relation.Binary.Core using (REL; _⇒_)
+open import Relation.Binary.Definitions using (Decidable; Trans; Antisym)
 open import Relation.Binary.PropositionalEquality.Core using (_≢_; refl; cong)
 open import Data.List.Relation.Binary.Pointwise.Base as Pointwise using (Pointwise)
 open import Data.List.Relation.Binary.Infix.Heterogeneous
diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda
index 0852085a37..9ecab7f628 100644
--- a/src/Data/List/Relation/Binary/Pointwise.agda
+++ b/src/Data/List/Relation/Binary/Pointwise.agda
@@ -25,7 +25,10 @@ open import Level
 open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec using (map′)
 open import Relation.Unary as U using (Pred)
-open import Relation.Binary renaming (Rel to Rel₂)
+open import Relation.Binary.Core renaming (Rel to Rel₂)
+open import Relation.Binary.Definitions using (_Respects_; _Respects₂_)
+open import Relation.Binary.Bundles using (Setoid; DecSetoid; Preorder; Poset)
+open import Relation.Binary.Structures using (IsEquivalence; IsDecEquivalence; IsPartialOrder; IsPreorder)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as P
 
diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
index 1378e745f5..844dd1c996 100644
--- a/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
@@ -22,7 +22,7 @@ import Data.List.Relation.Binary.Sublist.Setoid.Properties
 open import Data.Product using (∃; _,_; proj₂)
 open import Function.Base
 open import Level using (Level)
-open import Relation.Binary using (_Respects_)
+open import Relation.Binary.Definitions using (_Respects_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary using (Pred)
 
diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
index abe9a20b73..df904a0452 100644
--- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
@@ -6,7 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; Setoid; _⇒_; _Preserves_⟶_)
+open import Relation.Binary.Core using (Rel; _⇒_; _Preserves_⟶_)
+open import Relation.Binary.Bundles using (Setoid)
 
 module Data.List.Relation.Binary.Sublist.Setoid.Properties
   {c ℓ} (S : Setoid c ℓ) where
@@ -20,7 +21,7 @@ open import Data.Product using (∃; _,_; proj₂)
 open import Function.Base
 open import Function.Bundles using (_⇔_; _⤖_)
 open import Level
-open import Relation.Binary using () renaming (Decidable to Decidable₂)
+open import Relation.Binary.Definitions using () renaming (Decidable to Decidable₂)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 open import Relation.Binary.Structures using (IsDecTotalOrder)
 open import Relation.Unary using (Pred; Decidable; Irrelevant)
diff --git a/src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda b/src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda
index aeeb927d2d..441956829f 100644
--- a/src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda
+++ b/src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda
@@ -9,7 +9,7 @@
 module Data.List.Relation.Binary.Suffix.Heterogeneous where
 
 open import Level
-open import Relation.Binary using (REL; _⇒_)
+open import Relation.Binary.Core using (REL; _⇒_)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Binary.Pointwise.Base as Pointwise
   using (Pointwise; []; _∷_)
diff --git a/src/Data/List/Relation/Unary/AllPairs/Core.agda b/src/Data/List/Relation/Unary/AllPairs/Core.agda
index 04728171b0..899d2d76fd 100644
--- a/src/Data/List/Relation/Unary/AllPairs/Core.agda
+++ b/src/Data/List/Relation/Unary/AllPairs/Core.agda
@@ -12,7 +12,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 
 module Data.List.Relation.Unary.AllPairs.Core
   {a ℓ} {A : Set a} (R : Rel A ℓ) where
diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda
index 037279cfe1..c116fcb00f 100644
--- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda
+++ b/src/Data/List/Relation/Unary/AllPairs/Properties.agda
@@ -19,7 +19,8 @@ open import Data.Nat.Base using (zero; suc; _<_; z≤n; s≤s)
 open import Data.Nat.Properties using (≤-refl; m<n⇒m<1+n)
 open import Function.Base using (_∘_; flip)
 open import Level using (Level)
-open import Relation.Binary using (Rel; DecSetoid)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (DecSetoid)
 open import Relation.Binary.PropositionalEquality.Core using (_≢_)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Nullary.Decidable using (does)
diff --git a/src/Data/List/Relation/Unary/Grouped/Properties.agda b/src/Data/List/Relation/Unary/Grouped/Properties.agda
index 65ac3d6ed6..f020cdd233 100644
--- a/src/Data/List/Relation/Unary/Grouped/Properties.agda
+++ b/src/Data/List/Relation/Unary/Grouped/Properties.agda
@@ -16,7 +16,8 @@ open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _
 open import Data.List.Relation.Unary.Grouped
 open import Function.Base using (_∘_)
 open import Function.Bundles using (module Equivalence; _⇔_)
-open import Relation.Binary as B using (REL; Rel)
+open import Relation.Binary.Definitions as B
+open import Relation.Binary.Core using (REL; Rel)
 open import Relation.Unary as U using (Pred)
 open import Relation.Nullary using (¬_; does; yes; no)
 open import Relation.Nullary.Negation using (contradiction)
diff --git a/src/Data/List/Relation/Unary/Linked.agda b/src/Data/List/Relation/Unary/Linked.agda
index cfafbc28b5..71e889924e 100644
--- a/src/Data/List/Relation/Unary/Linked.agda
+++ b/src/Data/List/Relation/Unary/Linked.agda
@@ -16,7 +16,8 @@ open import Data.Maybe.Relation.Binary.Connected
   using (Connected; just; just-nothing)
 open import Function.Base using (id; _∘_)
 open import Level using (Level; _⊔_)
-open import Relation.Binary as B using (Rel; _⇒_)
+open import Relation.Binary.Definitions as B
+open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
diff --git a/src/Data/List/Sort.agda b/src/Data/List/Sort.agda
index d0939b4d49..acae2ce7f5 100644
--- a/src/Data/List/Sort.agda
+++ b/src/Data/List/Sort.agda
@@ -10,7 +10,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Data.List.Base using (List)
-open import Relation.Binary using (DecTotalOrder)
+open import Relation.Binary.Bundles using (DecTotalOrder)
 
 module Data.List.Sort
   {a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂)
diff --git a/src/Data/List/Sort/Base.agda b/src/Data/List/Sort/Base.agda
index 0c20220e78..ae64c39bd3 100644
--- a/src/Data/List/Sort/Base.agda
+++ b/src/Data/List/Sort/Base.agda
@@ -9,7 +9,7 @@
 open import Data.List.Base using (List)
 open import Data.List.Relation.Binary.Permutation.Propositional
 open import Level using (_⊔_)
-open import Relation.Binary using (TotalOrder)
+open import Relation.Binary.Bundles using (TotalOrder)
 
 module Data.List.Sort.Base
   {a ℓ₁ ℓ₂} (totalOrder : TotalOrder a ℓ₁ ℓ₂)
diff --git a/src/Data/List/Sort/MergeSort.agda b/src/Data/List/Sort/MergeSort.agda
index 09ccdf2471..c51e8c35eb 100644
--- a/src/Data/List/Sort/MergeSort.agda
+++ b/src/Data/List/Sort/MergeSort.agda
@@ -26,7 +26,7 @@ open import Data.Nat.Induction
 open import Data.Nat.Properties using (m<n⇒m<1+n)
 open import Data.Product as Prod using (_,_)
 open import Function.Base using (_∘_)
-open import Relation.Binary using (DecTotalOrder)
+open import Relation.Binary.Bundles using (DecTotalOrder)
 open import Relation.Nullary.Negation using (¬_)
 
 module Data.List.Sort.MergeSort
diff --git a/src/Data/Maybe/Properties.agda b/src/Data/Maybe/Properties.agda
index cb19c9c328..ab1554a389 100644
--- a/src/Data/Maybe/Properties.agda
+++ b/src/Data/Maybe/Properties.agda
@@ -17,7 +17,7 @@ open import Data.Product using (_,_)
 open import Function.Base using (_∋_; id; _∘_; _∘′_)
 open import Function.Definitions using (Injective)
 open import Level using (Level)
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Decidable using (map′)
diff --git a/src/Data/Nat/Divisibility/Core.agda b/src/Data/Nat/Divisibility/Core.agda
index 3b06bc2c96..2f8cdbe241 100644
--- a/src/Data/Nat/Divisibility/Core.agda
+++ b/src/Data/Nat/Divisibility/Core.agda
@@ -16,7 +16,7 @@ open import Data.Nat.Base using (ℕ; _*_)
 open import Data.Nat.Properties
 open import Level using (0ℓ)
 open import Relation.Nullary.Negation using (¬_)
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; sym; cong₂; module ≡-Reasoning)
 
diff --git a/src/Data/Product/Effectful/Examples.agda b/src/Data/Product/Effectful/Examples.agda
index 0ada48ad84..f11631341e 100644
--- a/src/Data/Product/Effectful/Examples.agda
+++ b/src/Data/Product/Effectful/Examples.agda
@@ -18,7 +18,7 @@ open import Data.Product
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Function.Base using (id)
 import Function.Identity.Effectful as Id
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Product/Properties.agda b/src/Data/Product/Properties.agda
index 1cc3c2383e..e741f8976a 100644
--- a/src/Data/Product/Properties.agda
+++ b/src/Data/Product/Properties.agda
@@ -13,7 +13,7 @@ open import Data.Product.Base
 open import Function.Base using (_∋_; _∘_; id)
 open import Function.Bundles using (_↔_; mk↔′)
 open import Level using (Level)
-open import Relation.Binary using (DecidableEquality)
+open import Relation.Binary.Definitions using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable as Dec using (Dec; yes; no)
 
diff --git a/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda b/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda
index 13edd9aa66..7fce761f79 100644
--- a/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda
+++ b/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda
@@ -13,7 +13,7 @@ open import Data.Product
 open import Data.Product.Relation.Binary.Pointwise.Dependent
 open import Function.Base
 open import Function.Inverse using (Inverse)
-open import Relation.Binary using (_⇒_)
+open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.HeterogeneousEquality as H using (_≅_)
 open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
diff --git a/src/Data/Sum/Properties.agda b/src/Data/Sum/Properties.agda
index 2c6e638731..1ee329a2d5 100644
--- a/src/Data/Sum/Properties.agda
+++ b/src/Data/Sum/Properties.agda
@@ -12,7 +12,7 @@ open import Level
 open import Data.Sum.Base
 open import Function.Base using (_∋_; _∘_; id)
 open import Function.Bundles using (mk↔′; _↔_)
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Decidable using (map′)
diff --git a/src/Data/These/Properties.agda b/src/Data/These/Properties.agda
index 62257ed1ad..a6c96a3208 100644
--- a/src/Data/These/Properties.agda
+++ b/src/Data/These/Properties.agda
@@ -11,7 +11,7 @@ module Data.These.Properties where
 open import Data.Product
 open import Data.These.Base
 open import Function.Base using (_∘_)
-open import Relation.Binary using (Decidable)
+open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary.Decidable using (yes; no; map′; _×-dec_)
 
diff --git a/src/Data/Tree/AVL/Indexed.agda b/src/Data/Tree/AVL/Indexed.agda
index 16ebdff70e..c322d680e3 100644
--- a/src/Data/Tree/AVL/Indexed.agda
+++ b/src/Data/Tree/AVL/Indexed.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Indexed
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) where
@@ -19,7 +19,7 @@ open import Data.List.Base as List using (List)
 open import Data.DifferenceList using (DiffList; []; _∷_; _++_)
 open import Function.Base as F hiding (const)
 open import Relation.Unary
-open import Relation.Binary using (_Respects_; Tri; tri<; tri≈; tri>)
+open import Relation.Binary.Definitions using (_Respects_; Tri; tri<; tri≈; tri>)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 private
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda
index 5add64a3cc..af3d328138 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Indexed.Relation.Unary.All
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
index 2b0d6f98a7..2710a373b5 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Indexed.Relation.Unary.Any
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
index ef06c5574a..9f4aa1aeca 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties
   {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
@@ -21,7 +21,7 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
 open import Function.Base as F
 open import Level using (Level)
 
-open import Relation.Binary using (_Respects_; tri<; tri≈; tri>)
+open import Relation.Binary.Definitions using (_Respects_; tri<; tri≈; tri>)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_) renaming (refl to ≡-refl)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Nullary.Negation using (contradiction)
diff --git a/src/Data/Tree/AVL/Map.agda b/src/Data/Tree/AVL/Map.agda
index 65731a8f29..53d72e10a3 100644
--- a/src/Data/Tree/AVL/Map.agda
+++ b/src/Data/Tree/AVL/Map.agda
@@ -8,7 +8,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Map
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional.agda b/src/Data/Tree/AVL/Map/Membership/Propositional.agda
index 5e9498ea31..0873c66cd2 100644
--- a/src/Data/Tree/AVL/Map/Membership/Propositional.agda
+++ b/src/Data/Tree/AVL/Map/Membership/Propositional.agda
@@ -7,7 +7,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Map.Membership.Propositional
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
@@ -21,7 +21,7 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; _∘′_)
 open import Level using (Level)
 
-open import Relation.Binary using (Transitive; Symmetric; _Respectsˡ_)
+open import Relation.Binary.Definitions using (Transitive; Symmetric; _Respectsˡ_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Construct.Intersection using (_∩_)
 open import Relation.Binary.PropositionalEquality
diff --git a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
index 050dd82f12..aef88a23d7 100644
--- a/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
+++ b/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
@@ -7,7 +7,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Map.Membership.Propositional.Properties
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
@@ -21,7 +21,7 @@ open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base using (_∘_; _∘′_)
 open import Level using (Level)
 
-open import Relation.Binary using (Transitive; Symmetric; _Respectsˡ_)
+open import Relation.Binary.Definitions using (Transitive; Symmetric; _Respectsˡ_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Construct.Intersection using (_∩_)
 open import Relation.Binary.PropositionalEquality
diff --git a/src/Data/Tree/AVL/Map/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Map/Relation/Unary/Any.agda
index 4bd6961c3d..8a347bd5ff 100644
--- a/src/Data/Tree/AVL/Map/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Map/Relation/Unary/Any.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Map.Relation.Unary.Any
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
diff --git a/src/Data/Tree/AVL/NonEmpty.agda b/src/Data/Tree/AVL/NonEmpty.agda
index 0e6b680d90..d95686b93c 100644
--- a/src/Data/Tree/AVL/NonEmpty.agda
+++ b/src/Data/Tree/AVL/NonEmpty.agda
@@ -11,7 +11,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.NonEmpty
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) where
diff --git a/src/Data/Tree/AVL/NonEmpty/Propositional.agda b/src/Data/Tree/AVL/NonEmpty/Propositional.agda
index 82ea9125fd..632d4de428 100644
--- a/src/Data/Tree/AVL/NonEmpty/Propositional.agda
+++ b/src/Data/Tree/AVL/NonEmpty/Propositional.agda
@@ -6,7 +6,9 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; IsStrictTotalOrder; StrictTotalOrder)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Structures using (IsStrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; subst)
 
 module Data.Tree.AVL.NonEmpty.Propositional
diff --git a/src/Data/Tree/AVL/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Relation/Unary/Any.agda
index e0dbadfa83..a9429d4ed2 100644
--- a/src/Data/Tree/AVL/Relation/Unary/Any.agda
+++ b/src/Data/Tree/AVL/Relation/Unary/Any.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Relation.Unary.Any
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
diff --git a/src/Data/Tree/AVL/Sets.agda b/src/Data/Tree/AVL/Sets.agda
index b533605b95..163b4e0d95 100644
--- a/src/Data/Tree/AVL/Sets.agda
+++ b/src/Data/Tree/AVL/Sets.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Sets
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
diff --git a/src/Data/Tree/AVL/Sets/Membership.agda b/src/Data/Tree/AVL/Sets/Membership.agda
index 53e0aea9f9..0c1ae29947 100644
--- a/src/Data/Tree/AVL/Sets/Membership.agda
+++ b/src/Data/Tree/AVL/Sets/Membership.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Sets.Membership
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
diff --git a/src/Data/Tree/AVL/Sets/Membership/Properties.agda b/src/Data/Tree/AVL/Sets/Membership/Properties.agda
index 75fc1e9242..b41f7848cb 100644
--- a/src/Data/Tree/AVL/Sets/Membership/Properties.agda
+++ b/src/Data/Tree/AVL/Sets/Membership/Properties.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (StrictTotalOrder)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Tree.AVL.Sets.Membership.Properties
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
diff --git a/src/Data/Tree/AVL/Value.agda b/src/Data/Tree/AVL/Value.agda
index 77af5cffdb..8be94311b5 100644
--- a/src/Data/Tree/AVL/Value.agda
+++ b/src/Data/Tree/AVL/Value.agda
@@ -7,7 +7,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Setoid; _Respects_)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions using (_Respects_)
 
 module Data.Tree.AVL.Value {a ℓ} (S : Setoid a ℓ) where
 
diff --git a/src/Data/Trie.agda b/src/Data/Trie.agda
index 7f06a6f0ed..694d7afe7b 100644
--- a/src/Data/Trie.agda
+++ b/src/Data/Trie.agda
@@ -9,7 +9,8 @@
 
 {-# OPTIONS --cubical-compatible --sized-types #-}
 
-open import Relation.Binary using (Rel; StrictTotalOrder)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (StrictTotalOrder)
 
 module Data.Trie {k e r} (S : StrictTotalOrder k e r) where
 
diff --git a/src/Data/Vec/Bounded.agda b/src/Data/Vec/Bounded.agda
index 3a1aae623e..2f189339d0 100644
--- a/src/Data/Vec/Bounded.agda
+++ b/src/Data/Vec/Bounded.agda
@@ -12,7 +12,7 @@ open import Level using (Level)
 open import Data.Nat.Base
 open import Data.Vec as Vec using (Vec)
 open import Function.Base using (id)
-open import Relation.Binary using (_Preserves_⟶_)
+open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Unary using (Pred; Decidable)
 
 private
diff --git a/src/Data/Vec/Membership/DecSetoid.agda b/src/Data/Vec/Membership/DecSetoid.agda
index 10efd977d7..fac9138660 100644
--- a/src/Data/Vec/Membership/DecSetoid.agda
+++ b/src/Data/Vec/Membership/DecSetoid.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (DecSetoid)
+open import Relation.Binary.Bundles using (DecSetoid)
 
 module Data.Vec.Membership.DecSetoid {c ℓ} (DS : DecSetoid c ℓ) where
 
diff --git a/src/Data/Vec/Membership/Setoid.agda b/src/Data/Vec/Membership/Setoid.agda
index 50ef16bb79..57476d5f35 100644
--- a/src/Data/Vec/Membership/Setoid.agda
+++ b/src/Data/Vec/Membership/Setoid.agda
@@ -6,7 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Setoid; _Respects_)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions using (_Respects_)
 
 module Data.Vec.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
 
diff --git a/src/Data/Vec/Relation/Unary/All.agda b/src/Data/Vec/Relation/Unary/All.agda
index 2eda26c71e..a8faa0e79f 100644
--- a/src/Data/Vec/Relation/Unary/All.agda
+++ b/src/Data/Vec/Relation/Unary/All.agda
@@ -19,7 +19,8 @@ open import Function.Base using (_∘_)
 open import Level using (Level; _⊔_)
 open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no)
 open import Relation.Unary hiding (_∈_)
-open import Relation.Binary using (Setoid; _Respects_)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Definitions using (_Respects_)
 open import Relation.Binary.PropositionalEquality.Core as P using (subst)
 
 private
diff --git a/src/Data/Vec/Relation/Unary/AllPairs.agda b/src/Data/Vec/Relation/Unary/AllPairs.agda
index 0fee880769..bc671b3826 100644
--- a/src/Data/Vec/Relation/Unary/AllPairs.agda
+++ b/src/Data/Vec/Relation/Unary/AllPairs.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel; _⇒_)
 
 module Data.Vec.Relation.Unary.AllPairs
        {a ℓ} {A : Set a} {R : Rel A ℓ} where
@@ -17,7 +17,7 @@ open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.Product as Prod using (_,_; _×_; uncurry; <_,_>)
 open import Function.Base using (id; _∘_)
 open import Level using (_⊔_)
-open import Relation.Binary as B using (Rel; _⇒_)
+open import Relation.Binary.Definitions as B
 open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
diff --git a/src/Data/Vec/Relation/Unary/AllPairs/Core.agda b/src/Data/Vec/Relation/Unary/AllPairs/Core.agda
index a101f14057..bb094cc5fb 100644
--- a/src/Data/Vec/Relation/Unary/AllPairs/Core.agda
+++ b/src/Data/Vec/Relation/Unary/AllPairs/Core.agda
@@ -12,7 +12,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 
 module Data.Vec.Relation.Unary.AllPairs.Core
   {a ℓ} {A : Set a} (R : Rel A ℓ) where
diff --git a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda
index 672c9fa485..2158246fbc 100644
--- a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda
@@ -19,7 +19,7 @@ open import Data.Fin.Properties using (suc-injective)
 open import Data.Nat.Base using (zero; suc; _+_)
 open import Function.Base using (_∘_)
 open import Level using (Level)
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≢_)
 
 private
diff --git a/src/Data/Vec/Relation/Unary/Linked.agda b/src/Data/Vec/Relation/Unary/Linked.agda
index 2ca0182f03..abd9a5b4ef 100644
--- a/src/Data/Vec/Relation/Unary/Linked.agda
+++ b/src/Data/Vec/Relation/Unary/Linked.agda
@@ -14,7 +14,8 @@ open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.Product as Prod using (_,_; _×_; uncurry; <_,_>)
 open import Function.Base using (id; _∘_)
 open import Level using (Level; _⊔_)
-open import Relation.Binary as B using (Rel; _⇒_)
+open import Relation.Binary.Core using (Rel; _⇒_)
+open import Relation.Binary.Definitions as B
 open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
index 340b6b81a2..c32e4c8df6 100644
--- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
@@ -19,7 +19,9 @@ open import Data.Nat.Base using (ℕ; zero; suc; NonZero)
 open import Data.Nat.Properties using (<-pred)
 open import Level using (Level)
 open import Function.Base using (_∘_; flip; _on_)
-open import Relation.Binary using (Rel; Transitive; DecSetoid)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Transitive)
+open import Relation.Binary.Bundles using (DecSetoid)
 open import Relation.Binary.PropositionalEquality.Core using (_≢_)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Nullary.Decidable using (yes; no; does)
diff --git a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda
index 9ab4cd57f7..fee62c2306 100644
--- a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda
@@ -20,7 +20,8 @@ open import Data.Product using (_×_; _,_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (≡⇒≡×≡)
 open import Function.Base using (id; _∘_)
 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)
 open import Relation.Binary.PropositionalEquality
   using (refl; _≡_; _≢_; sym; setoid)
 open import Relation.Unary using (Pred; Decidable)
diff --git a/src/Data/Vec/Relation/Unary/Unique/Setoid.agda b/src/Data/Vec/Relation/Unary/Unique/Setoid.agda
index 3f0db9d300..76610e0485 100644
--- a/src/Data/Vec/Relation/Unary/Unique/Setoid.agda
+++ b/src/Data/Vec/Relation/Unary/Unique/Setoid.agda
@@ -6,7 +6,8 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary using (Rel; Setoid)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles using (Setoid)
 
 module Data.Vec.Relation.Unary.Unique.Setoid {a ℓ} (S : Setoid a ℓ) where
 
diff --git a/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda b/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda
index 4c433c04f6..cb276cae9a 100644
--- a/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda
@@ -18,7 +18,8 @@ import Data.Vec.Relation.Unary.AllPairs.Properties as AllPairsₚ
 open import Data.Nat.Base using (ℕ; _+_)
 open import Function.Base using (_∘_; id)
 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)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Nullary.Negation using (contradiction; contraposition)
 
diff --git a/src/Data/Word/Base.agda b/src/Data/Word/Base.agda
index 1dcaea5731..81a7ae6666 100644
--- a/src/Data/Word/Base.agda
+++ b/src/Data/Word/Base.agda
@@ -11,7 +11,7 @@ module Data.Word.Base where
 open import Level using (zero)
 import Data.Nat.Base as ℕ
 open import Function.Base using (_on_)
-open import Relation.Binary using (Rel)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality
 
 ------------------------------------------------------------------------
diff --git a/src/Effect/Monad/Partiality/All.agda b/src/Effect/Monad/Partiality/All.agda
index 2954a5da2b..c2db61c031 100644
--- a/src/Effect/Monad/Partiality/All.agda
+++ b/src/Effect/Monad/Partiality/All.agda
@@ -13,7 +13,8 @@ open import Effect.Monad.Partiality as Partiality using (_⊥; ⇒≈)
 open import Codata.Musical.Notation
 open import Function.Base using (flip; _∘_)
 open import Level
-open import Relation.Binary using (_Respects_; IsEquivalence)
+open import Relation.Binary.Definitions using (_Respects_)
+open import Relation.Binary.Structures using (IsEquivalence)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 open Partiality._⊥
diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda
index d53142c532..c41305f9e9 100644
--- a/src/Function/Endomorphism/Propositional.agda
+++ b/src/Function/Endomorphism/Propositional.agda
@@ -20,7 +20,7 @@ open import Data.Product.Base using (_,_)
 
 open import Function.Base using (id; _∘′_; _∋_)
 open import Function.Equality using (_⟨$⟩_)
-open import Relation.Binary using (_Preserves_⟶_)
+open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
 import Relation.Binary.PropositionalEquality.Properties as P
 
diff --git a/src/Function/Properties/Equivalence.agda b/src/Function/Properties/Equivalence.agda
index 066316c01b..beaa7d8940 100644
--- a/src/Function/Properties/Equivalence.agda
+++ b/src/Function/Properties/Equivalence.agda
@@ -11,7 +11,8 @@ module Function.Properties.Equivalence where
 
 open import Function.Bundles using (Equivalence; _⇔_)
 open import Level
-open import Relation.Binary using (Setoid; IsEquivalence)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
 import Relation.Binary.PropositionalEquality.Properties as Eq
 
 import Function.Construct.Identity as Identity
diff --git a/src/Function/Properties/Inverse.agda b/src/Function/Properties/Inverse.agda
index 6ef0b45af0..efc557d507 100644
--- a/src/Function/Properties/Inverse.agda
+++ b/src/Function/Properties/Inverse.agda
@@ -13,7 +13,8 @@ open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Function.Bundles
 open import Level using (Level)
-open import Relation.Binary using (Setoid; IsEquivalence)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
 import Relation.Binary.PropositionalEquality.Core as P
 import Relation.Binary.PropositionalEquality.Properties as P
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
diff --git a/src/Function/Properties/RightInverse.agda b/src/Function/Properties/RightInverse.agda
index f5aa05d9df..12dcbf69e1 100644
--- a/src/Function/Properties/RightInverse.agda
+++ b/src/Function/Properties/RightInverse.agda
@@ -13,7 +13,8 @@ open import Function.Bundles
 open import Function.Consequences using (inverseʳ⇒surjective)
 open import Level using (Level)
 open import Data.Product
-open import Relation.Binary using (Setoid; IsEquivalence)
+open import Relation.Binary.Bundles using (Setoid)
+open import Relation.Binary.Structures using (IsEquivalence)
 
 private
   variable
diff --git a/src/Reflection/AST/Abstraction.agda b/src/Reflection/AST/Abstraction.agda
index 3bf47f81a4..43fb2f8302 100644
--- a/src/Reflection/AST/Abstraction.agda
+++ b/src/Reflection/AST/Abstraction.agda
@@ -13,7 +13,7 @@ open import Data.String.Properties as String           using (_≟_)
 open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
 open import Level
 open import Relation.Nullary.Decidable                 using (Dec; map′; _×-dec_)
-open import Relation.Binary                            using (DecidableEquality)
+open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
 
 private
diff --git a/src/Reflection/AST/AlphaEquality.agda b/src/Reflection/AST/AlphaEquality.agda
index 2c8637e9dc..4849470d50 100644
--- a/src/Reflection/AST/AlphaEquality.agda
+++ b/src/Reflection/AST/AlphaEquality.agda
@@ -8,12 +8,12 @@
 
 module Reflection.AST.AlphaEquality where
 
-open import Data.Bool.Base             using (Bool; true; false; _∧_)
-open import Data.List.Base             using ([]; _∷_)
-open import Data.Nat.Base as ℕ        using (ℕ; zero; suc; _≡ᵇ_)
-open import Data.Product.Base          using (_,_)
-open import Relation.Nullary.Decidable using (⌊_⌋)
-open import Relation.Binary            using (DecidableEquality)
+open import Data.Bool.Base                using (Bool; true; false; _∧_)
+open import Data.List.Base                using ([]; _∷_)
+open import Data.Nat.Base as ℕ            using (ℕ; zero; suc; _≡ᵇ_)
+open import Data.Product.Base             using (_,_)
+open import Relation.Nullary.Decidable    using (⌊_⌋)
+open import Relation.Binary.Definitions   using (DecidableEquality)
 
 open import Reflection.AST.Abstraction
 open import Reflection.AST.Argument
diff --git a/src/Reflection/AST/Argument.agda b/src/Reflection/AST/Argument.agda
index fe95ccedc1..b97ec90f77 100644
--- a/src/Reflection/AST/Argument.agda
+++ b/src/Reflection/AST/Argument.agda
@@ -11,7 +11,7 @@ module Reflection.AST.Argument where
 open import Data.List.Base as List                     using (List; []; _∷_)
 open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
 open import Relation.Nullary.Decidable                 using (Dec; map′; _×-dec_)
-open import Relation.Binary                            using (DecidableEquality)
+open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
 open import Level
 
diff --git a/src/Reflection/AST/Argument/Information.agda b/src/Reflection/AST/Argument/Information.agda
index e0f5be24a5..66fec3be77 100644
--- a/src/Reflection/AST/Argument/Information.agda
+++ b/src/Reflection/AST/Argument/Information.agda
@@ -10,7 +10,7 @@ module Reflection.AST.Argument.Information where
 
 open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
 open import Relation.Nullary.Decidable                 using (map′; _×-dec_)
-open import Relation.Binary                            using (DecidableEquality)
+open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
 
 open import Reflection.AST.Argument.Modality as Modality using (Modality)
diff --git a/src/Reflection/AST/Argument/Modality.agda b/src/Reflection/AST/Argument/Modality.agda
index 02e481af58..489247031e 100644
--- a/src/Reflection/AST/Argument/Modality.agda
+++ b/src/Reflection/AST/Argument/Modality.agda
@@ -10,7 +10,7 @@ module Reflection.AST.Argument.Modality where
 
 open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
 open import Relation.Nullary.Decidable                 using (map′; _×-dec_)
-open import Relation.Binary                            using (DecidableEquality)
+open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
 
 open import Reflection.AST.Argument.Relevance as Relevance using (Relevance)
diff --git a/src/Reflection/AST/Argument/Quantity.agda b/src/Reflection/AST/Argument/Quantity.agda
index 5b3b98e092..bc79d74b3c 100644
--- a/src/Reflection/AST/Argument/Quantity.agda
+++ b/src/Reflection/AST/Argument/Quantity.agda
@@ -9,7 +9,7 @@
 module Reflection.AST.Argument.Quantity where
 
 open import Relation.Nullary                           using (yes; no)
-open import Relation.Binary                            using (DecidableEquality)
+open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 ------------------------------------------------------------------------
diff --git a/src/Reflection/AST/Argument/Relevance.agda b/src/Reflection/AST/Argument/Relevance.agda
index 03ba0f4f0a..3ac78cf765 100644
--- a/src/Reflection/AST/Argument/Relevance.agda
+++ b/src/Reflection/AST/Argument/Relevance.agda
@@ -9,7 +9,7 @@
 module Reflection.AST.Argument.Relevance where
 
 open import Relation.Nullary                           using (yes; no)
-open import Relation.Binary                            using (DecidableEquality)
+open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 ------------------------------------------------------------------------
diff --git a/src/Reflection/AST/Argument/Visibility.agda b/src/Reflection/AST/Argument/Visibility.agda
index b5e9236043..b384609c93 100644
--- a/src/Reflection/AST/Argument/Visibility.agda
+++ b/src/Reflection/AST/Argument/Visibility.agda
@@ -9,7 +9,7 @@
 module Reflection.AST.Argument.Visibility where
 
 open import Relation.Nullary                           using (yes; no)
-open import Relation.Binary                            using (DecidableEquality)
+open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 ------------------------------------------------------------------------
diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda
index ea005eebd3..b5b5b32700 100644
--- a/src/Reflection/AST/Definition.agda
+++ b/src/Reflection/AST/Definition.agda
@@ -12,7 +12,7 @@ import Data.List.Properties as Listₚ                   using (≡-dec)
 import Data.Nat.Properties as ℕₚ                       using (_≟_)
 open import Data.Product.Base                          using (_×_; <_,_>; uncurry)
 open import Relation.Nullary.Decidable                 using (map′; _×-dec_; yes; no)
-open import Relation.Binary                            using (DecidableEquality)
+open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
 
 import Reflection.AST.Argument as Arg
diff --git a/src/Reflection/AST/Literal.agda b/src/Reflection/AST/Literal.agda
index f400c9f1dc..00ac5cc652 100644
--- a/src/Reflection/AST/Literal.agda
+++ b/src/Reflection/AST/Literal.agda
@@ -18,7 +18,7 @@ import Reflection.AST.Meta as Meta
 import Reflection.AST.Name as Name
 open import Relation.Nullary                           using (yes; no)
 open import Relation.Nullary.Decidable                 using (map′; isYes)
-open import Relation.Binary                            using (DecidableEquality)
+open import Relation.Binary.Definitions                using (DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
 ------------------------------------------------------------------------
diff --git a/src/Reflection/AST/Meta.agda b/src/Reflection/AST/Meta.agda
index 56bda50d31..682a52c8ca 100644
--- a/src/Reflection/AST/Meta.agda
+++ b/src/Reflection/AST/Meta.agda
@@ -11,7 +11,8 @@ module Reflection.AST.Meta where
 import Data.Nat.Properties as ℕₚ                       using (_≟_)
 open import Function.Base                              using (_on_)
 open import Relation.Nullary.Decidable                 using (map′)
-open import Relation.Binary                            using (Rel; Decidable; DecidableEquality)
+open import Relation.Binary.Core                       using (Rel)
+open import Relation.Binary.Definitions                using (Decidable; DecidableEquality)
 import Relation.Binary.Construct.On as On
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 
diff --git a/src/Reflection/AST/Name.agda b/src/Reflection/AST/Name.agda
index fb31bc777a..ac478443fb 100644
--- a/src/Reflection/AST/Name.agda
+++ b/src/Reflection/AST/Name.agda
@@ -13,7 +13,8 @@ import Data.Product.Properties as Prodₚ using (≡-dec)
 import Data.Word.Properties as Wₚ       using (_≟_)
 open import Function.Base               using (_on_)
 open import Relation.Nullary.Decidable                 using (map′)
-open import Relation.Binary                            using (Rel; Decidable; DecidableEquality)
+open import Relation.Binary.Core                       using (Rel)
+open import Relation.Binary.Definitions                using (Decidable; DecidableEquality)
 open import Relation.Binary.Construct.On               using (decidable)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 
diff --git a/src/Reflection/AST/Term.agda b/src/Reflection/AST/Term.agda
index b22641b2a9..33ef68d6f0 100644
--- a/src/Reflection/AST/Term.agda
+++ b/src/Reflection/AST/Term.agda
@@ -8,16 +8,16 @@
 
 module Reflection.AST.Term where
 
-open import Data.List.Base as List  hiding (_++_)
-open import Data.List.Properties    using (∷-dec)
-open import Data.Nat as ℕ           using (ℕ; zero; suc)
-open import Data.Product.Base       using (_×_; _,_; <_,_>; uncurry; map₁)
-open import Data.Product.Properties using (,-injective)
-open import Data.Maybe.Base         using (Maybe; just; nothing)
-open import Data.String.Base    using (String)
-open import Data.String.Properties as String hiding (_≟_)
+open import Data.List.Base as List                     hiding (_++_)
+open import Data.List.Properties                       using (∷-dec)
+open import Data.Nat as ℕ                              using (ℕ; zero; suc)
+open import Data.Product.Base                          using (_×_; _,_; <_,_>; uncurry; map₁)
+open import Data.Product.Properties                    using (,-injective)
+open import Data.Maybe.Base                            using (Maybe; just; nothing)
+open import Data.String.Base                           using (String)
+open import Data.String.Properties as String           hiding (_≟_)
 open import Relation.Nullary.Decidable                 using (map′; _×-dec_; yes; no)
-open import Relation.Binary                            using (Decidable; DecidableEquality)
+open import Relation.Binary.Definitions                using (Decidable; DecidableEquality)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
 
 open import Reflection.AST.Abstraction