Simplify import of Data.List.Relation.Binary.Pointwise in agda-stdl

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₃ = {!!}

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 (_≡_)

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

src/Data/List/Relation/Binary/Equality/DecSetoid.agda

@@ -12,7 +12,8 @@ module Data.List.Relation.Binary.Equality.DecSetoid
   {a ℓ} (DS : DecSetoid a ℓ) where
 
 import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
-import Data.List.Relation.Binary.Pointwise as PW
+import Data.List.Relation.Binary.Pointwise as PW using (isDecEquivalence; decSetoid)
+import Data.List.Relation.Binary.Pointwise.Properties as PW using (decidable)
 open import Level
 open import Relation.Binary using (Decidable)
 open DecSetoid DS

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; []; _∷_)

src/Data/List/Relation/Binary/Infix/Homogeneous/Properties.agda

@@ -12,7 +12,9 @@ open import Level
 open import Function.Base using (_∘′_)
 open import Relation.Binary
 
-open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise)
+open import Data.List.Relation.Binary.Pointwise.Base as Pointwise using (Pointwise)
+import Data.List.Relation.Binary.Pointwise as Pointwise using (isEquivalence)
+open import Data.List.Relation.Binary.Pointwise.Properties as Pointwise using (decidable)
 open import Data.List.Relation.Binary.Infix.Heterogeneous
 open import Data.List.Relation.Binary.Infix.Heterogeneous.Properties
 

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

src/Data/List/Relation/Binary/Lex/Strict.agda

@@ -21,9 +21,10 @@ open import Level using (_⊔_)
 open import Relation.Nullary using (yes; no; ¬_)
 open import Relation.Binary
 open import Relation.Binary.Consequences
-open import Data.List.Relation.Binary.Pointwise as Pointwise
+open import Data.List.Relation.Binary.Pointwise.Base as Pointwise
    using (Pointwise; []; _∷_; head; tail)
-
+import Data.List.Relation.Binary.Pointwise as Pointwise using (isEquivalence)
+open import Data.List.Relation.Binary.Pointwise.Properties as Pointwise using (decidable)
 import Data.List.Relation.Binary.Lex as Core
 
 ----------------------------------------------------------------------

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
 

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 (_⊔_)

src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda

@@ -15,8 +15,10 @@ module Data.List.Relation.Binary.Permutation.Setoid.Properties
 open import Algebra
 open import Data.Bool.Base using (true; false)
 open import Data.List.Base as List hiding (head; tail)
-open import Data.List.Relation.Binary.Pointwise as Pointwise
-  using (Pointwise; head; tail)
+import Data.List.Relation.Binary.Pointwise.Base as Pointwise
+  using (Pointwise; head; tail; map)
+import Data.List.Relation.Binary.Pointwise as Pointwise
+  using (map⁺; ++⁺)
 import Data.List.Relation.Binary.Equality.Setoid as Equality
 import Data.List.Relation.Binary.Permutation.Setoid as Permutation
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
@@ -319,43 +321,43 @@ dropMiddleElement {v} ws xs {ys} {zs} p = helper p ws xs ≋-refl ≋-refl
   helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈w y≈w p) [] (x ∷ []) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
     ys               ≋⟨  ≋₁ ⟩
     a ∷ as           ↭⟨  prep y≈w p ⟩
-    _ ∷ bs           ≋˘⟨ ≈₂ ∷ tail ≋₂ ⟩
+    _ ∷ bs           ≋˘⟨ ≈₂ ∷ Pointwise.tail ≋₂ ⟩
     x ∷ zs           ∎
   helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap v≈w y≈x p) [] (x ∷ w ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
     ys               ≋⟨ ≋₁ ⟩
     a ∷ as           ↭⟨ prep y≈x p ⟩
-    _ ∷ bs           ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩
-    x ∷ xs ++ v ∷ zs ↭⟨ prep ≈-refl (shift (lemma ≈₁ v≈w (head ≋₂)) xs zs) ⟩
+    _ ∷ bs           ≋⟨ ≋-sym (≈₂ ∷ Pointwise.tail ≋₂) ⟩
+    x ∷ xs ++ v ∷ zs ↭⟨ prep ≈-refl (shift (lemma ≈₁ v≈w (Pointwise.head ≋₂)) xs zs) ⟩
     x ∷ w ∷ xs ++ zs ∎
   helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap w≈x _ p) (w ∷ []) [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    w ∷ ys           ≋⟨ ≈₁ ∷ tail (≋₁) ⟩
+    w ∷ ys           ≋⟨ ≈₁ ∷ Pointwise.tail (≋₁) ⟩
     _ ∷ as           ↭⟨ prep w≈x p ⟩
     b ∷ bs           ≋⟨ ≋-sym ≋₂ ⟩
     zs               ∎
   helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap w≈y x≈v p) (w ∷ x ∷ ws) [] {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    w ∷ x ∷ ws ++ ys ↭⟨ prep ≈-refl (↭-sym (shift (lemma ≈₂ (≈-sym x≈v) (head ≋₁)) ws ys)) ⟩
-    w ∷ ws ++ v ∷ ys ≋⟨ ≈₁ ∷ tail ≋₁ ⟩
+    w ∷ x ∷ ws ++ ys ↭⟨ prep ≈-refl (↭-sym (shift (lemma ≈₂ (≈-sym x≈v) (Pointwise.head ≋₁)) ws ys)) ⟩
+    w ∷ ws ++ v ∷ ys ≋⟨ ≈₁ ∷ Pointwise.tail ≋₁ ⟩
     _ ∷ as           ↭⟨ prep w≈y p ⟩
     b ∷ bs           ≋⟨ ≋-sym ≋₂ ⟩
     zs               ∎
   helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap x≈v v≈y p) (x ∷ []) (y ∷ []) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    x ∷ ys           ≋⟨ ≈₁ ∷ tail ≋₁ ⟩
