diff --git a/src/Algebra/Construct/LiftedChoice.agda b/src/Algebra/Construct/LiftedChoice.agda
index 83cf2110c3..91d3f1d546 100644
--- a/src/Algebra/Construct/LiftedChoice.agda
+++ b/src/Algebra/Construct/LiftedChoice.agda
@@ -16,7 +16,7 @@ open import Relation.Nullary using (¬_; yes; no)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Product.Base using (_×_; _,_)
 open import Level using (Level; _⊔_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Unary using (Pred)
 
 import Relation.Binary.Reasoning.Setoid as EqReasoning
diff --git a/src/Algebra/Operations/CommutativeMonoid.agda b/src/Algebra/Operations/CommutativeMonoid.agda
index 3c94a94419..52d72af156 100644
--- a/src/Algebra/Operations/CommutativeMonoid.agda
+++ b/src/Algebra/Operations/CommutativeMonoid.agda
@@ -12,7 +12,7 @@ open import Data.Fin.Base using (Fin; zero)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Function.Base using (_∘_)
 open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 module Algebra.Operations.CommutativeMonoid
   {s₁ s₂} (CM : CommutativeMonoid s₁ s₂)
diff --git a/src/Algebra/Properties/CommutativeMonoid/Mult/TCOptimised.agda b/src/Algebra/Properties/CommutativeMonoid/Mult/TCOptimised.agda
index b61a3e987e..8985fb21cb 100644
--- a/src/Algebra/Properties/CommutativeMonoid/Mult/TCOptimised.agda
+++ b/src/Algebra/Properties/CommutativeMonoid/Mult/TCOptimised.agda
@@ -10,7 +10,6 @@
 open import Algebra.Bundles using (CommutativeMonoid)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
 module Algebra.Properties.CommutativeMonoid.Mult.TCOptimised
   {a ℓ} (M : CommutativeMonoid a ℓ) where
diff --git a/src/Algebra/Properties/CommutativeMonoid/Sum.agda b/src/Algebra/Properties/CommutativeMonoid/Sum.agda
index f70b965130..6cb417bc69 100644
--- a/src/Algebra/Properties/CommutativeMonoid/Sum.agda
+++ b/src/Algebra/Properties/CommutativeMonoid/Sum.agda
@@ -14,7 +14,7 @@ open import Data.Fin.Permutation as Perm using (Permutation; _⟨$⟩ˡ_; _⟨$
 open import Data.Fin.Patterns using (0F)
 open import Data.Vec.Functional
 open import Function.Base using (_∘_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Nullary.Negation using (contradiction)
 
 module Algebra.Properties.CommutativeMonoid.Sum
diff --git a/src/Algebra/Properties/Monoid/Mult.agda b/src/Algebra/Properties/Monoid/Mult.agda
index f74404e886..1a9e346585 100644
--- a/src/Algebra/Properties/Monoid/Mult.agda
+++ b/src/Algebra/Properties/Monoid/Mult.agda
@@ -9,7 +9,7 @@
 open import Algebra.Bundles using (Monoid)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 module Algebra.Properties.Monoid.Mult {a ℓ} (M : Monoid a ℓ) where
 
diff --git a/src/Algebra/Properties/Monoid/Mult/TCOptimised.agda b/src/Algebra/Properties/Monoid/Mult/TCOptimised.agda
index 86c4ac566c..ded5f1339e 100644
--- a/src/Algebra/Properties/Monoid/Mult/TCOptimised.agda
+++ b/src/Algebra/Properties/Monoid/Mult/TCOptimised.agda
@@ -10,7 +10,7 @@
 open import Algebra.Bundles using (Monoid)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 module Algebra.Properties.Monoid.Mult.TCOptimised
   {a ℓ} (M : Monoid a ℓ) where
diff --git a/src/Algebra/Properties/Semiring/Exp.agda b/src/Algebra/Properties/Semiring/Exp.agda
index df467b1f66..1d50298ca5 100644
--- a/src/Algebra/Properties/Semiring/Exp.agda
+++ b/src/Algebra/Properties/Semiring/Exp.agda
@@ -9,7 +9,7 @@
 open import Algebra
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Data.Nat.Properties as ℕ
 
 module Algebra.Properties.Semiring.Exp
diff --git a/src/Algebra/Solver/CommutativeMonoid.agda b/src/Algebra/Solver/CommutativeMonoid.agda
index 623beaeebd..7e4b14b18c 100644
--- a/src/Algebra/Solver/CommutativeMonoid.agda
+++ b/src/Algebra/Solver/CommutativeMonoid.agda
@@ -27,7 +27,7 @@ import Relation.Binary.Reflection as Reflection
 import Relation.Nullary.Decidable as Dec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
-open import Relation.Binary.PropositionalEquality as P using (_≡_; decSetoid)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Nullary.Decidable using (Dec)
 
 open CommutativeMonoid M
diff --git a/src/Algebra/Solver/CommutativeMonoid/Example.agda b/src/Algebra/Solver/CommutativeMonoid/Example.agda
index 83351df044..e59f5b1e1f 100644
--- a/src/Algebra/Solver/CommutativeMonoid/Example.agda
+++ b/src/Algebra/Solver/CommutativeMonoid/Example.agda
@@ -8,7 +8,7 @@
 
 module Algebra.Solver.CommutativeMonoid.Example where
 
-open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 open import Data.Bool.Base using (_∨_)
 open import Data.Bool.Properties using (∨-commutativeMonoid)
diff --git a/src/Algebra/Solver/Monoid.agda b/src/Algebra/Solver/Monoid.agda
index 3006374347..bf066f7745 100644
--- a/src/Algebra/Solver/Monoid.agda
+++ b/src/Algebra/Solver/Monoid.agda
@@ -22,7 +22,7 @@ open import Data.Vec.Base using (Vec; lookup)
 open import Function.Base using (_∘_; _$_)
 open import Relation.Binary using (Decidable)
 
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.Reflection
 open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec
diff --git a/src/Algebra/Solver/Ring.agda b/src/Algebra/Solver/Ring.agda
index a1ea98ead3..e103b7a70e 100644
--- a/src/Algebra/Solver/Ring.agda
+++ b/src/Algebra/Solver/Ring.agda
@@ -42,7 +42,7 @@ open import Algebra.Properties.Semiring.Exp semiring
 open import Relation.Binary
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Binary.Reasoning.Setoid setoid
-import Relation.Binary.PropositionalEquality as PropEq
+import Relation.Binary.PropositionalEquality.Core as PropEq
 import Relation.Binary.Reflection as Reflection
 
 open import Data.Nat.Base using (ℕ; suc; zero)
diff --git a/src/Algebra/Solver/Ring/NaturalCoefficients.agda b/src/Algebra/Solver/Ring/NaturalCoefficients.agda
index 95af2b0a33..fdd0a65e6b 100644
--- a/src/Algebra/Solver/Ring/NaturalCoefficients.agda
+++ b/src/Algebra/Solver/Ring/NaturalCoefficients.agda
@@ -14,7 +14,7 @@ open import Algebra.Solver.Ring.AlmostCommutativeRing
 open import Data.Nat.Base as ℕ
 open import Data.Product.Base using (module Σ)
 open import Function.Base using (id)
-open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 module Algebra.Solver.Ring.NaturalCoefficients
   {r₁ r₂} (R : CommutativeSemiring r₁ r₂)
diff --git a/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda b/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda
index df01719174..84003922a0 100644
--- a/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda
+++ b/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda
@@ -20,7 +20,7 @@ import Algebra.Properties.Semiring.Mult as SemiringMultiplication
 open import Data.Maybe.Base using (Maybe; map)
 open import Data.Nat using (_≟_)
 open import Relation.Binary.Consequences using (dec⇒weaklyDec)
-import Relation.Binary.PropositionalEquality as P
+import Relation.Binary.PropositionalEquality.Core as P
 
 open CommutativeSemiring R
 open SemiringMultiplication semiring
diff --git a/src/Codata/Guarded/Stream/Properties.agda b/src/Codata/Guarded/Stream/Properties.agda
index 3e4bd83dcb..29ea54bb1d 100644
--- a/src/Codata/Guarded/Stream/Properties.agda
+++ b/src/Codata/Guarded/Stream/Properties.agda
@@ -20,7 +20,7 @@ open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂)
 open import Data.Vec.Base as Vec using (Vec; _∷_)
 open import Function.Base using (const; flip; id; _∘′_; _$′_; _⟨_⟩_; _∘₂′_)
 open import Level using (Level)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; cong; cong₂)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; cong; cong₂)
 
 private
   variable
diff --git a/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda b/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda
index c2d44f8145..3f610599a5 100644
--- a/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda
+++ b/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda
@@ -13,7 +13,8 @@ open import Data.Nat.Base using (ℕ; zero; suc)
 open import Function.Base using (_∘_; _on_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as P
 
 private
   variable
diff --git a/src/Codata/Musical/Cofin.agda b/src/Codata/Musical/Cofin.agda
index 082a6848dd..bc901ef194 100644
--- a/src/Codata/Musical/Cofin.agda
+++ b/src/Codata/Musical/Cofin.agda
@@ -12,7 +12,7 @@ open import Codata.Musical.Notation
 open import Codata.Musical.Conat as Conat using (Coℕ; suc; ∞ℕ)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Fin.Base using (Fin; zero; suc)
-open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_ ; refl)
 open import Function.Base using (_∋_)
 
 ------------------------------------------------------------------------
diff --git a/src/Codata/Musical/Colist/Infinite-merge.agda b/src/Codata/Musical/Colist/Infinite-merge.agda
index 9c859bcf26..677024808a 100644
--- a/src/Codata/Musical/Colist/Infinite-merge.agda
+++ b/src/Codata/Musical/Colist/Infinite-merge.agda
@@ -23,7 +23,7 @@ open import Function.Inverse as Inv using (_↔_; Inverse; inverse)
 import Function.Related as Related
 open import Function.Related.TypeIsomorphisms
 import Induction.WellFounded as WF
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.Construct.On as On
 
 ------------------------------------------------------------------------
diff --git a/src/Codata/Musical/Conat.agda b/src/Codata/Musical/Conat.agda
index f8c1490a40..d8e76d90be 100644
--- a/src/Codata/Musical/Conat.agda
+++ b/src/Codata/Musical/Conat.agda
@@ -12,7 +12,7 @@ open import Codata.Musical.Notation
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Function.Base using (_∋_)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 ------------------------------------------------------------------------
 -- Re-exporting the type and basic operations
diff --git a/src/Codata/Musical/Covec.agda b/src/Codata/Musical/Covec.agda
index 48cc1910e8..88b15c070b 100644
--- a/src/Codata/Musical/Covec.agda
+++ b/src/Codata/Musical/Covec.agda
@@ -18,7 +18,7 @@ open import Data.Product using (_,_)
 open import Function.Base using (_∋_)
 open import Level using (Level)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 private
   variable
diff --git a/src/Codata/Musical/Stream.agda b/src/Codata/Musical/Stream.agda
index 9b00ba510f..a51f8f41b5 100644
--- a/src/Codata/Musical/Stream.agda
+++ b/src/Codata/Musical/Stream.agda
@@ -14,7 +14,7 @@ open import Codata.Musical.Colist using (Colist; []; _∷_)
 open import Data.Vec.Base using (Vec; []; _∷_)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 private
   variable
diff --git a/src/Codata/Sized/Colist.agda b/src/Codata/Sized/Colist.agda
index 4f916fbc68..e57a5b632e 100644
--- a/src/Codata/Sized/Colist.agda
+++ b/src/Codata/Sized/Colist.agda
@@ -27,7 +27,7 @@ open import Codata.Sized.Cowriter as CW using (Cowriter; _∷_)
 open import Codata.Sized.Delay as Delay using (Delay ; now ; later)
 open import Codata.Sized.Stream using (Stream ; _∷_)
 
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 private
   variable
diff --git a/src/Codata/Sized/Colist/Bisimilarity.agda b/src/Codata/Sized/Colist/Bisimilarity.agda
index 0a9f76306b..9efbcebbca 100644
--- a/src/Codata/Sized/Colist/Bisimilarity.agda
+++ b/src/Codata/Sized/Colist/Bisimilarity.agda
@@ -16,7 +16,8 @@ open import Data.List.Base using (List; []; _∷_)
 open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
 open import Data.List.NonEmpty as List⁺  using (List⁺; _∷_)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as Eq
 
 private
   variable
diff --git a/src/Codata/Sized/Colist/Properties.agda b/src/Codata/Sized/Colist/Properties.agda
index dea697b088..de5925e482 100644
--- a/src/Codata/Sized/Colist/Properties.agda
+++ b/src/Codata/Sized/Colist/Properties.agda
@@ -31,7 +31,7 @@ open import Data.Product as Prod using (_×_; _,_; uncurry)
 open import Data.These.Base as These using (These; this; that; these)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Function.Base
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; [_])
+open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
 
 private
   variable
diff --git a/src/Codata/Sized/Covec/Bisimilarity.agda b/src/Codata/Sized/Covec/Bisimilarity.agda
index cbe55ecbf7..7610c41946 100644
--- a/src/Codata/Sized/Covec/Bisimilarity.agda
+++ b/src/Codata/Sized/Covec/Bisimilarity.agda
@@ -14,7 +14,7 @@ open import Codata.Sized.Thunk
 open import Codata.Sized.Conat hiding (_⊔_)
 open import Codata.Sized.Covec
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
 
 data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) (i : Size) :
            ∀ m n (xs : Covec A ∞ m) (ys : Covec B ∞ n) → Set (r ⊔ a ⊔ b) where
diff --git a/src/Codata/Sized/Covec/Properties.agda b/src/Codata/Sized/Covec/Properties.agda
index 139eba6029..08122efe0b 100644
--- a/src/Codata/Sized/Covec/Properties.agda
+++ b/src/Codata/Sized/Covec/Properties.agda
@@ -14,7 +14,7 @@ open import Codata.Sized.Conat
 open import Codata.Sized.Covec
 open import Codata.Sized.Covec.Bisimilarity
 open import Function.Base using (id; _∘_)
-open import Relation.Binary.PropositionalEquality as Eq
+open import Relation.Binary.PropositionalEquality.Core as Eq
 
 -- Functor laws
 
