[imports] Algebra.Lattice.Bundles .. Algebra.Module.Construct.* (#2606)

* Cleaning import Lattice 5

* line

* fix

* Update src/Algebra/Module/Construct/DirectProduct.agda

Dependency order

---------

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

Author: jmougeot

src/Algebra/Lattice/Bundles.agda

@@ -15,11 +15,14 @@
 
 module Algebra.Lattice.Bundles where
 
-open import Algebra.Core
-open import Algebra.Bundles
-open import Algebra.Structures
+open import Algebra.Core using (Op₁; Op₂)
+open import Algebra.Bundles using (Band)
 import Algebra.Lattice.Bundles.Raw as Raw
 open import Algebra.Lattice.Structures
+  using ( IsSemilattice; IsMeetSemilattice; IsJoinSemilattice
+        ; IsBoundedSemilattice; IsBoundedMeetSemilattice
+        ; IsBoundedJoinSemilattice; IsLattice; IsDistributiveLattice
+        ; IsBooleanAlgebra)
 open import Level using (suc; _⊔_)
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Core using (Rel)

src/Algebra/Lattice/Structures.agda

@@ -13,7 +13,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Core
+open import Algebra.Core using (Op₁; Op₂)
 open import Data.Product.Base using (proj₁; proj₂)
 open import Level using (_⊔_)
 open import Relation.Binary.Core using (Rel)

src/Algebra/Module/Bundles/Raw.agda

@@ -8,10 +8,10 @@
 
 module Algebra.Module.Bundles.Raw where
 
-open import Algebra.Bundles.Raw
-open import Algebra.Core
-open import Algebra.Module.Core
-open import Level
+open import Algebra.Bundles.Raw using (RawMonoid; RawGroup)
+open import Algebra.Core using (Op₁; Op₂)
+open import Algebra.Module.Core using (Opₗ; Opᵣ)
+open import Level using (Level; _⊔_; suc)
 open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Binary.Core using (Rel)
 

src/Algebra/Module/Construct/DirectProduct.agda

@@ -12,11 +12,12 @@
 module Algebra.Module.Construct.DirectProduct where
 
 open import Algebra.Bundles
-open import Algebra.Construct.DirectProduct
+open import Algebra.Construct.DirectProduct using (commutativeMonoid)
 open import Algebra.Module.Bundles
 open import Data.Product.Base using (map; zip; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
-open import Level
+  using (Pointwise)
+open import Level using (Level; _⊔_)
 
 private
   variable

src/Algebra/Module/Construct/Idealization.agda

@@ -37,11 +37,13 @@ open import Algebra.Module.Bundles using (Bimodule)
 module Algebra.Module.Construct.Idealization
   {r ℓr m ℓm} (ring : Ring r ℓr) (bimodule : Bimodule ring ring m ℓm) where
 
-open import Algebra.Core
-import Algebra.Consequences.Setoid as Consequences
+open import Algebra.Core using (Op₂)
+import Algebra.Consequences.Setoid as Consequences using (comm∧assoc⇒middleFour)
 import Algebra.Definitions as Definitions
-import Algebra.Module.Construct.DirectProduct as DirectProduct
-import Algebra.Module.Construct.TensorUnit as TensorUnit
+  using (Congruent₂; _DistributesOverˡ_; _DistributesOverʳ_; _DistributesOver_
+        ; LeftIdentity; RightIdentity; Identity; Associative)
+import Algebra.Module.Construct.DirectProduct as DirectProduct using (bimodule)
+import Algebra.Module.Construct.TensorUnit as TensorUnit using (bimodule)
 open import Algebra.Structures using (IsAbelianGroup; IsRing)
 open import Data.Product.Base using (_,_; ∃-syntax)
 open import Level using (Level; _⊔_)

src/Algebra/Module/Construct/TensorUnit.agda

@@ -12,8 +12,14 @@
 module Algebra.Module.Construct.TensorUnit where
 
 open import Algebra.Bundles
+  using (RawSemiring; RawRing; Semiring; Ring; CommutativeSemiring
+        ; CommutativeRing)
 open import Algebra.Module.Bundles
-open import Level
+  using (RawSemimodule; RawLeftSemimodule; RawRightSemimodule; RawBisemimodule
+        ; RawLeftModule; RawRightModule; RawBimodule; RawModule; LeftSemimodule
+        ; RightSemimodule; Bisemimodule; Semimodule; LeftModule; RightModule; Bimodule
+        ; Module)
+open import Level  using (Level; _⊔_)
 
 private
   variable

src/Algebra/Module/Construct/Zero.agda

@@ -10,13 +10,13 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Level
+open import Level using (Level)
 
 module Algebra.Module.Construct.Zero {c ℓ : Level} where
 
-open import Algebra.Bundles
+open import Algebra.Bundles using (RawSemiring; Semiring; Ring; CommutativeSemiring; CommutativeRing)
 open import Algebra.Module.Bundles
-open import Data.Unit.Polymorphic
+open import Data.Unit.Polymorphic using (⊤)
 open import Relation.Binary.Core using (Rel)
 
 private