-    _ ∷ as           ↭⟨ prep (≈-trans x≈v (≈-trans (≈-sym (head ≋₂)) (≈-trans (head ≋₁) v≈y))) p ⟩
-    _ ∷ bs           ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩
+    x ∷ ys           ≋⟨ ≈₁ ∷ Pointwise.tail ≋₁ ⟩
+    _ ∷ as           ↭⟨ prep (≈-trans x≈v (≈-trans (≈-sym (Pointwise.head ≋₂)) (≈-trans (Pointwise.head ≋₁) v≈y))) p ⟩
+    _ ∷ bs           ≋⟨ ≋-sym (≈₂ ∷ Pointwise.tail ≋₂) ⟩
     y ∷ zs           ∎
   helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap y≈w v≈z p) (y ∷ []) (z ∷ w ∷ xs) {ys} {zs} (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    y ∷ ys           ≋⟨ ≈₁ ∷ tail ≋₁ ⟩
+    y ∷ ys           ≋⟨ ≈₁ ∷ Pointwise.tail ≋₁ ⟩
     _ ∷ as           ↭⟨ prep y≈w p ⟩
     _ ∷ bs           ≋⟨ ≋-sym ≋₂ ⟩
     w ∷ xs ++ v ∷ zs ↭⟨ ↭-prep w (↭-shift xs zs) ⟩
-    w ∷ v ∷ xs ++ zs ↭⟨ swap ≈-refl (lemma (head ≋₁) v≈z ≈₂) ↭-refl ⟩
+    w ∷ v ∷ xs ++ zs ↭⟨ swap ≈-refl (lemma (Pointwise.head ≋₁) v≈z ≈₂) ↭-refl ⟩
     z ∷ w ∷ xs ++ zs ∎
   helper {_ ∷ a ∷ as} {_ ∷ b ∷ bs} (swap y≈v w≈z p) (y ∷ w ∷ ws) (z ∷ []) {ys} {zs}    (≈₁ ∷ ≋₁) (≈₂ ∷ ≋₂) = begin
-    y ∷ w ∷ ws ++ ys ↭⟨ swap (lemma ≈₁ y≈v (head ≋₂)) ≈-refl ↭-refl ⟩
+    y ∷ w ∷ ws ++ ys ↭⟨ swap (lemma ≈₁ y≈v (Pointwise.head ≋₂)) ≈-refl ↭-refl ⟩
     w ∷ v ∷ ws ++ ys ↭⟨ ↭-prep w (↭-sym (↭-shift ws ys)) ⟩
     w ∷ ws ++ v ∷ ys ≋⟨ ≋₁ ⟩
     _ ∷ as           ↭⟨ prep w≈z p ⟩
-    _ ∷ bs           ≋⟨ ≋-sym (≈₂ ∷ tail ≋₂) ⟩
+    _ ∷ bs           ≋⟨ ≋-sym (≈₂ ∷ Pointwise.tail ≋₂) ⟩
     z ∷ zs           ∎
   helper (swap x≈z y≈w p) (x ∷ y ∷ ws) (w ∷ z ∷ xs) {ys} {zs} (≈₁ ∷ ≈₃ ∷ ≋₁) (≈₂ ∷ ≈₄ ∷ ≋₂) = begin
     x ∷ y ∷ ws ++ ys ↭⟨ swap (lemma ≈₁ x≈z ≈₄) (lemma ≈₃ y≈w ≈₂) (helper p ws xs ≋₁ ≋₂) ⟩

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)

src/Data/List/Relation/Binary/Prefix/Homogeneous/Properties.agda

@@ -11,8 +11,8 @@ module Data.List.Relation.Binary.Prefix.Homogeneous.Properties where
 open import Level
 open import Function.Base using (_∘′_)
 open import Relation.Binary
-
-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.Pointwise as Pointwise using (isEquivalence)
 open import Data.List.Relation.Binary.Prefix.Heterogeneous
 open import Data.List.Relation.Binary.Prefix.Heterogeneous.Properties
 