diff --git a/src/Codata/Sized/Cowriter/Bisimilarity.agda b/src/Codata/Sized/Cowriter/Bisimilarity.agda
index 846101b538..84ab0375c4 100644
--- a/src/Codata/Sized/Cowriter/Bisimilarity.agda
+++ b/src/Codata/Sized/Cowriter/Bisimilarity.agda
@@ -13,7 +13,8 @@ open import Size
 open import Codata.Sized.Thunk
 open import Codata.Sized.Cowriter
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as Eq
 
 private
   variable
diff --git a/src/Codata/Sized/Delay/Bisimilarity.agda b/src/Codata/Sized/Delay/Bisimilarity.agda
index 1143f15263..4d9f702acc 100644
--- a/src/Codata/Sized/Delay/Bisimilarity.agda
+++ b/src/Codata/Sized/Delay/Bisimilarity.agda
@@ -13,7 +13,7 @@ open import Codata.Sized.Thunk
 open import Codata.Sized.Delay
 open import Level
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
 
 data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) i :
            (xs : Delay A ∞) (ys : Delay B ∞) → Set (a ⊔ b ⊔ r) where
diff --git a/src/Codata/Sized/Delay/Properties.agda b/src/Codata/Sized/Delay/Properties.agda
index 5db7bafe7f..e491178c71 100644
--- a/src/Codata/Sized/Delay/Properties.agda
+++ b/src/Codata/Sized/Delay/Properties.agda
@@ -17,7 +17,7 @@ open import Codata.Sized.Conat.Bisimilarity as Coℕ using (zero ; suc)
 open import Codata.Sized.Delay
 open import Codata.Sized.Delay.Bisimilarity
 open import Function.Base using (id; _∘′_)
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
 
 module _ {a} {A : Set a} where
 
diff --git a/src/Codata/Sized/M/Bisimilarity.agda b/src/Codata/Sized/M/Bisimilarity.agda
index 1b8cbd3188..3a60a91d16 100644
--- a/src/Codata/Sized/M/Bisimilarity.agda
+++ b/src/Codata/Sized/M/Bisimilarity.agda
@@ -17,7 +17,7 @@ open import Data.Container.Relation.Binary.Pointwise using (Pointwise; _,_)
 open import Data.Product using (_,_)
 open import Function.Base using (_∋_)
 open import Relation.Binary
-import Relation.Binary.PropositionalEquality as P
+import Relation.Binary.PropositionalEquality.Core as P
 
 data Bisim {s p} (C : Container s p) (i : Size) : Rel (M C ∞) (s ⊔ p) where
   inf : ∀ {t u} → Pointwise C (Thunk^R (Bisim C) i) t u → Bisim C i (inf t) (inf u)
diff --git a/src/Codata/Sized/M/Properties.agda b/src/Codata/Sized/M/Properties.agda
index 3b26955e60..4161f4d1f1 100644
--- a/src/Codata/Sized/M/Properties.agda
+++ b/src/Codata/Sized/M/Properties.agda
@@ -18,7 +18,8 @@ import Data.Container.Morphism as Mp
 open import Data.Product as Prod using (_,_)
 open import Data.Product.Properties hiding (map-cong)
 open import Function.Base using (_$′_; _∘′_)
-import Relation.Binary.PropositionalEquality as P
+import Relation.Binary.PropositionalEquality.Core as P
+import Relation.Binary.PropositionalEquality.Properties as P
 
 open import Data.Container.Relation.Binary.Pointwise using (_,_)
 import Data.Container.Relation.Binary.Equality.Setoid as EqSetoid
diff --git a/src/Codata/Sized/Stream/Bisimilarity.agda b/src/Codata/Sized/Stream/Bisimilarity.agda
index 737e73c306..74419c7809 100644
--- a/src/Codata/Sized/Stream/Bisimilarity.agda
+++ b/src/Codata/Sized/Stream/Bisimilarity.agda
@@ -15,7 +15,8 @@ open import Level
 open import Data.List.NonEmpty as List⁺ using (_∷_)
 open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as Eq
 
 private
   variable
diff --git a/src/Codata/Sized/Stream/Properties.agda b/src/Codata/Sized/Stream/Properties.agda
index 539a6b7b20..51b0719c7d 100644
--- a/src/Codata/Sized/Stream/Properties.agda
+++ b/src/Codata/Sized/Stream/Properties.agda
@@ -24,7 +24,7 @@ open import Data.Product as Prod using (_,_)
 open import Data.Vec.Base as Vec using (_∷_)
 
 open import Function.Base using (id; _$_; _∘′_; const)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; _≢_)
 
 private
   variable
diff --git a/src/Data/AVL/Indexed/WithK.agda b/src/Data/AVL/Indexed/WithK.agda
index 4a5de070f0..15da148fa2 100644
--- a/src/Data/AVL/Indexed/WithK.agda
+++ b/src/Data/AVL/Indexed/WithK.agda
@@ -7,7 +7,7 @@
 {-# OPTIONS --with-K --safe #-}
 
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; subst)
 
 module Data.AVL.Indexed.WithK
        {k r} (Key : Set k) {_<_ : Rel Key r}
diff --git a/src/Data/AVL/IndexedMap.agda b/src/Data/AVL/IndexedMap.agda
index 64a0d5c36a..25bccdee5f 100644
--- a/src/Data/AVL/IndexedMap.agda
+++ b/src/Data/AVL/IndexedMap.agda
@@ -8,7 +8,7 @@
 
 open import Data.Product as Prod
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality using (_≡_; cong; subst)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst)
 import Data.Tree.AVL.Value
 
 module Data.AVL.IndexedMap
diff --git a/src/Data/Bool.agda b/src/Data/Bool.agda
index 909b659f22..5fdbcc45e0 100644
--- a/src/Data/Bool.agda
+++ b/src/Data/Bool.agda
@@ -10,8 +10,7 @@ module Data.Bool where
 
 open import Relation.Nullary
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as PropEq
-  using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 ------------------------------------------------------------------------
 -- The boolean type and some operations
diff --git a/src/Data/Bool/Properties.agda b/src/Data/Bool/Properties.agda
index ef963f6511..56448d8e2b 100644
--- a/src/Data/Bool/Properties.agda
+++ b/src/Data/Bool/Properties.agda
@@ -22,7 +22,8 @@ open import Function.Equivalence
 open import Induction.WellFounded using (WellFounded; Acc; acc)
 open import Level using (Level; 0ℓ)
 open import Relation.Binary hiding (_⇔_)
-open import Relation.Binary.PropositionalEquality hiding ([_])
+open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality.Properties
 open import Relation.Nullary.Reflects using (ofʸ; ofⁿ)
 open import Relation.Nullary.Decidable.Core using (True; does; proof; yes; no)
 import Relation.Unary as U
diff --git a/src/Data/Char/Properties.agda b/src/Data/Char/Properties.agda
index 1db34c4f0b..2bbf63ab17 100644
--- a/src/Data/Char/Properties.agda
+++ b/src/Data/Char/Properties.agda
@@ -22,8 +22,9 @@ import Relation.Binary.Construct.On as On
 import Relation.Binary.Construct.Subst.Equality as Subst
 import Relation.Binary.Construct.Closure.Reflexive as Refl
 import Relation.Binary.Construct.Closure.Reflexive.Properties as Reflₚ
-open import Relation.Binary.PropositionalEquality as PropEq
+open import Relation.Binary.PropositionalEquality.Core as PropEq
   using (_≡_; _≢_; refl; cong; sym; trans; subst)
+import Relation.Binary.PropositionalEquality.Properties as PropEq
 
 ------------------------------------------------------------------------
 -- Primitive properties
diff --git a/src/Data/Container/Indexed/WithK.agda b/src/Data/Container/Indexed/WithK.agda
index 565b14fcdd..ca5f18205d 100644
--- a/src/Data/Container/Indexed/WithK.agda
+++ b/src/Data/Container/Indexed/WithK.agda
@@ -19,7 +19,7 @@ open import Data.Product as Prod hiding (map)
 open import Function.Base renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
 open import Level
 open import Relation.Unary using (Pred; _⊆_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
 open import Relation.Binary.HeterogeneousEquality as H using (_≅_; refl)
 open import Relation.Binary.Indexed.Heterogeneous
 
diff --git a/src/Data/Container/Relation/Binary/Pointwise.agda b/src/Data/Container/Relation/Binary/Pointwise.agda
index 8a022a072c..2b0b966b3d 100644
--- a/src/Data/Container/Relation/Binary/Pointwise.agda
+++ b/src/Data/Container/Relation/Binary/Pointwise.agda
@@ -12,7 +12,7 @@ open import Data.Product using (_,_; Σ-syntax; -,_; proj₁; proj₂)
 open import Function
 open import Level using (_⊔_)
 open import Relation.Binary using (REL; _⇒_)
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; subst; cong)
 
 open import Data.Container.Core using (Container; ⟦_⟧)
diff --git a/src/Data/Container/Relation/Binary/Pointwise/Properties.agda b/src/Data/Container/Relation/Binary/Pointwise/Properties.agda
index 24e48a74a3..3092037901 100644
--- a/src/Data/Container/Relation/Binary/Pointwise/Properties.agda
+++ b/src/Data/Container/Relation/Binary/Pointwise/Properties.agda
@@ -14,7 +14,7 @@ open import Data.Container.Relation.Binary.Pointwise
 open import Data.Product using (_,_; Σ-syntax; -,_)
 open import Level using (_⊔_)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; subst; cong)
 
 module _ {s p x r} {X : Set x} (C : Container s p) (R : Rel X r) where
diff --git a/src/Data/Digit.agda b/src/Data/Digit.agda
index 7e7c1c7555..60557b142a 100644
--- a/src/Data/Digit.agda
+++ b/src/Data/Digit.agda
@@ -21,7 +21,7 @@ open import Data.Nat.DivMod
 open import Data.Nat.Induction
 open import Relation.Nullary.Decidable using (True; does; toWitness)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
 open import Function.Base using (_$_)
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Digit/Properties.agda b/src/Data/Digit/Properties.agda
index 355467ec39..37ead69a28 100644
--- a/src/Data/Digit/Properties.agda
+++ b/src/Data/Digit/Properties.agda
@@ -16,7 +16,7 @@ open import Data.Vec.Relation.Unary.Unique.Propositional using (Unique)
 import Data.Vec.Relation.Unary.Unique.Propositional.Properties as Uniqueₚ
 open import Data.Vec.Relation.Unary.AllPairs using (allPairs?)
 open import Relation.Nullary.Decidable using (True; from-yes; ¬?)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Function.Base using (_∘_)
 
 module Data.Digit.Properties where
diff --git a/src/Data/Fin/Substitution/Example.agda b/src/Data/Fin/Substitution/Example.agda
index f4b42438e5..8b3c903a7c 100644
--- a/src/Data/Fin/Substitution/Example.agda
+++ b/src/Data/Fin/Substitution/Example.agda
@@ -14,7 +14,7 @@ open import Data.Fin.Substitution.Lemmas
 open import Data.Nat.Base hiding (_/_)
 open import Data.Fin.Base using (Fin)
 open import Data.Vec.Base
-open import Relation.Binary.PropositionalEquality as PropEq
+open import Relation.Binary.PropositionalEquality.Core as PropEq
   using (_≡_; refl; sym; cong; cong₂)
 open PropEq.≡-Reasoning
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
diff --git a/src/Data/Fin/Substitution/Lemmas.agda b/src/Data/Fin/Substitution/Lemmas.agda
index 3747f21018..6109f28726 100644
--- a/src/Data/Fin/Substitution/Lemmas.agda
+++ b/src/Data/Fin/Substitution/Lemmas.agda
@@ -15,7 +15,7 @@ open import Data.Fin.Base using (Fin; zero; suc; lift)
 open import Data.Vec.Base
 import Data.Vec.Properties as VecProp
 open import Function.Base as Fun using (_∘_; _$_; flip)
-open import Relation.Binary.PropositionalEquality as PropEq
+open import Relation.Binary.PropositionalEquality.Core as PropEq
   using (_≡_; refl; sym; cong; cong₂)
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
   using (Star; ε; _◅_; _▻_)
diff --git a/src/Data/Graph/Acyclic.agda b/src/Data/Graph/Acyclic.agda
index 440424206a..d7b298f0ef 100644
--- a/src/Data/Graph/Acyclic.agda
+++ b/src/Data/Graph/Acyclic.agda
@@ -28,7 +28,7 @@ open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Function
 open import Relation.Nullary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 ------------------------------------------------------------------------
 -- A lemma
diff --git a/src/Data/Integer/Coprimality.agda b/src/Data/Integer/Coprimality.agda
index 35df9a1457..c3cfafcbff 100644
--- a/src/Data/Integer/Coprimality.agda
+++ b/src/Data/Integer/Coprimality.agda
@@ -16,7 +16,7 @@ import Data.Nat.Divisibility as ℕ
 open import Function.Base using (_on_)
 open import Level using (0ℓ)
 open import Relation.Binary using (Rel; Decidable; Symmetric)
-open import Relation.Binary.PropositionalEquality using (subst)
+open import Relation.Binary.PropositionalEquality.Core using (subst)
 
 ------------------------------------------------------------------------
 -- Definition
diff --git a/src/Data/List/Countdown.agda b/src/Data/List/Countdown.agda
index fde7439ebf..f1ef43ba8e 100644
--- a/src/Data/List/Countdown.agda
+++ b/src/Data/List/Countdown.agda
@@ -29,9 +29,10 @@ open import Data.Sum.Properties
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary
 open import Relation.Nullary.Decidable using (dec-true; dec-false)
-open import Relation.Binary.PropositionalEquality as PropEq
+open import Relation.Binary.PropositionalEquality.Core as PropEq
   using (_≡_; _≢_; refl; cong)
 open PropEq.≡-Reasoning
+import Relation.Binary.PropositionalEquality.Properties as PropEq
 
 private
   open module D = DecSetoid D
