diff --git a/src/Algebra/Module/Bundles.agda b/src/Algebra/Module/Bundles.agda index 5df96258d6..69d55e2630 100644 --- a/src/Algebra/Module/Bundles.agda +++ b/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 diff --git a/src/Algebra/Module/Structures.agda b/src/Algebra/Module/Structures.agda index 64873252bd..ce641ee28a 100644 --- a/src/Algebra/Module/Structures.agda +++ b/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; _⊔_) diff --git a/src/Algebra/Module/Structures/Biased.agda b/src/Algebra/Module/Structures/Biased.agda index 40b550d9c0..9459874f0f 100644 --- a/src/Algebra/Module/Structures/Biased.agda +++ b/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; _⊔_)