import cleaning Module 1 (#2607)

Author: jmougeot

src/Algebra/Module/Definitions/Bi.agda

@@ -15,7 +15,7 @@ module Algebra.Module.Definitions.Bi
   {a a′ b ℓb} (A : Set a) (A′ : Set a′) {B : Set b} (_≈_ : Rel B ℓb)
   where
 
-  open import Algebra.Module.Core
+  open import Algebra.Module.Core using (Opₗ; Opᵣ)
 
   Associative : Opₗ A B → Opᵣ A′ B → Set _
   Associative _∙ₗ_ _∙ᵣ_ = ∀ x m y → ((x ∙ₗ m) ∙ᵣ y) ≈ (x ∙ₗ (m ∙ᵣ y))

src/Algebra/Module/Definitions/Bi/Simultaneous.agda

@@ -6,13 +6,13 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary
+open import Relation.Binary using (Rel)
 
 module Algebra.Module.Definitions.Bi.Simultaneous
   {a b ℓb} (A : Set a) {B : Set b} (_≈_ : Rel B ℓb)
   where
 
-open import Algebra.Module.Core
+open import Algebra.Module.Core using (Opₗ; Opᵣ)
 
 Coincident : Opₗ A B → Opᵣ A B → Set _
 Coincident _∙ₗ_ _∙ᵣ_ = ∀ x m → (x ∙ₗ m) ≈ (m ∙ᵣ x)

src/Algebra/Module/Definitions/Left.agda

@@ -19,8 +19,8 @@ module Algebra.Module.Definitions.Left
 ------------------------------------------------------------------------
 -- Binary operations
 
-open import Algebra.Core
-open import Algebra.Module.Core
+open import Algebra.Core using (Op₂)
+open import Algebra.Module.Core using (Opₗ)
 
 ------------------------------------------------------------------------
 -- Properties of operations

src/Algebra/Module/Definitions/Right.agda

@@ -19,8 +19,8 @@ module Algebra.Module.Definitions.Right
 ------------------------------------------------------------------------
 -- Binary operations
 
-open import Algebra.Core
-open import Algebra.Module.Core
+open import Algebra.Core using (Op₂)
+open import Algebra.Module.Core using (Opᵣ)
 
 ------------------------------------------------------------------------
 -- Properties of operations

src/Algebra/Module/Morphism/Construct/Composition.agda

@@ -9,10 +9,12 @@
 module Algebra.Module.Morphism.Construct.Composition where
 
 open import Algebra.Module.Bundles.Raw
+  using (RawLeftSemimodule; RawLeftModule; RawRightSemimodule; RawRightModule;
+  RawBisemimodule; RawBimodule; RawSemimodule; RawModule)
 open import Algebra.Module.Morphism.Structures
-open import Algebra.Morphism.Construct.Composition
+open import Algebra.Morphism.Construct.Composition using (isMonoidHomomorphism; isGroupHomomorphism)
 open import Function.Base using (_∘_)
-import Function.Construct.Composition as Func
+import Function.Construct.Composition as Func using (surjective)
 open import Level using (Level)
 open import Relation.Binary.Definitions using (Transitive)
 

src/Algebra/Module/Morphism/Construct/Identity.agda

@@ -19,7 +19,7 @@ open import Algebra.Module.Morphism.Structures
         ; module SemimoduleMorphisms
         ; module ModuleMorphisms
         )
-open import Algebra.Morphism.Construct.Identity
+open import Algebra.Morphism.Construct.Identity using ( isMonoidHomomorphism; isGroupHomomorphism)
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id)
 import Function.Construct.Identity as Id