diff --git a/src/Data/List/Extrema/Core.agda b/src/Data/List/Extrema/Core.agda
index aa0b3f8da9..1fb59ae06d 100644
--- a/src/Data/List/Extrema/Core.agda
+++ b/src/Data/List/Extrema/Core.agda
@@ -18,7 +18,7 @@ import Algebra.Construct.NaturalChoice.Max as Max
 open import Data.Product using (_×_; _,_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Level using (Level)
-open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 open import Algebra.Construct.LiftedChoice
 
diff --git a/src/Data/List/Extrema/Nat.agda b/src/Data/List/Extrema/Nat.agda
index d1d8f3f4ac..6e2899b8e6 100644
--- a/src/Data/List/Extrema/Nat.agda
+++ b/src/Data/List/Extrema/Nat.agda
@@ -20,7 +20,7 @@ open import Data.List.Relation.Unary.Any as Any using (Any)
 open import Data.List.Relation.Unary.All as All using (All)
 open import Data.Product using (_×_; _,_; uncurry′)
 open import Level using (Level)
-open import Relation.Binary.PropositionalEquality using (_≢_)
+open import Relation.Binary.PropositionalEquality.Core using (_≢_)
 
 private
   variable
diff --git a/src/Data/List/Fresh/Membership/Setoid/Properties.agda b/src/Data/List/Fresh/Membership/Setoid/Properties.agda
index 52be3b0d60..0515b84efe 100644
--- a/src/Data/List/Fresh/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Fresh/Membership/Setoid/Properties.agda
@@ -21,7 +21,7 @@ open import Function.Base using (id; _∘′_; _$_)
 open import Relation.Nullary
 open import Relation.Unary as U using (Pred)
 import Relation.Binary as B
-import Relation.Binary.PropositionalEquality as P
+import Relation.Binary.PropositionalEquality.Core as P
 open import Relation.Nary
 
 open import Data.List.Fresh
diff --git a/src/Data/List/Fresh/Relation/Unary/All/Properties.agda b/src/Data/List/Fresh/Relation/Unary/All/Properties.agda
index cbad777b96..f2c47657b5 100644
--- a/src/Data/List/Fresh/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Fresh/Relation/Unary/All/Properties.agda
@@ -16,7 +16,7 @@ open import Function.Base using (_∘′_)
 open import Relation.Nullary
 open import Relation.Unary  as U
 open import Relation.Binary as B using (Rel)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
 open import Data.List.Fresh using (List#; []; cons; _∷#_; _#_)
 open import Data.List.Fresh.Relation.Unary.All
diff --git a/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda b/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda
index f185a2ef32..09ec3d5333 100644
--- a/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda
@@ -20,7 +20,7 @@ open import Relation.Nullary
 open import Relation.Unary  as U using (Pred)
 open import Relation.Binary as B using (Rel)
 open import Relation.Nary
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
 open import Data.List.Fresh
 open import Data.List.Fresh.Relation.Unary.All
diff --git a/src/Data/List/Membership/DecPropositional.agda b/src/Data/List/Membership/DecPropositional.agda
index 4380ff8ca2..a59ce42c67 100644
--- a/src/Data/List/Membership/DecPropositional.agda
+++ b/src/Data/List/Membership/DecPropositional.agda
@@ -7,7 +7,8 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary using (Decidable)
-open import Relation.Binary.PropositionalEquality using (_≡_; decSetoid)
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
 module Data.List.Membership.DecPropositional
   {a} {A : Set a} (_≟_ : Decidable (_≡_ {A = A})) where
diff --git a/src/Data/List/Membership/Propositional.agda b/src/Data/List/Membership/Propositional.agda
index 4a74db3d04..c1ae08761e 100644
--- a/src/Data/List/Membership/Propositional.agda
+++ b/src/Data/List/Membership/Propositional.agda
@@ -10,7 +10,8 @@
 module Data.List.Membership.Propositional {a} {A : Set a} where
 
 open import Data.List.Relation.Unary.Any using (Any)
-open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; setoid; subst)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; subst)
+open import Relation.Binary.PropositionalEquality.Properties using (setoid)
 
 import Data.List.Membership.Setoid as SetoidMembership
 
diff --git a/src/Data/List/Membership/Propositional/Properties/Core.agda b/src/Data/List/Membership/Propositional/Properties/Core.agda
index 55a03f454c..85ad85aab0 100644
--- a/src/Data/List/Membership/Propositional/Properties/Core.agda
+++ b/src/Data/List/Membership/Propositional/Properties/Core.agda
@@ -20,7 +20,7 @@ open import Data.List.Membership.Propositional
 open import Data.Product as Prod
   using (_,_; proj₁; proj₂; uncurry′; ∃; _×_)
 open import Level using (Level)
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl)
 open import Relation.Unary using (Pred; _⊆_)
 
diff --git a/src/Data/List/Membership/Propositional/Properties/WithK.agda b/src/Data/List/Membership/Propositional/Properties/WithK.agda
index 5909ec3e72..60a86ee5e3 100644
--- a/src/Data/List/Membership/Propositional/Properties/WithK.agda
+++ b/src/Data/List/Membership/Propositional/Properties/WithK.agda
@@ -14,7 +14,7 @@ open import Data.List.Relation.Unary.Unique.Propositional
 open import Data.List.Membership.Propositional
 import Data.List.Membership.Setoid.Properties as Membershipₛ
 open import Relation.Unary using (Irrelevant)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Properties as P
 open import Relation.Binary.PropositionalEquality.WithK
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Membership/Setoid/Properties.agda b/src/Data/List/Membership/Setoid/Properties.agda
index 919bf19ba6..47768eed76 100644
--- a/src/Data/List/Membership/Setoid/Properties.agda
+++ b/src/Data/List/Membership/Setoid/Properties.agda
@@ -27,7 +27,7 @@ open import Function.Base using (_$_; flip; _∘_; _∘′_; id)
 open import Function.Inverse using (_↔_)
 open import Level using (Level)
 open import Relation.Binary as B hiding (Decidable)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Unary as U using (Decidable; Pred)
 open import Relation.Nullary using (¬_; does; _because_; yes; no)
 open import Relation.Nullary.Reflects using (invert)
diff --git a/src/Data/List/NonEmpty.agda b/src/Data/List/NonEmpty.agda
index 9e9f189fb5..5ce7ff4be2 100644
--- a/src/Data/List/NonEmpty.agda
+++ b/src/Data/List/NonEmpty.agda
@@ -9,21 +9,7 @@
 module Data.List.NonEmpty where
 
 open import Level using (Level)
-open import Effect.Monad
-open import Data.Bool.Base using (Bool; false; true; not; T)
-open import Data.Bool.Properties
-open import Data.List.Base as List using (List; []; _∷_)
-open import Data.Maybe.Base using (Maybe ; nothing; just)
-open import Data.Nat.Base as ℕ
-open import Data.Product as Prod using (∃; _×_; proj₁; proj₂; _,_; -,_)
-open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
-open import Data.These.Base as These using (These; this; that; these)
-open import Data.Unit.Base using (tt)
-open import Data.Vec.Base as Vec using (Vec; []; _∷_)
-open import Function.Base
-open import Function.Bundles using () renaming (module Equivalence to Eq)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl)
-open import Relation.Nullary.Decidable using (isYes)
+open import Data.List.Base as List using (List)
 
 ------------------------------------------------------------------------
 -- Re-export basic type and operations
diff --git a/src/Data/List/Relation/Binary/Disjoint/Propositional.agda b/src/Data/List/Relation/Binary/Disjoint/Propositional.agda
index ecae6c7610..6b78c64c85 100644
--- a/src/Data/List/Relation/Binary/Disjoint/Propositional.agda
+++ b/src/Data/List/Relation/Binary/Disjoint/Propositional.agda
@@ -11,7 +11,7 @@ open import Relation.Binary
 module Data.List.Relation.Binary.Disjoint.Propositional
   {a} {A : Set a} where
 
-open import Relation.Binary.PropositionalEquality using (setoid)
+open import Relation.Binary.PropositionalEquality.Properties using (setoid)
 open import Data.List.Relation.Binary.Disjoint.Setoid as DisjointUnique
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Relation/Binary/Equality/Propositional.agda b/src/Data/List/Relation/Binary/Equality/Propositional.agda
index f263778211..9ecb2cfd6b 100644
--- a/src/Data/List/Relation/Binary/Equality/Propositional.agda
+++ b/src/Data/List/Relation/Binary/Equality/Propositional.agda
@@ -16,7 +16,8 @@ module Data.List.Relation.Binary.Equality.Propositional {a} {A : Set a} where
 
 open import Data.List.Base
 import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as P
 
 ------------------------------------------------------------------------
 -- Re-export everything from setoid equality
diff --git a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
index 9366b5a027..f9610d5422 100644
--- a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
@@ -21,7 +21,7 @@ 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.PropositionalEquality using (_≢_; refl; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≢_; refl; cong)
 
 open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise)
 open import Data.List.Relation.Binary.Infix.Heterogeneous
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional.agda b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
index 939491ecc4..5d9068755b 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional.agda
@@ -11,7 +11,7 @@ module Data.List.Relation.Binary.Permutation.Propositional
 
 open import Data.List.Base using (List; []; _∷_)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
index f5a87cb067..135d5a778d 100644
--- a/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
@@ -28,7 +28,7 @@ open import Function.Inverse as Inv using (inverse)
 open import Level using (Level)
 open import Relation.Unary using (Pred)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as ≡
+open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_ ; refl ; cong; cong₂; _≢_)
 open import Relation.Nullary
 
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
index e98cc6315c..5a147d8008 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
@@ -17,7 +17,7 @@ import Data.List.Relation.Binary.Pointwise as Pointwise
 open import Data.List.Relation.Binary.Equality.Setoid S
 open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Level using (_⊔_)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 
 private
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index 3483323844..24b8bee2cf 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -36,7 +36,7 @@ open import Function.Inverse as Inv using (inverse)
 open import Level using (Level; _⊔_)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Binary.Properties.Setoid S using (≉-resp₂)
-open import Relation.Binary.PropositionalEquality as ≡
+open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_ ; refl; sym; cong; cong₂; subst; _≢_)
 open import Relation.Nullary.Decidable using (yes; no; does)
 open import Relation.Nullary.Negation using (contradiction)
diff --git a/src/Data/List/Relation/Binary/Pointwise.agda b/src/Data/List/Relation/Binary/Pointwise.agda
index cadfaf0846..0852085a37 100644
--- a/src/Data/List/Relation/Binary/Pointwise.agda
+++ b/src/Data/List/Relation/Binary/Pointwise.agda
@@ -26,7 +26,8 @@ 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.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as P
 
 private
   variable
diff --git a/src/Data/List/Relation/Binary/Pointwise/Properties.agda b/src/Data/List/Relation/Binary/Pointwise/Properties.agda
index 61470fdc76..207f0fe70d 100644
--- a/src/Data/List/Relation/Binary/Pointwise/Properties.agda
+++ b/src/Data/List/Relation/Binary/Pointwise/Properties.agda
@@ -13,7 +13,7 @@ open import Data.List.Base using (List; []; _∷_)
 open import Level
 open import Relation.Binary.Core using (REL; _⇒_)
 open import Relation.Binary.Definitions
-import Relation.Binary.PropositionalEquality as P
+import Relation.Binary.PropositionalEquality.Core as P
 open import Relation.Nullary using (yes; no; _×-dec_)
 import Relation.Nullary.Decidable as Dec
 
diff --git a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
index eea13df3b6..da5a26e6e0 100644
--- a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
@@ -26,7 +26,7 @@ open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no; _because_)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; _≢_)
 
 private
   variable
diff --git a/src/Data/List/Relation/Binary/Sublist/DecPropositional/Solver.agda b/src/Data/List/Relation/Binary/Sublist/DecPropositional/Solver.agda
index 6ca8768c43..6385ff0960 100644
--- a/src/Data/List/Relation/Binary/Sublist/DecPropositional/Solver.agda
+++ b/src/Data/List/Relation/Binary/Sublist/DecPropositional/Solver.agda
@@ -8,12 +8,12 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary using (Decidable)
-open import Agda.Builtin.Equality using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 module Data.List.Relation.Binary.Sublist.DecPropositional.Solver
        {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
        where
 
-import Relation.Binary.PropositionalEquality as P
+import Relation.Binary.PropositionalEquality.Properties as P
 
 open import Data.List.Relation.Binary.Sublist.DecSetoid.Solver (P.decSetoid _≟_) public
diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous.agda
index 854a6a1e8f..698dd789b0 100644
--- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous.agda
@@ -12,7 +12,7 @@ open import Data.List.Base using (List; []; _∷_; [_])
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Level using (_⊔_)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Unary using (Pred)
 
 module Data.List.Relation.Binary.Sublist.Heterogeneous
diff --git a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
index 7d13343130..f11e85258c 100644
--- a/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
@@ -34,7 +34,7 @@ open import Relation.Nullary using (Dec; does; _because_; yes; no; ¬_)
 open import Relation.Nullary.Decidable as Dec using (¬?)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary hiding (_⇔_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 ------------------------------------------------------------------------
 -- Injectivity of constructors
diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Disjoint.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Disjoint.agda
index edcf2b565b..a6a33cc43a 100644
--- a/src/Data/List/Relation/Binary/Sublist/Propositional/Disjoint.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Disjoint.agda
@@ -11,7 +11,7 @@ module Data.List.Relation.Binary.Sublist.Propositional.Disjoint
 
 open import Data.List.Base using (List)
 open import Data.List.Relation.Binary.Sublist.Propositional
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
 ------------------------------------------------------------------------
 -- A Union where the triangles commute is a
diff --git a/src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda b/src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda
index b8b8745b68..9a681ff916 100644
--- a/src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda
@@ -10,7 +10,7 @@
 
 module Data.List.Relation.Binary.Sublist.Propositional.Example.UniqueBoundVariables (Base : Set) where
 
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; subst; module ≡-Reasoning)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; cong; subst; module ≡-Reasoning)
 open ≡-Reasoning
 
 open import Data.List.Base using (List; []; _∷_; [_])
diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid.agda b/src/Data/List/Relation/Binary/Sublist/Setoid.agda
index 7a7b62c673..8915308cf2 100644
--- a/src/Data/List/Relation/Binary/Sublist/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Setoid.agda
@@ -26,7 +26,7 @@ import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
 open import Data.Product using (∃; ∃₂; _×_; _,_; proj₂)
 
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 
 open Setoid S renaming (Carrier to A)
