diff --git a/README/Case.agda b/README/Case.agda
index 358460a63b..938a2ba1ad 100644
--- a/README/Case.agda
+++ b/README/Case.agda
@@ -18,7 +18,6 @@ open import Data.Product
 open import Function.Base using (case_of_; case_return_of_)
 open import Relation.Nullary
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality
 
 ------------------------------------------------------------------------
 -- Different types of pattern-matching lambdas
diff --git a/README/Data/List/Relation/Binary/Equality.agda b/README/Data/List/Relation/Binary/Equality.agda
index 6201dc5c5d..4ce5fe2478 100644
--- a/README/Data/List/Relation/Binary/Equality.agda
+++ b/README/Data/List/Relation/Binary/Equality.agda
@@ -54,7 +54,7 @@ open import Relation.Binary.PropositionalEquality using (_≗_)
 -- to `_≗_`. However instead of using the pointwise module directly
 -- to write:
 
-open import Data.List.Relation.Binary.Pointwise using (Pointwise)
+open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise)
 
 lem₃ : Pointwise _≗_ ((λ x → x + 1) ∷ []) ((λ x → x + 2 ∸ 1) ∷ [])
 lem₃ = {!!}
diff --git a/README/Inspect.agda b/README/Inspect.agda
index cff492d008..002005abaa 100644
--- a/README/Inspect.agda
+++ b/README/Inspect.agda
@@ -15,7 +15,8 @@ module README.Inspect where
 open import Data.Nat.Base
 open import Data.Nat.Properties
 open import Data.Product
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality using (inspect)
 
 ------------------------------------------------------------------------
 -- Using inspect
diff --git a/src/Codata/Sized/Colist/Bisimilarity.agda b/src/Codata/Sized/Colist/Bisimilarity.agda
index 9efbcebbca..d66ade8b89 100644
--- a/src/Codata/Sized/Colist/Bisimilarity.agda
+++ b/src/Codata/Sized/Colist/Bisimilarity.agda
@@ -13,7 +13,7 @@ open import Size
 open import Codata.Sized.Thunk
 open import Codata.Sized.Colist
 open import Data.List.Base using (List; []; _∷_)
-open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
+open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
 open import Data.List.NonEmpty as List⁺  using (List⁺; _∷_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
diff --git a/src/Codata/Sized/Stream/Bisimilarity.agda b/src/Codata/Sized/Stream/Bisimilarity.agda
index 74419c7809..c036d030b7 100644
--- a/src/Codata/Sized/Stream/Bisimilarity.agda
+++ b/src/Codata/Sized/Stream/Bisimilarity.agda
@@ -13,7 +13,7 @@ open import Codata.Sized.Thunk
 open import Codata.Sized.Stream
 open import Level
 open import Data.List.NonEmpty as List⁺ using (_∷_)
-open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
+open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as Eq
diff --git a/src/Data/Container/Indexed/FreeMonad.agda b/src/Data/Container/Indexed/FreeMonad.agda
index f2fe0d2aab..1c6ee81c1a 100644
--- a/src/Data/Container/Indexed/FreeMonad.agda
+++ b/src/Data/Container/Indexed/FreeMonad.agda
@@ -19,7 +19,7 @@ open import Data.Product
 open import Data.W.Indexed
 open import Relation.Unary
 open import Relation.Unary.PredicateTransformer
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core using (refl)
 
 ------------------------------------------------------------------------
 
diff --git a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
index f9610d5422..cc067dc846 100644
--- a/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
@@ -22,8 +22,7 @@ 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.Core using (_≢_; refl; cong)
-
-open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise)
+open import Data.List.Relation.Binary.Pointwise.Base as Pointwise using (Pointwise)
 open import Data.List.Relation.Binary.Infix.Heterogeneous
 open import Data.List.Relation.Binary.Prefix.Heterogeneous
   as Prefix using (Prefix; []; _∷_)
diff --git a/src/Data/List/Relation/Binary/Lex/NonStrict.agda b/src/Data/List/Relation/Binary/Lex/NonStrict.agda
index 83c8767cb3..4606c9cdbd 100644
--- a/src/Data/List/Relation/Binary/Lex/NonStrict.agda
+++ b/src/Data/List/Relation/Binary/Lex/NonStrict.agda
@@ -16,7 +16,7 @@ open import Function.Base
 open import Data.Unit.Base using (⊤; tt)
 open import Data.Product
 open import Data.List.Base
-open import Data.List.Relation.Binary.Pointwise using (Pointwise; [])
+open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; [])
 import Data.List.Relation.Binary.Lex.Strict as Strict
 open import Level
 open import Relation.Nullary
diff --git a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
index 9e247e734b..6b9fd9c20d 100644
--- a/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
@@ -9,8 +9,10 @@
 module Data.List.Relation.Binary.Permutation.Homogeneous where
 
 open import Data.List.Base using (List; _∷_)
