From e79c19006dabf6fbd55561b0fe8b5ed4237bfedd Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Thu, 28 Mar 2024 21:18:23 -0400
Subject: [PATCH 1/4] tighten imports in some files, and make imports explicit
 in others. Driven by staring at a partial dependency graph.

---
 src/Algebra/Definitions/RawMagma.agda              | 4 ++--
 src/Data/Maybe/Base.agda                           | 6 +++---
 src/Data/Product/Properties.agda                   | 5 +++--
 src/Function/Indexed/Relation/Binary/Equality.agda | 2 +-
 4 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/Algebra/Definitions/RawMagma.agda b/src/Algebra/Definitions/RawMagma.agda
index f235f5d622..f186e7fc2d 100644
--- a/src/Algebra/Definitions/RawMagma.agda
+++ b/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
diff --git a/src/Data/Maybe/Base.agda b/src/Data/Maybe/Base.agda
index b0ae001f46..14cff5e9ba 100644
--- a/src/Data/Maybe/Base.agda
+++ b/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
diff --git a/src/Data/Product/Properties.agda b/src/Data/Product/Properties.agda
index 5e8509b76e..83742444f7 100644
--- a/src/Data/Product/Properties.agda
+++ b/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
diff --git a/src/Function/Indexed/Relation/Binary/Equality.agda b/src/Function/Indexed/Relation/Binary/Equality.agda
index ef9d6b3657..6f0bd7db8f 100644
--- a/src/Function/Indexed/Relation/Binary/Equality.agda
+++ b/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

From 2bba1e563349247ae017cf74b04fffdba1d5d905 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Thu, 28 Mar 2024 21:34:20 -0400
Subject: [PATCH 2/4] more tightening of imports

---
 src/Algebra/Definitions/RawMagma.agda     | 2 +-
 src/Relation/Binary/Reasoning/Syntax.agda | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Algebra/Definitions/RawMagma.agda b/src/Algebra/Definitions/RawMagma.agda
index f186e7fc2d..2e1bc657c7 100644
--- a/src/Algebra/Definitions/RawMagma.agda
+++ b/src/Algebra/Definitions/RawMagma.agda
@@ -14,7 +14,7 @@ open import Algebra.Bundles.Raw using (RawMagma)
 open import Data.Product.Base using (_×_; ∃)
 open import Level using (_⊔_)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Nullary.Negation using (¬_)
+open import Relation.Nullary.Negation.Core using (¬_)
 
 module Algebra.Definitions.RawMagma
   {a ℓ} (M : RawMagma a ℓ)
diff --git a/src/Relation/Binary/Reasoning/Syntax.agda b/src/Relation/Binary/Reasoning/Syntax.agda
index 809d238b39..3860f97b35 100644
--- a/src/Relation/Binary/Reasoning/Syntax.agda
+++ b/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 (_≡_)
 

From c8cbf7f1eb3d5e9c0ea561113fbea6629c4e70a1 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Thu, 28 Mar 2024 21:59:41 -0400
Subject: [PATCH 3/4] and even more tightening of imports

---
 src/Data/List/Relation/Unary/AllPairs.agda             |  2 +-
 src/Relation/Binary/Bundles.agda                       |  9 ++++-----
 src/Relation/Binary/PropositionalEquality/Algebra.agda | 10 ++++++----
 3 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/src/Data/List/Relation/Unary/AllPairs.agda b/src/Data/List/Relation/Unary/AllPairs.agda
index bed4a5972d..6036586822 100644
--- a/src/Data/List/Relation/Unary/AllPairs.agda
+++ b/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)
 
diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda
index 641803f8ef..5d29cabe57 100644
--- a/src/Relation/Binary/Bundles.agda
+++ b/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
diff --git a/src/Relation/Binary/PropositionalEquality/Algebra.agda b/src/Relation/Binary/PropositionalEquality/Algebra.agda
index 22ac67b298..7e0118bbcb 100644
--- a/src/Relation/Binary/PropositionalEquality/Algebra.agda
+++ b/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

From 50e08733f2fc3b3f48989372b221c07c3b1e9230 Mon Sep 17 00:00:00 2001
From: Jacques Carette <carette@mcmaster.ca>
Date: Thu, 28 Mar 2024 22:11:54 -0400
Subject: [PATCH 4/4] some explicit  for precision

---
 src/Algebra/Structures.agda               | 2 +-
 src/Relation/Binary/Reasoning/Setoid.agda | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index bb28e89882..5b88230e00 100644
--- a/src/Algebra/Structures.agda
+++ b/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₂)
diff --git a/src/Relation/Binary/Reasoning/Setoid.agda b/src/Relation/Binary/Reasoning/Setoid.agda
index ba6be9f79e..d80b2546d7 100644
--- a/src/Relation/Binary/Reasoning/Setoid.agda
+++ b/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