Tighten imports (#2334)

* tighten imports in some files, and make imports explicit in others. Driven by staring at a partial dependency graph.

* more tightening of imports

* and even more tightening of imports

* some explicit  for precision

---------

Co-authored-by: G. Allais <[email protected]>

Author: 2 people

src/Algebra/Definitions/RawMagma.agda

@@ -10,11 +10,11 @@
 
 {-# 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.Nullary.Negation using (¬_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Nullary.Negation.Core using (¬_)
 
 module Algebra.Definitions.RawMagma
   {a ℓ} (M : RawMagma a ℓ)

src/Algebra/Structures.agda

@@ -21,7 +21,7 @@ module Algebra.Structures
 -- The file is divided into sections depending on the arities of the
 -- components of the algebraic structure.
 
-open import Algebra.Core
+open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Definitions _≈_
 import Algebra.Consequences.Setoid as Consequences
 open import Data.Product.Base using (_,_; proj₁; proj₂)

src/Data/List/Relation/Unary/AllPairs.agda

@@ -18,7 +18,7 @@ open import Function.Base using (id; _∘_)
 open import Level using (_⊔_)
 open import Relation.Binary.Definitions as B
 open import Relation.Binary.Construct.Intersection renaming (_∩_ to _∩ᵇ_)
-open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.PropositionalEquality.Core using (refl; cong₂)
 open import Relation.Unary as U renaming (_∩_ to _∩ᵘ_) hiding (_⇒_)
 open import Relation.Nullary.Decidable as Dec using (_×-dec_; yes; no)
 

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,8 +8,8 @@
 
 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)

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

src/Relation/Binary/Bundles.agda

@@ -11,11 +11,10 @@
 module Relation.Binary.Bundles where
 
 open import Function.Base using (flip)
-open import Level
-open import Relation.Nullary.Negation using (¬_)
-open import Relation.Binary.Core
-open import Relation.Binary.Definitions
-open import Relation.Binary.Structures
+open import Level using (Level; suc; _⊔_)
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Structures -- most of it
 
 ------------------------------------------------------------------------
 -- Setoids

src/Relation/Binary/PropositionalEquality/Algebra.agda

@@ -8,10 +8,12 @@
 
 module Relation.Binary.PropositionalEquality.Algebra where
 
-open import Algebra
-open import Level
-open import Relation.Binary.PropositionalEquality.Core
-open import Relation.Binary.PropositionalEquality.Properties
+open import Algebra.Bundles using (Magma)
+open import Algebra.Core using (Op₂)
+open import Algebra.Structures using (IsMagma)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong₂)
+open import Relation.Binary.PropositionalEquality.Properties using (isEquivalence)
 
 private
   variable

src/Relation/Binary/Reasoning/Setoid.agda

@@ -21,7 +21,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Reasoning.Syntax
+open import Relation.Binary.Reasoning.Syntax using (module ≈-syntax)
 
 module Relation.Binary.Reasoning.Setoid {s₁ s₂} (S : Setoid s₁ s₂) where
 

src/Relation/Binary/Reasoning/Syntax.agda

@@ -9,9 +9,10 @@
 open import Level using (Level; _⊔_; suc)
 open import Relation.Nullary.Decidable.Core
   using (Dec; True; toWitness)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Negation.Core using (contradiction)
 open import Relation.Binary.Core using (Rel; REL; _⇒_)
 open import Relation.Binary.Definitions
+  using (_Respectsʳ_; Asymmetric; Trans; Sym; Reflexive)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_)