tighten imports in some files, and make imports explicit in others. D…

…riven by staring at a partial dependency graph.

src/Algebra/Definitions/RawMagma.agda

@@ -10,10 +10,10 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Bundles using (RawMagma)
+open import Algebra.Bundles.Raw using (RawMagma)
 open import Data.Product.Base using (_×_; ∃)
 open import Level using (_⊔_)
-open import Relation.Binary.Core
+open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary.Negation using (¬_)
 
 module Algebra.Definitions.RawMagma

src/Data/Maybe/Base.agda

@@ -15,9 +15,9 @@ open import Data.Bool.Base using (Bool; true; false; not)
 open import Data.Unit.Base using (⊤)
 open import Data.These.Base using (These; this; that; these)
 open import Data.Product.Base as Prod using (_×_; _,_)
-open import Function.Base
-open import Relation.Nullary.Reflects
-open import Relation.Nullary.Decidable.Core
+open import Function.Base using (const; _∘_; id)
+open import Relation.Nullary.Reflects using (invert)
+open import Relation.Nullary.Decidable.Core using (Dec; _because_)
 
 private
   variable

src/Data/Product/Properties.agda

@@ -8,13 +8,14 @@
 
 module Data.Product.Properties where
 
-open import Axiom.UniquenessOfIdentityProofs
-open import Data.Product.Base
+open import Axiom.UniquenessOfIdentityProofs using (UIP; module Decidable⇒UIP)
+open import Data.Product.Base using (_,_; Σ; _×_; map; swap; ∃; ∃₂)
 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
+  using (_≡_; _≗_; subst; cong; cong₂; cong′; refl)
 open import Relation.Nullary.Decidable as Dec using (Dec; yes; no)
 
 private

src/Function/Indexed/Relation/Binary/Equality.agda

@@ -8,7 +8,7 @@
 
 module Function.Indexed.Relation.Binary.Equality where
 
-open import Relation.Binary using (Setoid)
+open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Indexed.Heterogeneous using (IndexedSetoid)
 
 -- A variant of setoid which uses the propositional equality setoid