diff --git a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
index 5600339c7b..b9c3d21968 100644
--- a/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
@@ -21,7 +21,7 @@ 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.PropositionalEquality using (_≡_; refl; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 open import Relation.Binary.Structures using (IsDecTotalOrder)
 open import Relation.Unary using (Pred; Decidable; Irrelevant)
 open import Relation.Nullary.Negation using (¬_)
diff --git a/src/Data/List/Relation/Binary/Subset/Propositional.agda b/src/Data/List/Relation/Binary/Subset/Propositional.agda
index d97fc73114..c6ecf5e5fa 100644
--- a/src/Data/List/Relation/Binary/Subset/Propositional.agda
+++ b/src/Data/List/Relation/Binary/Subset/Propositional.agda
@@ -10,7 +10,7 @@ module Data.List.Relation.Binary.Subset.Propositional
   {a} {A : Set a} where
 
 import Data.List.Relation.Binary.Subset.Setoid as SetoidSubset
-open import Relation.Binary.PropositionalEquality using (setoid)
+open import Relation.Binary.PropositionalEquality.Properties using (setoid)
 
 ------------------------------------------------------------------------
 -- Re-export parameterised definitions from setoid sublists
diff --git a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda
index 736389bb75..05b7725d31 100644
--- a/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda
@@ -26,7 +26,7 @@ open import Relation.Unary as U using (Pred)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary as B
   using (REL; Rel; Trans; Antisym; Irrelevant; _⇒_)
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; _≢_; refl; sym; subst; subst₂)
 
 import Data.List.Properties as Listₚ
diff --git a/src/Data/List/Relation/Ternary/Appending.agda b/src/Data/List/Relation/Ternary/Appending.agda
index 75e50d15af..0d1f935414 100644
--- a/src/Data/List/Relation/Ternary/Appending.agda
+++ b/src/Data/List/Relation/Ternary/Appending.agda
@@ -13,7 +13,7 @@ open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
 open import Data.Product as Prod using (∃₂; _×_; _,_; -,_)
 open import Relation.Binary using (REL)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
 private
   variable
diff --git a/src/Data/List/Relation/Ternary/Appending/Properties.agda b/src/Data/List/Relation/Ternary/Appending/Properties.agda
index 11db3cf16e..4508a7f719 100644
--- a/src/Data/List/Relation/Ternary/Appending/Properties.agda
+++ b/src/Data/List/Relation/Ternary/Appending/Properties.agda
@@ -13,7 +13,7 @@ open import Data.List.Relation.Ternary.Appending
 open import Data.List.Relation.Binary.Pointwise as Pw using (Pointwise; []; _∷_)
 open import Level using (Level)
 open import Relation.Binary using (REL; Rel; Trans)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 private
   variable
diff --git a/src/Data/List/Relation/Ternary/Appending/Propositional/Properties.agda b/src/Data/List/Relation/Ternary/Appending/Propositional/Properties.agda
index e4ecefddae..757d888012 100644
--- a/src/Data/List/Relation/Ternary/Appending/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Ternary/Appending/Propositional/Properties.agda
@@ -14,7 +14,8 @@ import Data.List.Relation.Binary.Pointwise as Pw
 open import Data.List.Relation.Binary.Equality.Propositional using (_≋_)
 open import Data.List.Relation.Ternary.Appending.Propositional {A = A}
 open import Function.Base using (_∘′_)
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; setoid)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Binary.PropositionalEquality.Properties using (setoid)
 
 import Data.List.Relation.Ternary.Appending.Setoid.Properties (setoid A)
   as Appendingₚ
diff --git a/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda b/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda
index 60e3e2f4ad..0530b8b965 100644
--- a/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda
@@ -15,7 +15,7 @@ import Data.List.Properties as Listₚ
 open import Data.List.Relation.Binary.Pointwise using (Pointwise; [])
 import Data.List.Relation.Ternary.Appending.Properties as Appendingₚ
 open import Data.Product using (_,_)
-open import Relation.Binary.PropositionalEquality using (refl)
+open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 open import Data.List.Relation.Ternary.Appending.Setoid S
 module S = Setoid S; open S renaming (Carrier to A) using (_≈_)
diff --git a/src/Data/List/Relation/Ternary/Interleaving.agda b/src/Data/List/Relation/Ternary/Interleaving.agda
index cfc84e52c4..62206daf2c 100644
--- a/src/Data/List/Relation/Ternary/Interleaving.agda
+++ b/src/Data/List/Relation/Ternary/Interleaving.agda
@@ -16,7 +16,7 @@ open import Data.Product as Prod using (∃; ∃₂; _×_; uncurry; _,_; -,_; pr
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 ------------------------------------------------------------------------
 -- Definition
diff --git a/src/Data/List/Relation/Ternary/Interleaving/Propositional.agda b/src/Data/List/Relation/Ternary/Interleaving/Propositional.agda
index c1ac5c9adf..55515cd447 100644
--- a/src/Data/List/Relation/Ternary/Interleaving/Propositional.agda
+++ b/src/Data/List/Relation/Ternary/Interleaving/Propositional.agda
@@ -12,7 +12,8 @@ open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.List.Relation.Binary.Permutation.Propositional as Perm using (_↭_)
 open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (shift)
 import Data.List.Relation.Ternary.Interleaving.Setoid as General
-open import Relation.Binary.PropositionalEquality using (setoid; refl)
+open import Relation.Binary.PropositionalEquality.Core using (refl)
+open import Relation.Binary.PropositionalEquality.Properties using (setoid)
 open Perm.PermutationReasoning
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Relation/Ternary/Interleaving/Propositional/Properties.agda b/src/Data/List/Relation/Ternary/Interleaving/Propositional/Properties.agda
index b8328e48e8..c4253a7253 100644
--- a/src/Data/List/Relation/Ternary/Interleaving/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Ternary/Interleaving/Propositional/Properties.agda
@@ -11,7 +11,7 @@ module Data.List.Relation.Ternary.Interleaving.Propositional.Properties
 
 import Data.List.Relation.Ternary.Interleaving.Setoid.Properties
   as SetoidProperties
-open import Relation.Binary.PropositionalEquality using (setoid)
+open import Relation.Binary.PropositionalEquality.Properties using (setoid)
 
 ------------------------------------------------------------------------
 -- Re-exporting existing properties
diff --git a/src/Data/List/Relation/Unary/All.agda b/src/Data/List/Relation/Unary/All.agda
index 090af7e6b6..52d2baa819 100644
--- a/src/Data/List/Relation/Unary/All.agda
+++ b/src/Data/List/Relation/Unary/All.agda
@@ -24,7 +24,8 @@ open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec
 open import Relation.Unary hiding (_∈_)
 open import Relation.Binary using (Setoid; _Respects_)
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
+import Relation.Binary.PropositionalEquality.Properties as P
 
 private
   variable
diff --git a/src/Data/List/Relation/Unary/AllPairs/Properties.agda b/src/Data/List/Relation/Unary/AllPairs/Properties.agda
index 009ac3ce75..037279cfe1 100644
--- a/src/Data/List/Relation/Unary/AllPairs/Properties.agda
+++ b/src/Data/List/Relation/Unary/AllPairs/Properties.agda
@@ -20,7 +20,7 @@ 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.PropositionalEquality using (_≢_)
+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/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index 6ac93bc05e..6a0020d269 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -41,7 +41,7 @@ open import Function.Inverse as Inv using (_↔_; inverse; Inverse)
 open import Function.Related as Related using (Kind; Related; SK-sym)
 open import Level using (Level)
 open import Relation.Binary as B hiding (_⇔_)
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl)
 open import Relation.Unary as U
   using (Pred; _⟨×⟩_; _⟨→⟩_) renaming (_⊆_ to _⋐_)
diff --git a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda
index b9eabc66b3..dc0114238a 100644
--- a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda
@@ -20,7 +20,7 @@ open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Function
 open import Level
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 open import Relation.Binary.Properties.Setoid using (respʳ-flip)
 
 module Data.List.Relation.Unary.Enumerates.Setoid.Properties where
diff --git a/src/Data/List/Relation/Unary/Linked/Properties.agda b/src/Data/List/Relation/Unary/Linked/Properties.agda
index 7106ad3e1e..d969986a55 100644
--- a/src/Data/List/Relation/Unary/Linked/Properties.agda
+++ b/src/Data/List/Relation/Unary/Linked/Properties.agda
@@ -23,7 +23,7 @@ open import Data.Maybe.Relation.Binary.Connected
 open import Level using (Level)
 open import Function.Base using (_∘_; flip; _on_)
 open import Relation.Binary using (Rel; Transitive; DecSetoid)
-open import Relation.Binary.PropositionalEquality using (_≢_)
+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/List/Relation/Unary/Sufficient.agda b/src/Data/List/Relation/Unary/Sufficient.agda
index be7bf76261..35d63add25 100644
--- a/src/Data/List/Relation/Unary/Sufficient.agda
+++ b/src/Data/List/Relation/Unary/Sufficient.agda
@@ -18,7 +18,7 @@ module Data.List.Relation.Unary.Sufficient where
 
 open import Level using (Level; _⊔_)
 open import Data.List.Base using (List; []; _∷_; [_]; _++_)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 private
   variable
diff --git a/src/Data/List/Relation/Unary/Unique/DecPropositional.agda b/src/Data/List/Relation/Unary/Unique/DecPropositional.agda
index 19ba99025f..3f552b6fa9 100644
--- a/src/Data/List/Relation/Unary/Unique/DecPropositional.agda
+++ b/src/Data/List/Relation/Unary/Unique/DecPropositional.agda
@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary using (DecSetoid; DecidableEquality)
-open import Relation.Binary.PropositionalEquality using (decSetoid)
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
 module Data.List.Relation.Unary.Unique.DecPropositional
   {a} {A : Set a} (_≟_ : DecidableEquality A) where
diff --git a/src/Data/List/Relation/Unary/Unique/DecPropositional/Properties.agda b/src/Data/List/Relation/Unary/Unique/DecPropositional/Properties.agda
index 7512f05246..6d28ed56d6 100644
--- a/src/Data/List/Relation/Unary/Unique/DecPropositional/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/DecPropositional/Properties.agda
@@ -11,7 +11,7 @@ import Data.List.Relation.Unary.Unique.DecSetoid.Properties as Setoid
 open import Data.List.Relation.Unary.All.Properties using (all-filter)
 open import Level
 open import Relation.Binary using (DecidableEquality)
-open import Relation.Binary.PropositionalEquality using (decSetoid)
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
 module Data.List.Relation.Unary.Unique.DecPropositional.Properties
   {a} {A : Set a} (_≟_ : DecidableEquality A) where
diff --git a/src/Data/List/Relation/Unary/Unique/Propositional.agda b/src/Data/List/Relation/Unary/Unique/Propositional.agda
index 4e3b600d2e..2c32f0da46 100644
--- a/src/Data/List/Relation/Unary/Unique/Propositional.agda
+++ b/src/Data/List/Relation/Unary/Unique/Propositional.agda
@@ -8,7 +8,7 @@
 
 module Data.List.Relation.Unary.Unique.Propositional {a} {A : Set a} where
 
-open import Relation.Binary.PropositionalEquality using (setoid)
+open import Relation.Binary.PropositionalEquality.Properties using (setoid)
 open import Data.List.Relation.Unary.Unique.Setoid as SetoidUnique
 
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
index a7413994ba..33b66d2bd1 100644
--- a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
@@ -24,7 +24,7 @@ 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.PropositionalEquality using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Negation using (contraposition)
diff --git a/src/Data/Maybe/Relation/Binary/Connected.agda b/src/Data/Maybe/Relation/Binary/Connected.agda
index e2fea581af..33bff58154 100644
--- a/src/Data/Maybe/Relation/Binary/Connected.agda
+++ b/src/Data/Maybe/Relation/Binary/Connected.agda
@@ -13,7 +13,7 @@ open import Data.Product
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Relation.Binary hiding (_⇔_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec
 
diff --git a/src/Data/Maybe/Relation/Binary/Pointwise.agda b/src/Data/Maybe/Relation/Binary/Pointwise.agda
index 389c1fde6e..3ae5ad421e 100644
--- a/src/Data/Maybe/Relation/Binary/Pointwise.agda
+++ b/src/Data/Maybe/Relation/Binary/Pointwise.agda
@@ -13,7 +13,7 @@ open import Data.Product
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Relation.Binary hiding (_⇔_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec
 
diff --git a/src/Data/Maybe/Relation/Unary/All.agda b/src/Data/Maybe/Relation/Unary/All.agda
index 0c2c3faecd..a3818c38b2 100644
--- a/src/Data/Maybe/Relation/Unary/All.agda
+++ b/src/Data/Maybe/Relation/Unary/All.agda
@@ -16,7 +16,7 @@ open import Data.Product as Prod using (_,_)
 open import Function.Base using (id; _∘′_)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level
-open import Relation.Binary.PropositionalEquality as P using (_≡_; cong)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; cong)
 open import Relation.Unary
 open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec
diff --git a/src/Data/Maybe/Relation/Unary/Any.agda b/src/Data/Maybe/Relation/Unary/Any.agda
index 61a06e840a..ea81316c77 100644
--- a/src/Data/Maybe/Relation/Unary/Any.agda
+++ b/src/Data/Maybe/Relation/Unary/Any.agda
@@ -13,7 +13,7 @@ open import Data.Product as Prod using (∃; _,_; -,_)
 open import Function.Base using (id)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level
-open import Relation.Binary.PropositionalEquality as P using (_≡_; cong)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; cong)
 open import Relation.Unary
 open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec
diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda
index 6f126a80d6..13701b486c 100644
--- a/src/Data/Nat/Coprimality.agda
+++ b/src/Data/Nat/Coprimality.agda
@@ -21,7 +21,7 @@ open import Data.Nat.DivMod
 open import Data.Product as Prod
 open import Function
 open import Level using (0ℓ)
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; _≢_; refl; trans; cong; subst; module ≡-Reasoning)
 open import Relation.Nullary as Nullary hiding (recompute)
 open import Relation.Nullary.Negation using (contradiction)
diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda
index c202d740ba..26cd81bf27 100644
--- a/src/Data/Nat/Divisibility.agda
+++ b/src/Data/Nat/Divisibility.agda
@@ -20,8 +20,9 @@ open import Relation.Nullary.Decidable as Dec using (False; yes; no)
 open import Relation.Nullary.Negation.Core using (contradiction)
 open import Relation.Binary
 import Relation.Binary.Reasoning.Preorder as PreorderReasoning
-open import Relation.Binary.PropositionalEquality as PropEq
+open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl; sym; trans; cong; cong₂; subst)
+import Relation.Binary.PropositionalEquality.Properties as PropEq
 
 ------------------------------------------------------------------------
 -- Definition
diff --git a/src/Data/Nat/GCD.agda b/src/Data/Nat/GCD.agda
index fe90cc0282..9e21f6f812 100644
--- a/src/Data/Nat/GCD.agda
+++ b/src/Data/Nat/GCD.agda
@@ -21,7 +21,7 @@ open import Function
 open import Induction using (build)
 open import Induction.Lexicographic using (_⊗_; [_⊗_])
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; _≢_; subst; cong)
 open import Relation.Nullary.Decidable using (Dec)
 open import Relation.Nullary.Negation using (contradiction)
diff --git a/src/Data/Nat/LCM.agda b/src/Data/Nat/LCM.agda
index 9b8932785a..5ce1c7cd2a 100644
--- a/src/Data/Nat/LCM.agda
+++ b/src/Data/Nat/LCM.agda
@@ -18,7 +18,7 @@ open import Data.Nat.GCD
 open import Data.Product
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)
 open import Relation.Binary
 open import Relation.Nullary.Decidable using (False; fromWitnessFalse)
diff --git a/src/Data/Nat/Logarithm.agda b/src/Data/Nat/Logarithm.agda
index 4e08abcf4d..461fa540e6 100644
--- a/src/Data/Nat/Logarithm.agda
+++ b/src/Data/Nat/Logarithm.agda
@@ -11,7 +11,7 @@ module Data.Nat.Logarithm where
 open import Data.Nat
 open import Data.Nat.Induction using (<-wellFounded)
 open import Data.Nat.Logarithm.Core
-open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 ------------------------------------------------------------------------
 -- Logarithm base 2
diff --git a/src/Data/Nat/Show/Properties.agda b/src/Data/Nat/Show/Properties.agda
index 87622b79bf..564264946c 100644
--- a/src/Data/Nat/Show/Properties.agda
+++ b/src/Data/Nat/Show/Properties.agda
@@ -13,7 +13,7 @@ import Data.List.Properties as Listₚ
 open import Data.Nat.Base using (ℕ)
 open import Data.Nat.Properties using (_≤?_)
 open import Relation.Nullary.Decidable using (True)
-open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 open import Data.Nat.Show using (charsInBase)
 
 module Data.Nat.Show.Properties where
diff --git a/src/Data/Product/Effectful/Examples.agda b/src/Data/Product/Effectful/Examples.agda
index 90488642f6..daf05ce431 100644
--- a/src/Data/Product/Effectful/Examples.agda
+++ b/src/Data/Product/Effectful/Examples.agda
@@ -19,7 +19,7 @@ open import Data.Product.Relation.Binary.Pointwise.NonDependent
 open import Function
 import Function.Identity.Effectful as Id
 open import Relation.Binary using (Rel)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 ------------------------------------------------------------------------
 -- Examples
diff --git a/src/Data/Product/Function/Dependent/Setoid.agda b/src/Data/Product/Function/Dependent/Setoid.agda
index f6629e048a..cc6d4a12fc 100644
--- a/src/Data/Product/Function/Dependent/Setoid.agda
+++ b/src/Data/Product/Function/Dependent/Setoid.agda
@@ -28,7 +28,8 @@ open import Relation.Binary.Indexed.Heterogeneous
   using (IndexedSetoid)
 open import Relation.Binary.Indexed.Heterogeneous.Construct.At
   using (_atₛ_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as P
 
 ------------------------------------------------------------------------
 -- Properties related to "relatedness"
diff --git a/src/Data/Product/Function/Dependent/Setoid/WithK.agda b/src/Data/Product/Function/Dependent/Setoid/WithK.agda
index a343e22b43..c9468fb939 100644
--- a/src/Data/Product/Function/Dependent/Setoid/WithK.agda
+++ b/src/Data/Product/Function/Dependent/Setoid/WithK.agda
@@ -30,7 +30,8 @@ open import Relation.Binary.Indexed.Heterogeneous
   using (IndexedSetoid)
 open import Relation.Binary.Indexed.Heterogeneous.Construct.At
   using (_atₛ_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as P
 
 ------------------------------------------------------------------------
 -- Combinator for Inverse
diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda
index 5c7c117a4b..d0a09fa4ac 100644
--- a/src/Data/Product/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda
@@ -22,7 +22,7 @@ open import Level
 open import Relation.Nullary.Decidable
 open import Relation.Binary
 open import Relation.Binary.Consequences
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl)
 
 private
   variable
diff --git a/src/Data/Product/Relation/Binary/Pointwise/Dependent.agda b/src/Data/Product/Relation/Binary/Pointwise/Dependent.agda
index 5f6953071a..96f7211ce7 100644
--- a/src/Data/Product/Relation/Binary/Pointwise/Dependent.agda
+++ b/src/Data/Product/Relation/Binary/Pointwise/Dependent.agda
@@ -15,7 +15,7 @@ open import Relation.Binary as B
   using (_⇒_; Setoid; IsEquivalence)
 open import Relation.Binary.Indexed.Heterogeneous as I
   using (IREL; IRel; IndexedSetoid; IsIndexedEquivalence)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 ------------------------------------------------------------------------
 -- Pointwise lifting
diff --git a/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda b/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda
index c1228b5a91..13edd9aa66 100644
--- a/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda
+++ b/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda
@@ -16,7 +16,8 @@ open import Function.Inverse using (Inverse)
 open import Relation.Binary using (_⇒_)
 open import Relation.Binary.HeterogeneousEquality as H using (_≅_)
 open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as P
 
 ------------------------------------------------------------------------
 -- The propositional equality setoid over sigma types can be
diff --git a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
index 1bbf5981e1..fc77109043 100644
--- a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
+++ b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
@@ -27,7 +27,8 @@ open import Function.Surjection as Surj
   using (Surjection; _↠_; module Surjection)
 open import Relation.Nullary.Decidable using (_×-dec_)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as P
 
 module _ {a₁ a₂ ℓ₁ ℓ₂} {A₁ : Set a₁} {A₂ : Set a₂} where
 
diff --git a/src/Data/String.agda b/src/Data/String.agda
index 98814b1909..fffe1ac300 100644
--- a/src/Data/String.agda
+++ b/src/Data/String.agda
@@ -23,7 +23,7 @@ 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.PropositionalEquality using (_≡_; refl)
+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/Data/String/Properties.agda b/src/Data/String/Properties.agda
index e0f47fa175..b7ed9a93d6 100644
--- a/src/Data/String/Properties.agda
+++ b/src/Data/String/Properties.agda
@@ -20,7 +20,7 @@ open import Relation.Nullary.Decidable using (map′; isYes)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality.Core
 import Relation.Binary.Construct.On as On
-import Relation.Binary.PropositionalEquality as PropEq
+import Relation.Binary.PropositionalEquality.Properties as PropEq
 
 ------------------------------------------------------------------------
 -- Primitive properties
diff --git a/src/Data/String/Unsafe.agda b/src/Data/String/Unsafe.agda
index 9c001365a3..ff1ff28408 100644
--- a/src/Data/String/Unsafe.agda
+++ b/src/Data/String/Unsafe.agda
@@ -16,7 +16,7 @@ open import Data.Product.Base using (proj₂)
 open import Data.String.Base
 open import Function.Base using (_∘′_)
 
-open import Relation.Binary.PropositionalEquality; open ≡-Reasoning
+open import Relation.Binary.PropositionalEquality.Core; open ≡-Reasoning
 open import Relation.Binary.PropositionalEquality.TrustMe using (trustMe)
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Sum/Relation/Binary/LeftOrder.agda b/src/Data/Sum/Relation/Binary/LeftOrder.agda
index 063ba49bb7..34c676bcbb 100644
--- a/src/Data/Sum/Relation/Binary/LeftOrder.agda
+++ b/src/Data/Sum/Relation/Binary/LeftOrder.agda
@@ -18,7 +18,7 @@ open import Level
 open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 ----------------------------------------------------------------------
 -- Definition
diff --git a/src/Data/Sum/Relation/Binary/Pointwise.agda b/src/Data/Sum/Relation/Binary/Pointwise.agda
index d5ec85b943..23d10172c9 100644
--- a/src/Data/Sum/Relation/Binary/Pointwise.agda
+++ b/src/Data/Sum/Relation/Binary/Pointwise.agda
@@ -17,7 +17,8 @@ open import Function.Inverse using (Inverse)
 open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as P
 
 ----------------------------------------------------------------------
 -- Definition
diff --git a/src/Data/Tree/AVL/Indexed.agda b/src/Data/Tree/AVL/Indexed.agda
index 8cd4fc49bd..16ebdff70e 100644
--- a/src/Data/Tree/AVL/Indexed.agda
+++ b/src/Data/Tree/AVL/Indexed.agda
@@ -20,7 +20,7 @@ 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.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 private
   variable
diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda
index e37c7f9b34..5add64a3cc 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda
@@ -20,7 +20,7 @@ open import Function.Base
 open import Function.Nary.NonDependent using (congₙ)
 open import Level using (Level; _⊔_)
 
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Nullary.Decidable using (Dec; yes; map′; _×-dec_)
 open import Relation.Unary using (Pred; Decidable; Universal; Irrelevant; _⊆_; _∪_)
 
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 8b5b195d42..f2dec21b8c 100644
--- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
@@ -22,7 +22,7 @@ open import Function.Base as F
 open import Level using (Level)
 
 open import Relation.Binary using (_Respects_; tri<; tri≈; tri>)
-open import Relation.Binary.PropositionalEquality using (_≡_) renaming (refl to ≡-refl)
+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)
 open import Relation.Unary using (Pred; _∩_)
diff --git a/src/Data/Tree/AVL/Indexed/WithK.agda b/src/Data/Tree/AVL/Indexed/WithK.agda
index 2ef4ec3544..7467a3813f 100644
--- a/src/Data/Tree/AVL/Indexed/WithK.agda
+++ b/src/Data/Tree/AVL/Indexed/WithK.agda
@@ -7,7 +7,7 @@
 {-# OPTIONS --with-K --safe #-}
 
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; subst)
 
 module Data.Tree.AVL.Indexed.WithK
        {k r} (Key : Set k) {_<_ : Rel Key r}
diff --git a/src/Data/Tree/AVL/IndexedMap.agda b/src/Data/Tree/AVL/IndexedMap.agda
index 21413e0478..cb16cd6220 100644
--- a/src/Data/Tree/AVL/IndexedMap.agda
+++ b/src/Data/Tree/AVL/IndexedMap.agda
@@ -8,7 +8,7 @@
 
 open import Data.Product as Prod
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality using (_≡_; cong; subst)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst)
 import Data.Tree.AVL.Value
 
 module Data.Tree.AVL.IndexedMap
diff --git a/src/Data/Tree/AVL/Key.agda b/src/Data/Tree/AVL/Key.agda
index dc7e77824d..9a2b7e8521 100644
--- a/src/Data/Tree/AVL/Key.agda
+++ b/src/Data/Tree/AVL/Key.agda
@@ -17,7 +17,7 @@ open import Level
 open import Data.Empty
 open import Data.Unit
 open import Data.Product
-open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_ ; refl)
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Construct.Add.Extrema
   as AddExtremaToSet using (_±)
diff --git a/src/Data/Tree/AVL/NonEmpty/Propositional.agda b/src/Data/Tree/AVL/NonEmpty/Propositional.agda
index f537b1c673..82ea9125fd 100644
--- a/src/Data/Tree/AVL/NonEmpty/Propositional.agda
+++ b/src/Data/Tree/AVL/NonEmpty/Propositional.agda
@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary using (Rel; IsStrictTotalOrder; StrictTotalOrder)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; subst)
 
 module Data.Tree.AVL.NonEmpty.Propositional
   {k r} {Key : Set k} {_<_ : Rel Key r}
diff --git a/src/Data/Tree/AVL/Sets/Membership.agda b/src/Data/Tree/AVL/Sets/Membership.agda
index 947036500c..53e0aea9f9 100644
--- a/src/Data/Tree/AVL/Sets/Membership.agda
+++ b/src/Data/Tree/AVL/Sets/Membership.agda
@@ -18,7 +18,6 @@ open import Data.Sum.Base as Sum using (_⊎_)
 open import Data.Unit.Base using (tt)
 open import Function.Base using (_∘_; _∘′_; const)
 
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 open import Relation.Nullary using (¬_; yes; no; Reflects)
 open import Relation.Nullary.Reflects using (fromEquivalence)
 
diff --git a/src/Data/Tree/AVL/Sets/Membership/Properties.agda b/src/Data/Tree/AVL/Sets/Membership/Properties.agda
index 7c1f27a1d1..75fc1e9242 100644
--- a/src/Data/Tree/AVL/Sets/Membership/Properties.agda
+++ b/src/Data/Tree/AVL/Sets/Membership/Properties.agda
@@ -18,7 +18,7 @@ open import Data.Sum.Base as Sum using (_⊎_)
 open import Data.Unit.Base using (tt)
 open import Function.Base using (_∘_; _∘′_; const)
 
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Nullary using (¬_; yes; no; Reflects)
 open import Relation.Nullary.Reflects using (fromEquivalence)
 
diff --git a/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda b/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda
index 8b29e710f8..603582bf02 100644
--- a/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda
+++ b/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda
@@ -13,7 +13,7 @@ open import Data.Vec.Functional.Relation.Binary.Pointwise
 import Data.Vec.Functional.Relation.Binary.Pointwise.Properties as PW
 open import Level using (Level)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 module Data.Vec.Functional.Relation.Binary.Equality.Setoid
   {a ℓ} (S : Setoid a ℓ) where
diff --git a/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda b/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
index c0ae709b0f..0aa81b07a7 100644
--- a/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
+++ b/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
@@ -20,7 +20,7 @@ open import Data.Vec.Functional.Relation.Binary.Pointwise
 open import Function.Base
 open import Level using (Level)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 private
   variable
