Skip to content

Commit 2bce915

Browse files
jmougeotjmougeot
authored
[imports] Algebra.Module.Morphism.* (#2608)
* Import cleaning Module 2 * Import cleaning Module 2 * Import cleaning
1 parent 4c095ab commit 2bce915

11 files changed

+72
-73
lines changed

‎src/Algebra/Module/Morphism/BimoduleMonomorphism.agda

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@
66

77
{-# OPTIONS --safe --cubical-compatible #-}
88

9-
open import Algebra.Module.Bundles.Raw
10-
open import Algebra.Module.Morphism.Structures
9+
open import Algebra.Module.Bundles.Raw using (RawBimodule)
10+
open import Algebra.Module.Morphism.Structures using (IsBimoduleMonomorphism)
1111

1212
module Algebra.Module.Morphism.BimoduleMonomorphism
1313
{r s a b ℓ₁ ℓ₂} {R : Set r} {S : Set s} {M : RawBimodule R S a ℓ₁} {N : RawBimodule R S b ℓ₂} {⟦_⟧}
@@ -19,11 +19,10 @@ private
1919
module M = RawBimodule M
2020
module N = RawBimodule N
2121

22-
open import Algebra.Bundles
23-
open import Algebra.Core
24-
open import Algebra.Module.Structures
25-
open import Algebra.Structures
26-
open import Relation.Binary.Core
22+
open import Algebra.Bundles using (Ring)
23+
open import Algebra.Module.Structures using (IsBimodule)
24+
open import Algebra.Structures using (IsRing)
25+
open import Relation.Binary.Core using (Rel)
2726

2827
------------------------------------------------------------------------
2928
-- Re-exports

‎src/Algebra/Module/Morphism/BisemimoduleMonomorphism.agda

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@
66

77
{-# OPTIONS --safe --cubical-compatible #-}
88

9-
open import Algebra.Module.Bundles.Raw
10-
open import Algebra.Module.Morphism.Structures
9+
open import Algebra.Module.Bundles.Raw using (RawBisemimodule)
10+
open import Algebra.Module.Morphism.Structures using (IsBisemimoduleMonomorphism)
1111

1212
module Algebra.Module.Morphism.BisemimoduleMonomorphism
1313
{r s a b ℓ₁ ℓ₂} {R : Set r} {S : Set s} {M : RawBisemimodule R S a ℓ₁} {N : RawBisemimodule R S b ℓ₂} {⟦_⟧}
@@ -19,15 +19,15 @@ private
1919
module M = RawBisemimodule M
2020
module N = RawBisemimodule N
2121

22-
open import Algebra.Bundles
23-
open import Algebra.Core
24-
import Algebra.Module.Definitions.Bi as BiDefs
25-
import Algebra.Module.Definitions.Left as LeftDefs
26-
import Algebra.Module.Definitions.Right as RightDefs
27-
open import Algebra.Module.Structures
28-
open import Algebra.Structures
29-
open import Function.Base
30-
open import Relation.Binary.Core
22+
open import Algebra.Bundles using (Semiring)
23+
open import Algebra.Core using (Op₂)
24+
import Algebra.Module.Definitions.Bi as BiDefs using (Associative)
25+
import Algebra.Module.Definitions.Left as LeftDefs using (LeftCongruent)
26+
import Algebra.Module.Definitions.Right as RightDefs using (RightCongruent)
27+
open import Algebra.Module.Structures using (IsBisemimodule)
28+
open import Algebra.Structures using (IsMagma; IsSemiring)
29+
open import Function.Base using (flip; _$_)
30+
open import Relation.Binary.Core using (Rel)
3131
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
3232

3333
------------------------------------------------------------------------

‎src/Algebra/Module/Morphism/Definitions.agda

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
------------------------------------------------------------------------
77
{-# OPTIONS --cubical-compatible --safe #-}
88

9-
open import Relation.Binary.Core
9+
open import Relation.Binary.Core using (Rel)
1010

1111
module Algebra.Module.Morphism.Definitions
1212
{r} (R : Set r) -- The underlying ring
@@ -15,7 +15,7 @@ module Algebra.Module.Morphism.Definitions
1515
{ℓ} (_≈_ : Rel B ℓ) -- The equality relation over the codomain
1616
where
1717

18-
open import Algebra.Module.Core
18+
open import Algebra.Module.Core using (Opₗ; Opᵣ)
1919
open import Algebra.Morphism.Definitions A B _≈_ public
2020

2121
Homomorphicₗ : (A → B) → Opₗ R A → Opₗ R B → Set _

‎src/Algebra/Module/Morphism/LeftModuleMonomorphism.agda

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@
66

77
{-# OPTIONS --cubical-compatible --safe #-}
88

9-
open import Algebra.Module.Bundles.Raw
10-
open import Algebra.Module.Morphism.Structures
9+
open import Algebra.Module.Bundles.Raw using (RawLeftModule)
10+
open import Algebra.Module.Morphism.Structures using (IsLeftModuleMonomorphism)
1111

1212
module Algebra.Module.Morphism.LeftModuleMonomorphism
1313
{r a b ℓ₁ ℓ₂} {R : Set r} {M : RawLeftModule R a ℓ₁} {N : RawLeftModule R b ℓ₂} {⟦_⟧}
@@ -19,11 +19,11 @@ private
1919
module M = RawLeftModule M
2020
module N = RawLeftModule N
2121

22-
open import Algebra.Bundles
23-
open import Algebra.Core
24-
open import Algebra.Module.Structures
25-
open import Algebra.Structures
26-
open import Relation.Binary.Core
22+
open import Algebra.Bundles using (Ring)
23+
open import Algebra.Core using (Op₂)
24+
open import Algebra.Module.Structures using (IsLeftModule)
25+
open import Algebra.Structures using (IsRing)
26+
open import Relation.Binary.Core using (Rel)
2727

2828
------------------------------------------------------------------------
2929
-- Re-exports

‎src/Algebra/Module/Morphism/LeftSemimoduleMonomorphism.agda

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@
66

77
{-# OPTIONS --cubical-compatible --safe #-}
88

9-
open import Algebra.Module.Bundles.Raw
10-
open import Algebra.Module.Morphism.Structures
9+
open import Algebra.Module.Bundles.Raw using (RawLeftSemimodule)
10+
open import Algebra.Module.Morphism.Structures using (IsLeftSemimoduleMonomorphism)
1111

1212
module Algebra.Module.Morphism.LeftSemimoduleMonomorphism
1313
{r a b ℓ₁ ℓ₂} {R : Set r} {M₁ : RawLeftSemimodule R a ℓ₁} {M₂ : RawLeftSemimodule R b ℓ₂} {⟦_⟧}
@@ -19,14 +19,14 @@ private
1919
module M = RawLeftSemimodule M₁
2020
module N = RawLeftSemimodule M₂
2121

22-
open import Algebra.Bundles
23-
open import Algebra.Core
22+
open import Algebra.Bundles using (Semiring)
23+
open import Algebra.Core using (Op₂)
2424
import Algebra.Module.Definitions.Left as LeftDefs
25-
open import Algebra.Module.Structures
26-
open import Algebra.Structures
27-
open import Function.Base
28-
open import Level
29-
open import Relation.Binary.Core
25+
open import Algebra.Module.Structures using (IsLeftSemimodule)
26+
open import Algebra.Structures using (IsSemiring; IsMagma)
27+
open import Function.Base using (flip; _$_)
28+
open import Level using (Level)
29+
open import Relation.Binary.Core using (Rel)
3030
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
3131

3232
private

‎src/Algebra/Module/Morphism/ModuleHomomorphism.agda

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,9 @@
99
import Algebra.Module.Properties as ModuleProperties
1010
import Algebra.Module.Morphism.Structures as MorphismStructures
1111

12-
open import Algebra using (CommutativeRing)
13-
open import Algebra.Module using (Module)
14-
open import Level using (Level)
12+
open import Algebra using (CommutativeRing)
13+
open import Algebra.Module using (Module)
14+
open import Level using (Level)
1515

1616
module Algebra.Module.Morphism.ModuleHomomorphism
1717
{r ℓr m ℓm : Level}
@@ -24,7 +24,7 @@ module Algebra.Module.Morphism.ModuleHomomorphism
2424
(isModuleHomomorphism : IsModuleHomomorphism f)
2525
where
2626

27-
open import Axiom.DoubleNegationElimination
27+
open import Axiom.DoubleNegationElimination using (DoubleNegationElimination)
2828
open import Data.Product.Base using (∃₂; _×_; _,_)
2929
open import Relation.Binary.Reasoning.MultiSetoid
3030
open import Relation.Nullary using (¬_)

‎src/Algebra/Module/Morphism/ModuleMonomorphism.agda

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@
66

77
{-# OPTIONS --safe --cubical-compatible #-}
88

9-
open import Algebra.Module.Bundles.Raw
10-
open import Algebra.Module.Morphism.Structures
9+
open import Algebra.Module.Bundles.Raw using (RawModule)
10+
open import Algebra.Module.Morphism.Structures using (IsModuleMonomorphism)
1111

1212
module Algebra.Module.Morphism.ModuleMonomorphism
1313
{r a b ℓ₁ ℓ₂} {R : Set r} {M : RawModule R a ℓ₁} {N : RawModule R b ℓ₂} {⟦_⟧}
@@ -19,11 +19,11 @@ private
1919
module M = RawModule M
2020
module N = RawModule N
2121

22-
open import Algebra.Bundles
23-
open import Algebra.Core
24-
open import Algebra.Module.Structures
25-
open import Algebra.Structures
26-
open import Relation.Binary.Core
22+
open import Algebra.Bundles using (CommutativeRing)
23+
open import Algebra.Core using (Op₂)
24+
open import Algebra.Module.Structures using (IsModule)
25+
open import Algebra.Structures using (IsCommutativeRing)
26+
open import Relation.Binary.Core using (Rel)
2727

2828
------------------------------------------------------------------------
2929
-- Re-exports

‎src/Algebra/Module/Morphism/RightModuleMonomorphism.agda

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@
66

77
{-# OPTIONS --cubical-compatible --safe #-}
88

9-
open import Algebra.Module.Bundles.Raw
10-
open import Algebra.Module.Morphism.Structures
9+
open import Algebra.Module.Bundles.Raw using (RawRightModule)
10+
open import Algebra.Module.Morphism.Structures using (IsRightModuleMonomorphism)
1111

1212
module Algebra.Module.Morphism.RightModuleMonomorphism
1313
{r a b ℓ₁ ℓ₂} {R : Set r} {M : RawRightModule R a ℓ₁} {N : RawRightModule R b ℓ₂} {⟦_⟧}
@@ -18,11 +18,11 @@ open IsRightModuleMonomorphism isRightModuleMonomorphism
1818
module M = RawRightModule M
1919
module N = RawRightModule N
2020

21-
open import Algebra.Bundles
22-
open import Algebra.Core
23-
open import Algebra.Module.Structures
24-
open import Algebra.Structures
25-
open import Relation.Binary.Core
21+
open import Algebra.Bundles using (Ring)
22+
open import Algebra.Core using (Op₂)
23+
open import Algebra.Module.Structures using (IsRightModule)
24+
open import Algebra.Structures using (IsRing)
25+
open import Relation.Binary.Core using (Rel)
2626

2727
------------------------------------------------------------------------
2828
-- Re-exports

‎src/Algebra/Module/Morphism/RightSemimoduleMonomorphism.agda

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@
66

77
{-# OPTIONS --cubical-compatible --safe #-}
88

9-
open import Algebra.Module.Bundles.Raw
10-
open import Algebra.Module.Morphism.Structures
9+
open import Algebra.Module.Bundles.Raw using (RawRightSemimodule)
10+
open import Algebra.Module.Morphism.Structures using (IsRightSemimoduleMonomorphism)
1111

1212
module Algebra.Module.Morphism.RightSemimoduleMonomorphism
1313
{r a b ℓ₁ ℓ₂} {R : Set r} {M : RawRightSemimodule R a ℓ₁} {N : RawRightSemimodule R b ℓ₂} {⟦_⟧}
@@ -19,14 +19,14 @@ private
1919
module M = RawRightSemimodule M
2020
module N = RawRightSemimodule N
2121

22-
open import Algebra.Bundles
23-
open import Algebra.Core
22+
open import Algebra.Bundles using (Semiring)
23+
open import Algebra.Core using (Op₂)
2424
import Algebra.Module.Definitions.Right as RightDefs
25-
open import Algebra.Module.Structures
26-
open import Algebra.Structures
27-
open import Function.Base
28-
open import Level
29-
open import Relation.Binary.Core
25+
open import Algebra.Module.Structures using (IsRightSemimodule)
26+
open import Algebra.Structures using (IsMagma; IsSemiring)
27+
open import Function.Base using (flip; _$_)
28+
open import Level using (Level)
29+
open import Relation.Binary.Core using (Rel)
3030
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
3131

3232
private

‎src/Algebra/Module/Morphism/SemimoduleMonomorphism.agda

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,8 @@
66

77
{-# OPTIONS --safe --cubical-compatible #-}
88

9-
open import Algebra.Module.Bundles.Raw
10-
open import Algebra.Module.Morphism.Structures
9+
open import Algebra.Module.Bundles.Raw using (RawSemimodule)
10+
open import Algebra.Module.Morphism.Structures using (IsSemimoduleMonomorphism)
1111

1212
module Algebra.Module.Morphism.SemimoduleMonomorphism
1313
{r a b ℓ₁ ℓ₂} {R : Set r} {M : RawSemimodule R a ℓ₁} {N : RawSemimodule R b ℓ₂} {⟦_⟧}
@@ -19,13 +19,13 @@ private
1919
module M = RawSemimodule M
2020
module N = RawSemimodule N
2121

22-
open import Algebra.Bundles
23-
open import Algebra.Core
22+
open import Algebra.Bundles using (CommutativeSemiring)
23+
open import Algebra.Core using (Op₂)
2424
import Algebra.Module.Definitions.Bi.Simultaneous as SimulDefs
25-
open import Algebra.Module.Structures
26-
open import Algebra.Structures
27-
open import Function.Base
28-
open import Relation.Binary.Core
25+
open import Algebra.Module.Structures using (IsSemimodule)
26+
open import Algebra.Structures using (IsCommutativeSemiring; IsMagma)
27+
open import Function.Base using (flip; _$_)
28+
open import Relation.Binary.Core using (Rel)
2929
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
3030

3131
------------------------------------------------------------------------

0 commit comments

Comments
 (0)