src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda

@@ -18,7 +18,9 @@ open import Data.List.Base as List hiding (map; _∷ʳ_)
 import Data.List.Properties as Lₚ
 open import Data.List.Relation.Unary.Any.Properties
   using (here-injective; there-injective)
-open import Data.List.Relation.Binary.Pointwise as Pw using (Pointwise; []; _∷_)
+open import Data.List.Relation.Binary.Pointwise.Base as Pw using (Pointwise; []; _∷_)
+import Data.List.Relation.Binary.Pointwise.Properties as Pw using (refl; decidable)
+import Data.List.Relation.Binary.Pointwise as Pw using (isEquivalence)
 open import Data.List.Relation.Binary.Sublist.Heterogeneous
 
 open import Data.Maybe.Relation.Unary.All as MAll using (nothing; just)

src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda

@@ -11,9 +11,10 @@ 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
 
   infixr 5 _++_

src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda

@@ -11,8 +11,12 @@ module Data.List.Relation.Binary.Suffix.Heterogeneous.Properties where
 open import Data.Bool.Base using (true; false)
 open import Data.List.Base as List
   using (List; []; _∷_; _++_; length; filter; replicate; reverse; reverseAcc)
-open import Data.List.Relation.Binary.Pointwise as Pw
-  using (Pointwise; []; _∷_; Pointwise-length)
+open import Data.List.Relation.Binary.Pointwise.Base as Pw
+  using (Pointwise; []; _∷_)
+import Data.List.Relation.Binary.Pointwise as Pw
+  using (Pointwise-length; reverse⁺; ++⁺; map⁺; map⁻; filter⁺; replicate⁺)
+import Data.List.Relation.Binary.Pointwise.Properties as Pw
+  using (transitive; antisymmetric; irrelevant)
 open import Data.List.Relation.Binary.Suffix.Heterogeneous as Suffix
   using (Suffix; here; there; tail)
 open import Data.List.Relation.Binary.Prefix.Heterogeneous as Prefix
@@ -75,7 +79,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 
   length-mono : ∀ {as bs} → Suffix R as bs → length as ≤ length bs
-  length-mono (here rs)   = ≤-reflexive (Pointwise-length rs)
+  length-mono (here rs)   = ≤-reflexive (Pw.Pointwise-length rs)
   length-mono (there suf) = m≤n⇒m≤1+n (length-mono suf)
 
   S[as][bs]⇒∣as∣≢1+∣bs∣ : ∀ {as bs} → Suffix R as bs →
@@ -139,7 +143,7 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
       length ds                   ≤⟨ m≤n+m (length ds) (length bs) ⟩
       length bs + length ds       <⟨ ≤-refl ⟩
       suc (length bs + length ds) ≡⟨ sym $ Listₚ.length-++ (b ∷ bs) ⟩
-      length (b ∷ bs ++ ds)       ≡⟨ sym $ Pointwise-length rs ⟩
+      length (b ∷ bs ++ ds)       ≡⟨ sym $ Pw.Pointwise-length rs ⟩
       length cs                   ∎
 
 ------------------------------------------------------------------------
@@ -199,8 +203,8 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 
   irrelevant : Irrelevant R → Irrelevant (Suffix R)
   irrelevant irr (here  rs)   (here  rs₁)   = P.cong here $ Pw.irrelevant irr rs rs₁
-  irrelevant irr (here  rs)   (there rsuf)  = contradiction (Pointwise-length rs) (S[as][bs]⇒∣as∣≢1+∣bs∣ rsuf)
-  irrelevant irr (there rsuf) (here  rs)    = contradiction (Pointwise-length rs) (S[as][bs]⇒∣as∣≢1+∣bs∣ rsuf)
+  irrelevant irr (here  rs)   (there rsuf)  = contradiction (Pw.Pointwise-length rs) (S[as][bs]⇒∣as∣≢1+∣bs∣ rsuf)
+  irrelevant irr (there rsuf) (here  rs)    = contradiction (Pw.Pointwise-length rs) (S[as][bs]⇒∣as∣≢1+∣bs∣ rsuf)
   irrelevant irr (there rsuf) (there rsuf₁) = P.cong there $ irrelevant irr rsuf rsuf₁
 
 ------------------------------------------------------------------------

src/Data/List/Relation/Binary/Suffix/Homogeneous/Properties.agda

@@ -12,7 +12,8 @@ open import Level
 open import Function.Base using (_∘′_)
 open import Relation.Binary
 
-open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise)
+open import Data.List.Relation.Binary.Pointwise as Pointwise using (isEquivalence)
+open import Data.List.Relation.Binary.Pointwise.Base as Pointwise using (Pointwise)
 open import Data.List.Relation.Binary.Suffix.Heterogeneous
 open import Data.List.Relation.Binary.Suffix.Heterogeneous.Properties
 

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)

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)

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)
 

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 (_∘′_)

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)

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

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)

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)