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

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

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

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

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/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)
 
 ------------------------------------------------------------------------
 

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/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/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/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/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

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/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
 

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)

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}