diff --git a/src/Data/Vec/Membership/DecPropositional.agda b/src/Data/Vec/Membership/DecPropositional.agda
index 0b20505b4b..e1b100f0af 100644
--- a/src/Data/Vec/Membership/DecPropositional.agda
+++ b/src/Data/Vec/Membership/DecPropositional.agda
@@ -7,7 +7,8 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary using (Decidable)
-open import Relation.Binary.PropositionalEquality using (_≡_; decSetoid)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
 module Data.Vec.Membership.DecPropositional
   {a} {A : Set a} (_≟_ : Decidable (_≡_ {A = A})) where
diff --git a/src/Data/Vec/Membership/Propositional.agda b/src/Data/Vec/Membership/Propositional.agda
index d76cedd1d3..21213e679d 100644
--- a/src/Data/Vec/Membership/Propositional.agda
+++ b/src/Data/Vec/Membership/Propositional.agda
@@ -11,7 +11,8 @@ module Data.Vec.Membership.Propositional {a} {A : Set a} where
 
 open import Data.Vec.Base using (Vec)
 open import Data.Vec.Relation.Unary.Any using (Any)
-open import Relation.Binary.PropositionalEquality using (setoid; subst)
+open import Relation.Binary.PropositionalEquality.Core using (subst)
+open import Relation.Binary.PropositionalEquality.Properties using (setoid)
 
 import Data.Vec.Membership.Setoid as SetoidMembership
 
diff --git a/src/Data/Vec/Membership/Propositional/Properties.agda b/src/Data/Vec/Membership/Propositional/Properties.agda
index 8efef380d4..983e70ae63 100644
--- a/src/Data/Vec/Membership/Propositional/Properties.agda
+++ b/src/Data/Vec/Membership/Propositional/Properties.agda
@@ -21,7 +21,7 @@ open import Data.List.Membership.Propositional
 open import Level using (Level)
 open import Function.Base using (_∘_; id)
 open import Relation.Unary using (Pred)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
 private
   variable
diff --git a/src/Data/Vec/Properties/WithK.agda b/src/Data/Vec/Properties/WithK.agda
index 8d3bd95aee..7ca8cc2c91 100644
--- a/src/Data/Vec/Properties/WithK.agda
+++ b/src/Data/Vec/Properties/WithK.agda
@@ -12,7 +12,7 @@ module Data.Vec.Properties.WithK where
 open import Data.Nat.Base
 open import Data.Nat.Properties using (+-assoc)
 open import Data.Vec.Base
-open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
 open import Relation.Binary.HeterogeneousEquality as H using (_≅_; refl)
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Vec/Recursive/Properties.agda b/src/Data/Vec/Recursive/Properties.agda
index 745681a617..d557808cee 100644
--- a/src/Data/Vec/Recursive/Properties.agda
+++ b/src/Data/Vec/Recursive/Properties.agda
@@ -14,7 +14,7 @@ open import Data.Product
 open import Data.Vec.Recursive
 open import Data.Vec.Base using (Vec; _∷_)
 open import Function.Inverse using (_↔_; inverse)
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
 open ≡-Reasoning
 
 private
diff --git a/src/Data/Vec/Relation/Binary/Equality/Setoid.agda b/src/Data/Vec/Relation/Binary/Equality/Setoid.agda
index 116b104829..d40bd24998 100644
--- a/src/Data/Vec/Relation/Binary/Equality/Setoid.agda
+++ b/src/Data/Vec/Relation/Binary/Equality/Setoid.agda
@@ -19,7 +19,6 @@ open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
 open import Function.Base
 open import Level using (_⊔_)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
 open Setoid S renaming (Carrier to A)
 
diff --git a/src/Data/Vec/Relation/Binary/Lex/Core.agda b/src/Data/Vec/Relation/Binary/Lex/Core.agda
index 4ac943401e..a3ff214a06 100644
--- a/src/Data/Vec/Relation/Binary/Lex/Core.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/Core.agda
@@ -19,7 +19,7 @@ open import Function.Base using (flip)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (Level; _⊔_)
 open import Relation.Binary hiding (_⇔_)
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl; cong)
 import Relation.Nullary as Nullary
 open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _×-dec_; _⊎-dec_)
diff --git a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
index 877d345045..d3c24ab42b 100644
--- a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
@@ -22,7 +22,6 @@ open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 open import Function.Base using (id)
 open import Relation.Binary
 import Relation.Binary.Construct.NonStrictToStrict as Conv
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Nullary hiding (Irrelevant)
 open import Level using (Level; _⊔_)
 
diff --git a/src/Data/Vec/Relation/Binary/Lex/Strict.agda b/src/Data/Vec/Relation/Binary/Lex/Strict.agda
index 7e4052476b..a1f11fb1b1 100644
--- a/src/Data/Vec/Relation/Binary/Lex/Strict.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/Strict.agda
@@ -27,7 +27,7 @@ open import Relation.Nullary using (yes; no; ¬_)
 open import Relation.Binary
 open import Relation.Binary.Consequences
 open import Relation.Binary.Construct.On as On using (wellFounded)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Level using (Level; _⊔_)
 
 private
diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda b/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
index ff6fd79833..c7b2b3d7ea 100644
--- a/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
+++ b/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
@@ -19,7 +19,7 @@ open import Function.Bundles using (module Equivalence; _⇔_; mk⇔)
 open import Function.Properties.Equivalence using (⇔-setoid)
 open import Level using (Level; _⊔_; 0ℓ)
 open import Relation.Binary hiding (_⇔_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Binary.Construct.Closure.Transitive as Plus
   hiding (equivalent; map)
 open import Relation.Nullary
diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
index e435e2681b..011c2b731b 100644
--- a/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
+++ b/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
@@ -17,7 +17,7 @@ open import Level using (Level; _⊔_)
 open import Function.Base using (_∘_)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Nullary.Decidable using (yes; no; _×-dec_; map′)
 open import Relation.Unary using (Pred)
 
diff --git a/src/Data/Vec/Relation/Unary/All.agda b/src/Data/Vec/Relation/Unary/All.agda
index 9ba434368c..2eda26c71e 100644
--- a/src/Data/Vec/Relation/Unary/All.agda
+++ b/src/Data/Vec/Relation/Unary/All.agda
@@ -20,7 +20,7 @@ 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.PropositionalEquality as P using (subst)
+open import Relation.Binary.PropositionalEquality.Core as P using (subst)
 
 private
   variable
diff --git a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda
index 339a884a3b..672c9fa485 100644
--- a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda
@@ -20,7 +20,7 @@ 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.PropositionalEquality using (_≢_)
+open import Relation.Binary.PropositionalEquality.Core using (_≢_)
 
 private
   variable
diff --git a/src/Data/Vec/Relation/Unary/Any/Properties.agda b/src/Data/Vec/Relation/Unary/Any/Properties.agda
index 5b3eab5fa1..1c9f171d7b 100644
--- a/src/Data/Vec/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Any/Properties.agda
@@ -29,7 +29,7 @@ open import Level using (Level)
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Unary hiding (_∈_)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_; refl)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
 
 private
   variable
diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
index a9604e1e6a..340b6b81a2 100644
--- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
@@ -20,7 +20,7 @@ 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.PropositionalEquality using (_≢_)
+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.agda b/src/Data/Vec/Relation/Unary/Unique/Propositional.agda
index 836f7f5b67..20b042ef17 100644
--- a/src/Data/Vec/Relation/Unary/Unique/Propositional.agda
+++ b/src/Data/Vec/Relation/Unary/Unique/Propositional.agda
@@ -8,7 +8,7 @@
 
 module Data.Vec.Relation.Unary.Unique.Propositional {a} {A : Set a} where
 
-open import Relation.Binary.PropositionalEquality using (setoid)
+open import Relation.Binary.PropositionalEquality.Properties using (setoid)
 open import Data.Vec.Relation.Unary.Unique.Setoid as SetoidUnique
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda b/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda
index 66371b89b5..4c433c04f6 100644
--- a/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda
@@ -19,7 +19,7 @@ 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.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Nullary.Negation using (contradiction; contraposition)
 
 private
diff --git a/src/Data/W/Sized.agda b/src/Data/W/Sized.agda
index c16b21828e..72d742ff4b 100644
--- a/src/Data/W/Sized.agda
+++ b/src/Data/W/Sized.agda
@@ -15,7 +15,7 @@ open import Data.Product using (_,_; -,_; proj₂)
 open import Data.Container.Core as Container using (Container; ⟦_⟧; Shape; Position; _⇒_; ⟪_⟫)
 open import Data.Container.Relation.Unary.All using (□; all)
 open import Relation.Nullary.Negation using (¬_)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 private
   variable
diff --git a/src/Effect/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda
index 03f82db8bb..0751cb5b15 100644
--- a/src/Effect/Monad/Partiality.agda
+++ b/src/Effect/Monad/Partiality.agda
@@ -21,7 +21,8 @@ open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (Level; _⊔_)
 open import Relation.Binary as B hiding (Rel; _⇔_)
 import Relation.Binary.Properties.Setoid as SetoidProperties
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as P
 open import Relation.Nullary
 open import Relation.Nullary.Decidable hiding (map)
 open import Relation.Nullary.Negation
diff --git a/src/Effect/Monad/Partiality/All.agda b/src/Effect/Monad/Partiality/All.agda
index 9bc5d4bc7e..7e90400a85 100644
--- a/src/Effect/Monad/Partiality/All.agda
+++ b/src/Effect/Monad/Partiality/All.agda
@@ -14,7 +14,7 @@ open import Codata.Musical.Notation
 open import Function
 open import Level
 open import Relation.Binary using (_Respects_; IsEquivalence)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 open Partiality._⊥
 open Partiality.Equality using (Rel)
diff --git a/src/Function/Construct/Identity.agda b/src/Function/Construct/Identity.agda
index 32660bee09..bec0ecd3d6 100644
--- a/src/Function/Construct/Identity.agda
+++ b/src/Function/Construct/Identity.agda
@@ -15,7 +15,8 @@ import Function.Definitions as Definitions
 import Function.Structures as Structures
 open import Level using (Level)
 open import Relation.Binary as B hiding (_⇔_; IsEquivalence)
-open import Relation.Binary.PropositionalEquality using (_≡_; setoid)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Binary.PropositionalEquality.Properties using (setoid)
 
 private
   variable
diff --git a/src/Function/Endomorphism/Propositional.agda b/src/Function/Endomorphism/Propositional.agda
index 8a78f69496..d14128edfe 100644
--- a/src/Function/Endomorphism/Propositional.agda
+++ b/src/Function/Endomorphism/Propositional.agda
@@ -21,7 +21,8 @@ open import Data.Product using (_,_)
 open import Function
 open import Function.Equality using (_⟨$⟩_)
 open import Relation.Binary using (_Preserves_⟶_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
+import Relation.Binary.PropositionalEquality.Properties as P
 
 import Function.Endomorphism.Setoid (P.setoid A) as Setoid
 
diff --git a/src/Function/Metric/Nat/Structures.agda b/src/Function/Metric/Nat/Structures.agda
index 648e7a4adc..839dc7b974 100644
--- a/src/Function/Metric/Nat/Structures.agda
+++ b/src/Function/Metric/Nat/Structures.agda
@@ -12,7 +12,7 @@ open import Data.Nat.Base hiding (suc)
 open import Function.Base using (const)
 open import Level using (Level; suc)
 open import Relation.Binary hiding (Symmetric)
-open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 open import Function.Metric.Nat.Core
 open import Function.Metric.Nat.Definitions
diff --git a/src/Function/Metric/Rational/Structures.agda b/src/Function/Metric/Rational/Structures.agda
index 824f90b912..daa2b71a60 100644
--- a/src/Function/Metric/Rational/Structures.agda
+++ b/src/Function/Metric/Rational/Structures.agda
@@ -10,7 +10,7 @@ open import Data.Rational.Base
 open import Function.Base using (const)
 open import Level using (Level; suc)
 open import Relation.Binary hiding (Symmetric)
-open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 open import Function.Metric.Rational.Core
 open import Function.Metric.Rational.Definitions
diff --git a/src/Function/Properties/Bijection.agda b/src/Function/Properties/Bijection.agda
index e484098774..c8abd7db19 100644
--- a/src/Function/Properties/Bijection.agda
+++ b/src/Function/Properties/Bijection.agda
@@ -11,7 +11,7 @@ module Function.Properties.Bijection where
 open import Function.Bundles
 open import Level using (Level)
 open import Relation.Binary hiding (_⇔_)
-open import Relation.Binary.PropositionalEquality as P using (setoid)
+import Relation.Binary.PropositionalEquality.Properties as P
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 open import Data.Product using (_,_; proj₁; proj₂)
 open import Function.Base using (_∘_)
diff --git a/src/Function/Properties/Equivalence.agda b/src/Function/Properties/Equivalence.agda
index ced34d9bd3..066316c01b 100644
--- a/src/Function/Properties/Equivalence.agda
+++ b/src/Function/Properties/Equivalence.agda
@@ -12,7 +12,7 @@ module Function.Properties.Equivalence where
 open import Function.Bundles using (Equivalence; _⇔_)
 open import Level
 open import Relation.Binary using (Setoid; IsEquivalence)
-import Relation.Binary.PropositionalEquality as Eq using (setoid)
+import Relation.Binary.PropositionalEquality.Properties as Eq
 
 import Function.Construct.Identity as Identity
 import Function.Construct.Symmetry as Symmetry
diff --git a/src/Function/Properties/Inverse.agda b/src/Function/Properties/Inverse.agda
index 508a8664be..6ef0b45af0 100644
--- a/src/Function/Properties/Inverse.agda
+++ b/src/Function/Properties/Inverse.agda
@@ -14,7 +14,8 @@ 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.PropositionalEquality as P using (setoid)
+import Relation.Binary.PropositionalEquality.Core as P
+import Relation.Binary.PropositionalEquality.Properties as P
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 open import Function.Consequences
 
diff --git a/src/Function/Related.agda b/src/Function/Related.agda
index fa114d077c..ca06dceffb 100644
--- a/src/Function/Related.agda
+++ b/src/Function/Related.agda
@@ -18,7 +18,8 @@ open import Function.Inverse     as Inv     using (Inverse; _↔_)
 open import Function.LeftInverse as LeftInv using (LeftInverse)
 open import Function.Surjection  as Surj    using (Surjection)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as P
 open import Data.Product using (_,_; proj₁; proj₂; <_,_>)
 
 import Function.Related.Propositional as R
diff --git a/src/Function/Related/Propositional.agda b/src/Function/Related/Propositional.agda
index 0ef8830265..5d62c0718b 100644
--- a/src/Function/Related/Propositional.agda
+++ b/src/Function/Related/Propositional.agda
@@ -13,7 +13,8 @@ open import Relation.Binary
   using (Sym; Reflexive; Trans; IsEquivalence; Setoid; IsPreorder; Preorder)
 open import Function.Bundles
 open import Function.Base
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as P
 
 open import Function.Properties.Surjection   using (↠⇒↪; ↠⇒⇔)
 open import Function.Properties.RightInverse using (↪⇒↠)
diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda
index cf151d9d3c..58cf6bab88 100644
--- a/src/Function/Related/TypeIsomorphisms.agda
+++ b/src/Function/Related/TypeIsomorphisms.agda
@@ -28,7 +28,7 @@ open import Function.Equivalence as Eq using (_⇔_; Equivalence)
 open import Function.Inverse as Inv using (_↔_; Inverse; inverse)
 open import Function.Related
 open import Relation.Binary hiding (_⇔_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary using (Dec; ¬_; _because_; ofⁿ)
 import Relation.Nullary.Indexed as I
diff --git a/src/Reflection/AST/Abstraction.agda b/src/Reflection/AST/Abstraction.agda
index 9ed64b8835..793c729aec 100644
--- a/src/Reflection/AST/Abstraction.agda
+++ b/src/Reflection/AST/Abstraction.agda
@@ -8,12 +8,12 @@
 
 module Reflection.AST.Abstraction where
 
-open import Data.Product                          using (_×_; <_,_>; uncurry)
-open import Data.String as String                 using (String)
+open import Data.Product                               using (_×_; <_,_>; uncurry)
+open import Data.String as String                      using (String)
 open import Level
-open import Relation.Nullary.Decidable            using (Dec; map′; _×-dec_)
-open import Relation.Binary                       using (DecidableEquality)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂)
+open import Relation.Nullary.Decidable                 using (Dec; map′; _×-dec_)
+open import Relation.Binary                            using (DecidableEquality)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
 
 private
   variable
diff --git a/src/Reflection/AST/Argument.agda b/src/Reflection/AST/Argument.agda
index 1b0884b615..0feb2deddd 100644
--- a/src/Reflection/AST/Argument.agda
+++ b/src/Reflection/AST/Argument.agda
@@ -8,11 +8,11 @@
 
 module Reflection.AST.Argument where
 
-open import Data.List.Base as List                using (List; []; _∷_)
-open import Data.Product                          using (_×_; <_,_>; uncurry)
-open import Relation.Nullary.Decidable            using (Dec; map′; _×-dec_)
-open import Relation.Binary                       using (DecidableEquality)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong₂)
+open import Data.List.Base as List                     using (List; []; _∷_)
+open import Data.Product                               using (_×_; <_,_>; uncurry)
+open import Relation.Nullary.Decidable                 using (Dec; map′; _×-dec_)
+open import Relation.Binary                            using (DecidableEquality)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong₂)
 open import Level
 
 open import Reflection.AST.Argument.Visibility