-open import Data.List.Relation.Binary.Pointwise as Pointwise
+open import Data.List.Relation.Binary.Pointwise.Base as Pointwise
   using (Pointwise)
+open import Data.List.Relation.Binary.Pointwise.Properties as Pointwise
+  using (symmetric)
 open import Level using (Level; _⊔_)
 open import Relation.Binary
 
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid.agda b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
index 5a147d8008..a9a0cf6400 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid.agda
@@ -13,7 +13,7 @@ module Data.List.Relation.Binary.Permutation.Setoid
 
 open import Data.List.Base using (List; _∷_)
 import Data.List.Relation.Binary.Permutation.Homogeneous as Homogeneous
-import Data.List.Relation.Binary.Pointwise as Pointwise
+import Data.List.Relation.Binary.Pointwise.Properties as Pointwise using (refl)
 open import Data.List.Relation.Binary.Equality.Setoid S
 open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Level using (_⊔_)
diff --git a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
index da5a26e6e0..3f803d952d 100644
--- a/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
+++ b/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
@@ -15,7 +15,7 @@ open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 import Data.List.Relation.Unary.All.Properties as All
 open import Data.List.Base as List hiding (map; uncons)
 open import Data.List.Membership.Propositional.Properties using ([]∈inits)
-open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
+open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
 open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix hiding (PrefixView; _++_)
 open import Data.Nat.Base using (ℕ; zero; suc; _≤_; z≤n; s≤s)
 open import Data.Nat.Properties using (suc-injective)
diff --git a/src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda b/src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda
index 984b857c59..aeeb927d2d 100644
--- a/src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda
+++ b/src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda
@@ -11,7 +11,7 @@ module Data.List.Relation.Binary.Suffix.Heterogeneous where
 open import Level
 open import Relation.Binary using (REL; _⇒_)
 open import Data.List.Base as List using (List; []; _∷_)
-open import Data.List.Relation.Binary.Pointwise as Pointwise
+open import Data.List.Relation.Binary.Pointwise.Base as Pointwise
   using (Pointwise; []; _∷_)
 
 module _ {a b r} {A : Set a} {B : Set b} (R : REL A B r) where
