Move pointwise equality to .Core module (#2335)

* Closes #2331.

Also makes a few changes of imports that are related. Many of the places
which look like this improvement might also help use other things from
`Relation.Binary.PropositionalEquality` that should *not* be moved to `.Core`.
(But it might make sense to split them off into their own lighter weight module.)

* don't import Data.Nullary itself since its sub-modules were already imported, just redistribute the using properly.

Author: JacquesCarette

src/Algebra/Properties/Monoid/Sum.agda

@@ -13,7 +13,7 @@ open import Data.Fin.Base using (zero; suc)
 open import Data.Unit using (tt)
 open import Function.Base using (_∘_)
 open import Relation.Binary.Core using (_Preserves_⟶_)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≗_; _≡_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≗_; _≡_)
 
 module Algebra.Properties.Monoid.Sum {a ℓ} (M : Monoid a ℓ) where
 

src/Data/List/Effectful.agda

@@ -10,14 +10,19 @@ module Data.List.Effectful where
 
 open import Data.Bool.Base using (false; true)
 open import Data.List.Base
+  using (List; map; [_]; ap; []; _∷_; _++_; concat; concatMap)
 open import Data.List.Properties
-open import Effect.Choice
-open import Effect.Empty
-open import Effect.Functor
+  using (++-identityʳ; ++-assoc; map-cong; concatMap-cong; map-concatMap;
+    concatMap-pure)
+open import Effect.Choice using (RawChoice)
+open import Effect.Empty using (RawEmpty)
+open import Effect.Functor using (RawFunctor)
 open import Effect.Applicative
+  using (RawApplicative; RawApplicativeZero; RawAlternative)
 open import Effect.Monad
-open import Function.Base
-open import Level
+  using (RawMonad; module Join; RawMonadZero; RawMonadPlus)
+open import Function.Base using (flip; _∘_; const; _$_; id; _∘′_; _$′_)
+open import Level using (Level)
 open import Relation.Binary.PropositionalEquality as ≡
   using (_≡_; _≢_; _≗_; refl)
 open ≡.≡-Reasoning

src/Data/List/Membership/Propositional/Properties.agda

@@ -37,7 +37,7 @@ open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions as Binary hiding (Decidable)
 open import Relation.Binary.PropositionalEquality as ≡
-  using (_≡_; _≢_; refl; sym; trans; cong; subst; →-to-⟶; _≗_)
+  using (_≡_; _≢_; refl; sym; trans; cong; subst; _≗_)
 import Relation.Binary.Properties.DecTotalOrder as DTOProperties
 open import Relation.Unary using (_⟨×⟩_; Decidable)
 import Relation.Nullary.Reflects as Reflects

src/Data/List/Relation/Unary/All/Properties.agda

@@ -11,12 +11,13 @@ module Data.List.Relation.Unary.All.Properties where
 open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Data.Bool.Base using (Bool; T; true; false)
 open import Data.Bool.Properties using (T-∧)
-open import Data.Empty
+open import Data.Empty using (⊥-elim)
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List hiding (lookup; updateAt)
 open import Data.List.Properties as Listₚ using (partition-defn)
-open import Data.List.Membership.Propositional
+open import Data.List.Membership.Propositional using (_∈_; _≢∈_)
 open import Data.List.Membership.Propositional.Properties
+  using (there-injective-≢∈; ∈-filter⁻)
 import Data.List.Membership.Setoid as SetoidMembership
 open import Data.List.Relation.Unary.All as All using
   ( All; []; _∷_; lookup; updateAt
@@ -33,18 +34,18 @@ open import Data.Maybe.Relation.Unary.Any as Maybe using (just)
 open import Data.Nat.Base using (zero; suc; s≤s; _<_; z<s; s<s)
 open import Data.Nat.Properties using (≤-refl; m≤n⇒m≤1+n)
 open import Data.Product.Base as Product using (_×_; _,_; uncurry; uncurry′)
-open import Function.Base
-open import Function.Bundles
+open import Function.Base using (_∘_; _$_; id; case_of_; flip)
+open import Function.Bundles using (_↠_; mk↠ₛ; _⇔_; mk⇔; _↔_; mk↔ₛ′; Equivalence)
 open import Level using (Level)
 open import Relation.Binary.Core using (REL)
 open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.Definitions as B
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; refl; cong; cong₂; _≗_)
-open import Relation.Nullary
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Nullary.Decidable using (¬?; decidable-stable)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Nullary.Decidable
+  using (Dec; does; yes; no; _because_; ¬?; decidable-stable)
 open import Relation.Unary
   using (Decidable; Pred; Universal; ∁; _∩_; _⟨×⟩_) renaming (_⊆_ to _⋐_)
 open import Relation.Unary.Properties using (∁?)

src/Data/Product/Properties.agda

@@ -14,7 +14,8 @@ open import Function.Base using (_∋_; _∘_; id)
 open import Function.Bundles using (_↔_; mk↔ₛ′)
 open import Level using (Level)
 open import Relation.Binary.Definitions using (DecidableEquality)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core
+  using (_≡_; refl; _≗_; subst; cong; cong₂; cong′)
 open import Relation.Nullary.Decidable as Dec using (Dec; yes; no)
 
 private

src/Relation/Binary/PropositionalEquality.agda

@@ -37,14 +37,9 @@ open import Relation.Binary.PropositionalEquality.Algebra public
 ------------------------------------------------------------------------
 -- Pointwise equality
 
-infix 4 _≗_
-
 _→-setoid_ : ∀ (A : Set a) (B : Set b) → Setoid _ _
 A →-setoid B = ≡-setoid A (Trivial.indexedSetoid (setoid B))
 
-_≗_ : (f g : A → B) → Set _
-_≗_ {A = A} {B = B} = Setoid._≈_ (A →-setoid B)
-
 :→-to-Π : ∀ {A : Set a} {B : IndexedSetoid A b ℓ} →
           ((x : A) → IndexedSetoid.Carrier B x) →
           Dependent.Func (setoid A) B

src/Relation/Binary/PropositionalEquality/Core.agda

@@ -32,6 +32,15 @@ infix 4 _≢_
 _≢_ : {A : Set a} → Rel A a
 x ≢ y = ¬ x ≡ y
 
+------------------------------------------------------------------------
+-- Pointwise equality
+
+infix 4 _≗_
+
+_≗_ : (f g : A → B) → Set _
+_≗_ {A = A} {B = B} f g = ∀ x → f x ≡ g x
+
+
 ------------------------------------------------------------------------
 -- A variant of `refl` where the argument is explicit