diff --git a/src/Reflection/AST/Argument/Information.agda b/src/Reflection/AST/Argument/Information.agda
index fe09976fb9..e0f5be24a5 100644
--- a/src/Reflection/AST/Argument/Information.agda
+++ b/src/Reflection/AST/Argument/Information.agda
@@ -8,10 +8,10 @@
 
 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.PropositionalEquality using (_≡_; refl; cong₂)
+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.PropositionalEquality.Core using (_≡_; refl; cong₂)
 
 open import Reflection.AST.Argument.Modality as Modality using (Modality)
 open import Reflection.AST.Argument.Visibility as Visibility using (Visibility)
diff --git a/src/Reflection/AST/Argument/Modality.agda b/src/Reflection/AST/Argument/Modality.agda
index 95f15b2264..02e481af58 100644
--- a/src/Reflection/AST/Argument/Modality.agda
+++ b/src/Reflection/AST/Argument/Modality.agda
@@ -8,10 +8,10 @@
 
 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.PropositionalEquality using (_≡_; refl; cong₂)
+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.PropositionalEquality.Core using (_≡_; refl; cong₂)
 
 open import Reflection.AST.Argument.Relevance as Relevance using (Relevance)
 open import Reflection.AST.Argument.Quantity as Quantity using (Quantity)
diff --git a/src/Reflection/AST/Argument/Quantity.agda b/src/Reflection/AST/Argument/Quantity.agda
index 0c53a521c1..5b3b98e092 100644
--- a/src/Reflection/AST/Argument/Quantity.agda
+++ b/src/Reflection/AST/Argument/Quantity.agda
@@ -8,9 +8,9 @@
 
 module Reflection.AST.Argument.Quantity where
 
-open import Relation.Nullary                      using (yes; no)
-open import Relation.Binary                       using (DecidableEquality)
-open import Relation.Binary.PropositionalEquality using (refl)
+open import Relation.Nullary                           using (yes; no)
+open import Relation.Binary                            using (DecidableEquality)
+open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 ------------------------------------------------------------------------
 -- Re-exporting the builtins publicly
diff --git a/src/Reflection/AST/Argument/Relevance.agda b/src/Reflection/AST/Argument/Relevance.agda
index 6cdce1d96f..03ba0f4f0a 100644
--- a/src/Reflection/AST/Argument/Relevance.agda
+++ b/src/Reflection/AST/Argument/Relevance.agda
@@ -8,9 +8,9 @@
 
 module Reflection.AST.Argument.Relevance where
 
-open import Relation.Nullary                      using (yes; no)
-open import Relation.Binary                       using (DecidableEquality)
-open import Relation.Binary.PropositionalEquality using (refl)
+open import Relation.Nullary                           using (yes; no)
+open import Relation.Binary                            using (DecidableEquality)
+open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 ------------------------------------------------------------------------
 -- Re-exporting the builtins publicly
diff --git a/src/Reflection/AST/Argument/Visibility.agda b/src/Reflection/AST/Argument/Visibility.agda
index 4f94b24fe3..b5e9236043 100644
--- a/src/Reflection/AST/Argument/Visibility.agda
+++ b/src/Reflection/AST/Argument/Visibility.agda
@@ -8,9 +8,9 @@
 
 module Reflection.AST.Argument.Visibility where
 
-open import Relation.Nullary                      using (yes; no)
-open import Relation.Binary                       using (DecidableEquality)
-open import Relation.Binary.PropositionalEquality using (refl)
+open import Relation.Nullary                           using (yes; no)
+open import Relation.Binary                            using (DecidableEquality)
+open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 ------------------------------------------------------------------------
 -- Re-exporting the builtins publicly
diff --git a/src/Reflection/AST/Definition.agda b/src/Reflection/AST/Definition.agda
index 5b6dace7cd..7ccabb6f51 100644
--- a/src/Reflection/AST/Definition.agda
+++ b/src/Reflection/AST/Definition.agda
@@ -8,12 +8,12 @@
 
 module Reflection.AST.Definition where
 
-import Data.List.Properties as Listₚ              using (≡-dec)
-import Data.Nat.Properties as ℕₚ                 using (_≟_)
-open import Data.Product                          using (_×_; <_,_>; uncurry)
-open import Relation.Nullary.Decidable            using (map′; _×-dec_; yes; no)
-open import Relation.Binary                       using (DecidableEquality)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)
+import Data.List.Properties as Listₚ                   using (≡-dec)
+import Data.Nat.Properties as ℕₚ                       using (_≟_)
+open import Data.Product                               using (_×_; <_,_>; uncurry)
+open import Relation.Nullary.Decidable                 using (map′; _×-dec_; yes; no)
+open import Relation.Binary                            using (DecidableEquality)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
 
 import Reflection.AST.Argument as Arg
 import Reflection.AST.Name     as Name
diff --git a/src/Reflection/AST/Literal.agda b/src/Reflection/AST/Literal.agda
index 33ceed9ca5..ff8835236a 100644
--- a/src/Reflection/AST/Literal.agda
+++ b/src/Reflection/AST/Literal.agda
@@ -16,10 +16,10 @@ import Data.String as String using (_≟_)
 import Data.Word as Word     using (_≟_)
 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.PropositionalEquality using (_≡_; refl; cong)
+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.PropositionalEquality.Core using (_≡_; refl; cong)
 
 ------------------------------------------------------------------------
 -- Re-exporting the builtin type and constructors
diff --git a/src/Reflection/AST/Meta.agda b/src/Reflection/AST/Meta.agda
index 93584f573c..56bda50d31 100644
--- a/src/Reflection/AST/Meta.agda
+++ b/src/Reflection/AST/Meta.agda
@@ -8,12 +8,12 @@
 
 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)
+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)
 import Relation.Binary.Construct.On as On
-open import Relation.Binary.PropositionalEquality using (_≡_; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 
 open import Agda.Builtin.Reflection public
   using (Meta) renaming (primMetaToNat to toℕ; primMetaEquality to _≡ᵇ_)
diff --git a/src/Reflection/AST/Name.agda b/src/Reflection/AST/Name.agda
index 1baa63029f..a46940e0a5 100644
--- a/src/Reflection/AST/Name.agda
+++ b/src/Reflection/AST/Name.agda
@@ -8,14 +8,14 @@
 
 module Reflection.AST.Name where
 
-open import Data.List.Base                        using (List)
-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.Construct.On          using (decidable)
-open import Relation.Binary.PropositionalEquality using (_≡_; cong)
+open import Data.List.Base              using (List)
+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.Construct.On               using (decidable)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 
 ----------------------------------------------------------------------
 -- Re-export built-ins
diff --git a/src/Reflection/AST/Term.agda b/src/Reflection/AST/Term.agda
index 183f839015..cfa7e70cb1 100644
--- a/src/Reflection/AST/Term.agda
+++ b/src/Reflection/AST/Term.agda
@@ -15,9 +15,9 @@ open import Data.Product            using (_×_; _,_; <_,_>; uncurry; map₁)
 open import Data.Product.Properties using (,-injective)
 open import Data.Maybe.Base         using (Maybe; just; nothing)
 open import Data.String as String   using (String)
-open import Relation.Nullary.Decidable            using (map′; _×-dec_; yes; no)
-open import Relation.Binary                       using (Decidable; DecidableEquality)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)
+open import Relation.Nullary.Decidable                 using (map′; _×-dec_; yes; no)
+open import Relation.Binary                            using (Decidable; DecidableEquality)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong; cong₂)
 
 open import Reflection.AST.Abstraction
 open import Reflection.AST.Argument
diff --git a/src/Relation/Binary/Construct/Add/Extrema/NonStrict.agda b/src/Relation/Binary/Construct/Add/Extrema/NonStrict.agda
index 93a04ce62a..e160bb3b85 100644
--- a/src/Relation/Binary/Construct/Add/Extrema/NonStrict.agda
+++ b/src/Relation/Binary/Construct/Add/Extrema/NonStrict.agda
@@ -17,7 +17,7 @@ module Relation.Binary.Construct.Add.Extrema.NonStrict
 open import Function.Base
 open import Relation.Nullary.Construct.Add.Extrema
 import Relation.Nullary.Construct.Add.Infimum as I
-open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 import Relation.Binary.Construct.Add.Infimum.NonStrict as AddInfimum
 import Relation.Binary.Construct.Add.Supremum.NonStrict as AddSupremum
 import Relation.Binary.Construct.Add.Extrema.Equality as Equality
diff --git a/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda b/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
index c6c313c98c..b6cd5e4bf6 100644
--- a/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
+++ b/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
@@ -16,8 +16,9 @@ module Relation.Binary.Construct.Add.Infimum.NonStrict
 
 open import Level using (_⊔_)
 open import Data.Sum.Base as Sum
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl)
+import Relation.Binary.PropositionalEquality.Properties as P
 import Relation.Binary.Construct.Add.Infimum.Equality as Equality
 open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Construct.Add.Infimum
diff --git a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
index 45463af482..80a0727fc1 100644
--- a/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
+++ b/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
@@ -17,8 +17,9 @@ module Relation.Binary.Construct.Add.Infimum.Strict
 open import Level using (_⊔_)
 open import Data.Product
 open import Function.Base
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl)
+import Relation.Binary.PropositionalEquality.Properties as P
 import Relation.Binary.Construct.Add.Infimum.Equality as Equality
 import Relation.Binary.Construct.Add.Infimum.NonStrict as NonStrict
 open import Relation.Nullary hiding (Irrelevant)
diff --git a/src/Relation/Binary/Construct/Add/Point/Equality.agda b/src/Relation/Binary/Construct/Add/Point/Equality.agda
index a0b01a3d2b..1715d6f2d1 100644
--- a/src/Relation/Binary/Construct/Add/Point/Equality.agda
+++ b/src/Relation/Binary/Construct/Add/Point/Equality.agda
@@ -16,7 +16,7 @@ module Relation.Binary.Construct.Add.Point.Equality
 
 open import Level using (_⊔_)
 open import Function.Base
-import Relation.Binary.PropositionalEquality as P
+import Relation.Binary.PropositionalEquality.Core as P
 open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Construct.Add.Point
 import Relation.Nullary.Decidable as Dec
diff --git a/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda b/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
index be30c7973c..a509871377 100644
--- a/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
+++ b/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
@@ -18,8 +18,9 @@ open import Level using (_⊔_)
 open import Data.Sum.Base as Sum
 open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl)
+import Relation.Binary.PropositionalEquality.Properties as P
 open import Relation.Nullary.Construct.Add.Supremum
 import Relation.Binary.Construct.Add.Supremum.Equality as Equality
 
