Import cleaning Module 3 (#2609)

* Import cleaning Module 3

* Import cleaning Module

Author: jmougeot

src/Algebra/Module/Bundles.agda

@@ -26,15 +26,18 @@
 module Algebra.Module.Bundles where
 
 open import Algebra.Bundles
-open import Algebra.Core
+  using (Semiring; Ring; CommutativeSemiring; CommutativeRing;
+  CommutativeMonoid; AbelianGroup)
+open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Definitions using (Involutive)
 import Algebra.Module.Bundles.Raw as Raw
-open import Algebra.Module.Core
+open import Algebra.Module.Core using (Opₗ; Opᵣ)
 open import Algebra.Module.Structures
+  using (IsLeftSemimodule; IsRightSemimodule; IsBisemimodule;
+  IsSemimodule; IsLeftModule; IsRightModule; IsModule; IsBimodule)
 open import Algebra.Module.Definitions
-open import Algebra.Properties.Group
-open import Function.Base
-open import Level
+open import Function.Base using (flip)
+open import Level using (Level; _⊔_; suc)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary    using (¬_)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning

src/Algebra/Module/Structures.agda

@@ -13,11 +13,14 @@ open import Relation.Binary.Structures using (IsEquivalence)
 module Algebra.Module.Structures where
 
 open import Algebra.Bundles
-open import Algebra.Core
-open import Algebra.Module.Core
+  using (Semiring; Ring; CommutativeSemiring; CommutativeRing)
+open import Algebra.Core using (Op₁; Op₂)
+open import Algebra.Module.Core  using (Opₗ; Opᵣ)
 import Algebra.Definitions as Defs
 open import Algebra.Module.Definitions
-open import Algebra.Structures
+  using (module LeftDefs; module RightDefs; module BiDefs;
+  module SimultaneousBiDefs)
+open import Algebra.Structures using (IsCommutativeMonoid; IsAbelianGroup)
 open import Data.Product.Base using (_,_; proj₁; proj₂)
 open import Level using (Level; _⊔_)
 

src/Algebra/Module/Structures/Biased.agda

@@ -14,10 +14,13 @@ open import Relation.Binary.Structures using (IsEquivalence)
 module Algebra.Module.Structures.Biased where
 
 open import Algebra.Bundles
-open import Algebra.Core
-open import Algebra.Module.Core
+  using (Semiring; Ring; CommutativeSemiring; CommutativeRing)
+open import Algebra.Core using (Op₁; Op₂)
+open import Algebra.Module.Core using (Opₗ; Opᵣ)
 open import Algebra.Module.Consequences
 open import Algebra.Module.Structures
+  using (IsLeftSemimodule; IsRightSemimodule; IsBisemimodule;
+  IsSemimodule; IsLeftModule; IsRightModule; IsModule)
 open import Function.Base using (flip)
 open import Level using (Level; _⊔_)