diff --git a/src/Data/List/Relation/Ternary/Appending.agda b/src/Data/List/Relation/Ternary/Appending.agda
index 0d1f935414..802f80aac3 100644
--- a/src/Data/List/Relation/Ternary/Appending.agda
+++ b/src/Data/List/Relation/Ternary/Appending.agda
@@ -10,7 +10,7 @@ module Data.List.Relation.Ternary.Appending {a b c} {A : Set a} {B : Set b} {C :
 
 open import Level using (Level; _⊔_)
 open import Data.List.Base as List using (List; []; _∷_)
-open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
+open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
 open import Data.Product as Prod using (∃₂; _×_; _,_; -,_)
 open import Relation.Binary using (REL)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
diff --git a/src/Data/List/Relation/Ternary/Appending/Properties.agda b/src/Data/List/Relation/Ternary/Appending/Properties.agda
index 4508a7f719..6c02c49ffb 100644
--- a/src/Data/List/Relation/Ternary/Appending/Properties.agda
+++ b/src/Data/List/Relation/Ternary/Appending/Properties.agda
@@ -10,7 +10,8 @@ module Data.List.Relation.Ternary.Appending.Properties where
 
 open import Data.List.Base using (List; [])
 open import Data.List.Relation.Ternary.Appending
-open import Data.List.Relation.Binary.Pointwise as Pw using (Pointwise; []; _∷_)
+open import Data.List.Relation.Binary.Pointwise.Base as Pw using (Pointwise; []; _∷_)
+open import Data.List.Relation.Binary.Pointwise.Properties as Pw using (transitive)
 open import Level using (Level)
 open import Relation.Binary using (REL; Rel; Trans)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
diff --git a/src/Data/List/Relation/Ternary/Appending/Propositional.agda b/src/Data/List/Relation/Ternary/Appending/Propositional.agda
index 6149e2a236..46567a01ed 100644
--- a/src/Data/List/Relation/Ternary/Appending/Propositional.agda
+++ b/src/Data/List/Relation/Ternary/Appending/Propositional.agda
@@ -14,8 +14,7 @@ open import Data.List.Base as List using (List; []; _∷_)
 open import Data.Product using (_,_)
 
 import Data.List.Properties as Listₚ
-import Data.List.Relation.Binary.Pointwise as Pw
-
+import Data.List.Relation.Binary.Pointwise as Pw using (≡⇒Pointwise-≡; Pointwise-≡⇒≡)
 open import Relation.Binary.PropositionalEquality
   using (_≡_; setoid; refl; trans; cong₂; module ≡-Reasoning)
 
diff --git a/src/Data/List/Relation/Ternary/Appending/Propositional/Properties.agda b/src/Data/List/Relation/Ternary/Appending/Propositional/Properties.agda
index 757d888012..54e19f59d2 100644
--- a/src/Data/List/Relation/Ternary/Appending/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Ternary/Appending/Propositional/Properties.agda
@@ -10,7 +10,7 @@ module Data.List.Relation.Ternary.Appending.Propositional.Properties {a} {A : Se
 
 open import Data.List.Base as List using (List; [])
 import Data.List.Properties as Listₚ
-import Data.List.Relation.Binary.Pointwise as Pw
+import Data.List.Relation.Binary.Pointwise as Pw using (Pointwise-≡⇒≡)
 open import Data.List.Relation.Binary.Equality.Propositional using (_≋_)
 open import Data.List.Relation.Ternary.Appending.Propositional {A = A}
 open import Function.Base using (_∘′_)
diff --git a/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda b/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda
index 0530b8b965..c205170359 100644
--- a/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda
@@ -12,7 +12,7 @@ module Data.List.Relation.Ternary.Appending.Setoid.Properties {c l} (S : Setoid
 
 open import Data.List.Base as List using (List; [])
 import Data.List.Properties as Listₚ
-open import Data.List.Relation.Binary.Pointwise using (Pointwise; [])
+open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; [])
 import Data.List.Relation.Ternary.Appending.Properties as Appendingₚ
 open import Data.Product using (_,_)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
diff --git a/src/Data/List/Relation/Ternary/Interleaving.agda b/src/Data/List/Relation/Ternary/Interleaving.agda
index 62206daf2c..158701fc7e 100644
--- a/src/Data/List/Relation/Ternary/Interleaving.agda
+++ b/src/Data/List/Relation/Ternary/Interleaving.agda
@@ -11,7 +11,7 @@ module Data.List.Relation.Ternary.Interleaving where
 
 open import Level
 open import Data.List.Base as List using (List; []; _∷_; _++_)
-open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
+open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
 open import Data.Product as Prod using (∃; ∃₂; _×_; uncurry; _,_; -,_; proj₂)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Function.Base
diff --git a/src/Data/List/Relation/Ternary/Interleaving/Properties.agda b/src/Data/List/Relation/Ternary/Interleaving/Properties.agda
index 563adfc9d9..c15645e205 100644
--- a/src/Data/List/Relation/Ternary/Interleaving/Properties.agda
+++ b/src/Data/List/Relation/Ternary/Interleaving/Properties.agda
@@ -15,7 +15,9 @@ open import Data.List.Properties using (reverse-involutive)
 open import Data.List.Relation.Ternary.Interleaving hiding (map)
 open import Function
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality
+--open import Relation.Binary.PropositionalEquality
+--  using (_≡_; refl; sym; cong; module ≡-Reasoning)
+open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; sym; cong; module ≡-Reasoning)
 open ≡-Reasoning
 
diff --git a/src/Data/List/Relation/Unary/All/Properties.agda b/src/Data/List/Relation/Unary/All/Properties.agda
index 004424df80..da3de23dd9 100644
--- a/src/Data/List/Relation/Unary/All/Properties.agda
+++ b/src/Data/List/Relation/Unary/All/Properties.agda
@@ -25,7 +25,7 @@ open import Data.List.Relation.Unary.All as All using
   )
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 import Data.List.Relation.Binary.Equality.Setoid as ListEq using (_≋_; []; _∷_)
-open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
+open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; []; _∷_)
 open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.All as Maybe using (just; nothing)
diff --git a/src/Data/String.agda b/src/Data/String.agda
index fffe1ac300..8061e64b0e 100644
--- a/src/Data/String.agda
+++ b/src/Data/String.agda
@@ -16,7 +16,7 @@ import Data.Nat.Properties as ℕₚ
 open import Data.List.Base as List using (List; _∷_; []; [_])
 open import Data.List.NonEmpty as NE using (List⁺)
 open import Data.List.Extrema ℕₚ.≤-totalOrder
-open import Data.List.Relation.Binary.Pointwise using (Pointwise)
+open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise)
 open import Data.List.Relation.Binary.Lex.Strict using (Lex-<; Lex-≤)
 open import Data.Vec.Base as Vec using (Vec)
 open import Data.Char.Base as Char using (Char)
diff --git a/src/Text/Regex/Properties.agda b/src/Text/Regex/Properties.agda
index cf807ca3f3..9ade079d87 100644
--- a/src/Text/Regex/Properties.agda
+++ b/src/Text/Regex/Properties.agda
@@ -27,8 +27,7 @@ open import Relation.Binary using (Decidable)
 
 open DecPoset P? renaming (Carrier to A)
 open import Text.Regex.Base preorder
-
-open import Data.List.Relation.Binary.Pointwise using ([])
+open import Data.List.Relation.Binary.Pointwise.Base using ([])
 open import Data.List.Relation.Ternary.Appending.Propositional {A = A}
 open import Data.List.Relation.Ternary.Appending.Propositional.Properties {A = A}