diff --git a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
index 46415e6895..0bbefc05fa 100644
--- a/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
+++ b/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
@@ -19,8 +19,9 @@ open import Data.Product
 open import Function.Base
 open import Relation.Nullary hiding (Irrelevant)
 import Relation.Nullary.Decidable as Dec
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; refl)
+import Relation.Binary.PropositionalEquality.Properties as P
 open import Relation.Nullary.Construct.Add.Supremum
 import Relation.Binary.Construct.Add.Supremum.Equality as Equality
 import Relation.Binary.Construct.Add.Supremum.NonStrict as NonStrict
diff --git a/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda b/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda
index 9bac46632e..d9bf470f5c 100644
--- a/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda
+++ b/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda
@@ -15,7 +15,8 @@ open import Function.Base using (id)
 open import Level
 open import Relation.Binary hiding (_⇔_)
 open import Relation.Binary.Construct.Closure.Reflexive
-open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core as PropEq using (_≡_; refl)
+import Relation.Binary.PropositionalEquality.Properties as PropEq
 open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec
 open import Relation.Unary using (Pred)
diff --git a/src/Relation/Binary/Construct/Closure/Reflexive/Properties/WithK.agda b/src/Relation/Binary/Construct/Closure/Reflexive/Properties/WithK.agda
index 2ae6422870..26d04320b0 100644
--- a/src/Relation/Binary/Construct/Closure/Reflexive/Properties/WithK.agda
+++ b/src/Relation/Binary/Construct/Closure/Reflexive/Properties/WithK.agda
@@ -10,7 +10,7 @@ module Relation.Binary.Construct.Closure.Reflexive.Properties.WithK where
 
 open import Relation.Binary
 open import Relation.Binary.Construct.Closure.Reflexive
-open import Relation.Binary.PropositionalEquality as PropEq using (_≡_; refl; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 open import Relation.Nullary.Negation using (contradiction)
 
 open import Relation.Binary.Construct.Closure.Reflexive.Properties public
diff --git a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda
index 88e284c2bf..64c81b7151 100644
--- a/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda
+++ b/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda
@@ -11,8 +11,9 @@ module Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties where
 open import Function
 open import Relation.Binary
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
-open import Relation.Binary.PropositionalEquality as PropEq
+open import Relation.Binary.PropositionalEquality.Core as PropEq
   using (_≡_; refl; sym; cong; cong₂)
+import Relation.Binary.PropositionalEquality.Properties as PropEq
 import Relation.Binary.Reasoning.Preorder as PreR
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Binary/Construct/Closure/Transitive.agda b/src/Relation/Binary/Construct/Closure/Transitive.agda
index 1699dc0cb6..551b6f5cb5 100644
--- a/src/Relation/Binary/Construct/Closure/Transitive.agda
+++ b/src/Relation/Binary/Construct/Closure/Transitive.agda
@@ -13,7 +13,7 @@ open import Function.Bundles using (_⇔_; mk⇔)
 open import Induction.WellFounded
 open import Level
 open import Relation.Binary hiding (_⇔_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 private
   variable
diff --git a/src/Relation/Binary/Construct/Closure/Transitive/WithK.agda b/src/Relation/Binary/Construct/Closure/Transitive/WithK.agda
index 1eff43bbca..62816238d9 100644
--- a/src/Relation/Binary/Construct/Closure/Transitive/WithK.agda
+++ b/src/Relation/Binary/Construct/Closure/Transitive/WithK.agda
@@ -11,7 +11,7 @@ module Relation.Binary.Construct.Closure.Transitive.WithK where
 open import Function
 open import Relation.Binary
 open import Relation.Binary.Construct.Closure.Transitive
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 module _ {a ℓ} {A : Set a} {_∼_ : Rel A ℓ} where
 
diff --git a/src/Relation/Binary/HeterogeneousEquality.agda b/src/Relation/Binary/HeterogeneousEquality.agda
index 0a4886531e..1ca855e122 100644
--- a/src/Relation/Binary/HeterogeneousEquality.agda
+++ b/src/Relation/Binary/HeterogeneousEquality.agda
@@ -22,7 +22,8 @@ open import Relation.Binary.Indexed.Heterogeneous
   using (IndexedSetoid)
 open import Relation.Binary.Indexed.Heterogeneous.Construct.At
   using (_atₛ_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
+import Relation.Binary.PropositionalEquality.Properties as P
 
 import Relation.Binary.HeterogeneousEquality.Core as Core
 
diff --git a/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda b/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda
index fb1db6b9fb..d2825a3548 100644
--- a/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda
+++ b/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda
@@ -12,7 +12,7 @@ open import Relation.Binary.HeterogeneousEquality.Quotients
 open import Level using (0ℓ)
 open import Relation.Binary
 open import Relation.Binary.HeterogeneousEquality hiding (isEquivalence)
-import Relation.Binary.PropositionalEquality as ≡
+import Relation.Binary.PropositionalEquality.Core as ≡
 open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Product
diff --git a/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda b/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda
index fd83521783..5ed814cdc1 100644
--- a/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda
+++ b/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda
@@ -15,7 +15,7 @@ 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.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Binary.Indexed.Homogeneous.Core
 open import Relation.Binary.Indexed.Homogeneous.Structures
diff --git a/src/Relation/Binary/Indexed/Homogeneous/Structures.agda b/src/Relation/Binary/Indexed/Homogeneous/Structures.agda
index 1404bf7f52..38db83929a 100644
--- a/src/Relation/Binary/Indexed/Homogeneous/Structures.agda
+++ b/src/Relation/Binary/Indexed/Homogeneous/Structures.agda
@@ -21,7 +21,7 @@ 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.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Binary.Indexed.Homogeneous.Definitions
 
 ------------------------------------------------------------------------
diff --git a/src/Relation/Binary/Reasoning/MultiSetoid.agda b/src/Relation/Binary/Reasoning/MultiSetoid.agda
index 994ac3c4b6..7737e6a779 100644
--- a/src/Relation/Binary/Reasoning/MultiSetoid.agda
+++ b/src/Relation/Binary/Reasoning/MultiSetoid.agda
@@ -29,7 +29,7 @@ module Relation.Binary.Reasoning.MultiSetoid where
 open import Function.Base using (flip)
 open import Level using (_⊔_)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 import Relation.Binary.Reasoning.Setoid as EqR
 
diff --git a/src/Relation/Binary/Reflection.agda b/src/Relation/Binary/Reflection.agda
index 5a9ec838fb..20e2054cfc 100644
--- a/src/Relation/Binary/Reflection.agda
+++ b/src/Relation/Binary/Reflection.agda
@@ -14,7 +14,7 @@ open import Function.Base using (id; _⟨_⟩_)
 open import Function.Bundles using (module Equivalence)
 open import Level using (Level)
 open import Relation.Binary
-import Relation.Binary.PropositionalEquality as P
+import Relation.Binary.PropositionalEquality.Core as P
 
 -- Think of the parameters as follows:
 --
diff --git a/src/Relation/Nary.agda b/src/Relation/Nary.agda
index 5e6ecb5b25..da804883f5 100644
--- a/src/Relation/Nary.agda
+++ b/src/Relation/Nary.agda
@@ -27,7 +27,7 @@ open import Function.Nary.NonDependent
 open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _because_; _×-dec_)
 import Relation.Unary as Unary
-open import Relation.Binary.PropositionalEquality using (_≡_; cong; subst)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst)
 
 private
   variable
diff --git a/src/Relation/Nullary/Construct/Add/Extrema.agda b/src/Relation/Nullary/Construct/Add/Extrema.agda
index 4b88fb3b3e..3366d83c27 100644
--- a/src/Relation/Nullary/Construct/Add/Extrema.agda
+++ b/src/Relation/Nullary/Construct/Add/Extrema.agda
@@ -8,7 +8,7 @@
 
 module Relation.Nullary.Construct.Add.Extrema where
 
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Nullary.Construct.Add.Infimum  as Infimum  using (_₋)
 open import Relation.Nullary.Construct.Add.Supremum as Supremum using (_⁺)
 
diff --git a/src/Relation/Nullary/Universe.agda b/src/Relation/Nullary/Universe.agda
index 4c0308343d..68394c051c 100644
--- a/src/Relation/Nullary/Universe.agda
+++ b/src/Relation/Nullary/Universe.agda
@@ -12,8 +12,8 @@ open import Relation.Nullary
 open import Relation.Nullary.Negation
 open import Relation.Binary hiding (_⇒_)
 import Relation.Binary.Construct.Always as Always
-open import Relation.Binary.PropositionalEquality as PropEq
-  using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+import Relation.Binary.PropositionalEquality.Properties as PropEq
 import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial
   as Trivial
 open import Data.Sum     as Sum  hiding (map)
diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda
index 25e21193be..e46392ee5d 100644
--- a/src/Tactic/Cong.agda
+++ b/src/Tactic/Cong.agda
@@ -36,7 +36,7 @@ open import Data.Unit.Base            using (⊤)
 open import Data.Word.Base   as Word  using (toℕ)
 open import Data.Product
 
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong)
+open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_; refl; cong)
 
 -- 'Data.String.Properties' defines this via 'Dec', so let's use the builtin
 -- for maximum speed.
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
index d04ecbc131..1eb2244f5d 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
@@ -22,7 +22,7 @@ open import Data.Vec                  using (Vec)
 open import Function
 open import Relation.Unary
 
-import Relation.Binary.PropositionalEquality as ≡
+import Relation.Binary.PropositionalEquality.Core as ≡
 
 open Homomorphism homo hiding (_^_)
 open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas homo
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda
index 6fda530012..ca622ab00a 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda
@@ -21,7 +21,7 @@ open import Data.List.Kleene
 open import Data.Vec      using (Vec)
 
 import Data.Nat.Properties as ℕ-Prop
-import Relation.Binary.PropositionalEquality as ≡
+import Relation.Binary.PropositionalEquality.Core as ≡
 
 open Homomorphism homo
 open import Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas homo
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda
index ce20b1e381..6f2eba31d7 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda
@@ -13,20 +13,20 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas
   (homo : Homomorphism r₁ r₂ r₃ r₄)
   where
 
-open import Data.Bool                                  using (Bool;true;false)
-open import Data.Nat.Base as ℕ                         using (ℕ; suc; zero; compare; _≤′_; ≤′-step; ≤′-refl)
-open import Data.Nat.Properties as ℕₚ                  using (≤′-trans)
-open import Data.Vec.Base as Vec                       using (Vec; _∷_)
-open import Data.Fin                                   using (Fin; zero; suc)
-open import Data.List.Base                             using (_∷_; [])
+open import Data.Bool                                       using (Bool;true;false)
+open import Data.Nat.Base as ℕ                              using (ℕ; suc; zero; compare; _≤′_; ≤′-step; ≤′-refl)
+open import Data.Nat.Properties as ℕₚ                       using (≤′-trans)
+open import Data.Vec.Base as Vec                            using (Vec; _∷_)
+open import Data.Fin                                        using (Fin; zero; suc)
+open import Data.List.Base                                  using (_∷_; [])
 open import Data.Unit using (tt)
 open import Data.List.Kleene
-open import Data.Product                               using (_,_; proj₁; proj₂; map₁; _×_)
-open import Data.Maybe                                 using (nothing; just)
+open import Data.Product                                    using (_,_; proj₁; proj₂; map₁; _×_)
+open import Data.Maybe                                      using (nothing; just)
 open import Function
-open import Level                                      using (lift)
-open import Relation.Nullary                           using (Dec; yes; no)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+open import Level                                           using (lift)
+open import Relation.Nullary                                using (Dec; yes; no)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 
 open Homomorphism homo hiding (_^_)
 open import Tactic.RingSolver.Core.Polynomial.Reasoning to
diff --git a/src/Text/Regex/Derivative/Brzozowski.agda b/src/Text/Regex/Derivative/Brzozowski.agda
index ca3768296b..d368bfc70d 100644
--- a/src/Text/Regex/Derivative/Brzozowski.agda
+++ b/src/Text/Regex/Derivative/Brzozowski.agda
@@ -19,7 +19,7 @@ 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.PropositionalEquality using (_≡_; refl; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
 open DecPoset P? using (preorder) renaming (Carrier to A)
 open import Text.Regex.Base preorder as R hiding (_∣_; _∙_; _⋆)
diff --git a/src/Text/Regex/Properties.agda b/src/Text/Regex/Properties.agda
index 2652f9c8cf..cf807ca3f3 100644
--- a/src/Text/Regex/Properties.agda
+++ b/src/Text/Regex/Properties.agda
@@ -24,7 +24,6 @@ open import Relation.Nullary.Negation
 
 import Relation.Unary  as U
 open import Relation.Binary using (Decidable)
-import Relation.Binary.PropositionalEquality as P
 
 open DecPoset P? renaming (Carrier to A)
 open import Text.Regex.Base preorder
diff --git a/src/Text/Regex/Search.agda b/src/Text/Regex/Search.agda
index c802768e38..f5c8c780c3 100644
--- a/src/Text/Regex/Search.agda
+++ b/src/Text/Regex/Search.agda
@@ -30,7 +30,7 @@ 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.PropositionalEquality hiding (preorder)
+open import Relation.Binary.PropositionalEquality.Core
 
 open DecPoset P? using (preorder) renaming (Carrier to A)
 open import Text.Regex.Base preorder
diff --git a/src/Text/Regex/SmartConstructors.agda b/src/Text/Regex/SmartConstructors.agda
index eecda1284f..afe9d3f936 100644
--- a/src/Text/Regex/SmartConstructors.agda
+++ b/src/Text/Regex/SmartConstructors.agda
@@ -19,7 +19,7 @@ open import Data.Sum.Base using (inj₁; inj₂; fromInj₁; fromInj₂)
 
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Binary.PropositionalEquality using (refl)
+open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 open import Text.Regex.Base P as R hiding (_∣_; _∙_; _⋆)
 open import Text.Regex.Properties.Core P
diff --git a/src/Text/Regex/String/Unsafe.agda b/src/Text/Regex/String/Unsafe.agda
index bc6c9fc0d7..a46fcd5655 100644
--- a/src/Text/Regex/String/Unsafe.agda
+++ b/src/Text/Regex/String/Unsafe.agda
@@ -13,7 +13,7 @@ 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.PropositionalEquality using (_≡_; sym; subst)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; sym; subst)
 open import Relation.Nullary.Decidable using (map′)
 
 ------------------------------------------------------------------------