Skip to content

Commit b376a6e

Browse files
TanebTaneb
committed
Follow on changes that oughtn't be necessary
1 parent 201fc4a commit b376a6e

9 files changed

+32
-32
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ module Algebra.Module.Morphism.BimoduleMonomorphism
1414
(isBimoduleMonomorphism : IsBimoduleMonomorphism M N ⟦_⟧)
1515
where
1616

17-
open IsBimoduleMonomorphism isBimoduleMonomorphism
17+
open IsBimoduleMonomorphism M N isBimoduleMonomorphism
1818
private
1919
module M = RawBimodule M
2020
module N = RawBimodule N

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ module Algebra.Module.Morphism.BisemimoduleMonomorphism
1414
(isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism M N ⟦_⟧)
1515
where
1616

17-
open IsBisemimoduleMonomorphism isBisemimoduleMonomorphism
17+
open IsBisemimoduleMonomorphism M N isBisemimoduleMonomorphism
1818
private
1919
module M = RawBisemimodule M
2020
module N = RawBisemimodule N

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

Lines changed: 24 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -39,23 +39,23 @@ module _
3939
isLeftSemimoduleHomomorphism f-homo g-homo = record
4040
{ +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism ≈ᴹ₃-trans F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
4141
; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
42-
} where module F = IsLeftSemimoduleHomomorphism f-homo; module G = IsLeftSemimoduleHomomorphism g-homo
42+
} where module F = IsLeftSemimoduleHomomorphism M₁ M₂ f-homo; module G = IsLeftSemimoduleHomomorphism M₂ M₃ g-homo
4343

4444
isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism M₁ M₂ f →
4545
IsLeftSemimoduleMonomorphism M₂ M₃ g →
4646
IsLeftSemimoduleMonomorphism M₁ M₃ (g ∘ f)
4747
isLeftSemimoduleMonomorphism f-mono g-mono = record
4848
{ isLeftSemimoduleHomomorphism = isLeftSemimoduleHomomorphism F.isLeftSemimoduleHomomorphism G.isLeftSemimoduleHomomorphism
4949
; injective = F.injective ∘ G.injective
50-
} where module F = IsLeftSemimoduleMonomorphism f-mono; module G = IsLeftSemimoduleMonomorphism g-mono
50+
} where module F = IsLeftSemimoduleMonomorphism M₁ M₂ f-mono; module G = IsLeftSemimoduleMonomorphism M₂ M₃ g-mono
5151

5252
isLeftSemimoduleIsomorphism : IsLeftSemimoduleIsomorphism M₁ M₂ f →
5353
IsLeftSemimoduleIsomorphism M₂ M₃ g →
5454
IsLeftSemimoduleIsomorphism M₁ M₃ (g ∘ f)
5555
isLeftSemimoduleIsomorphism f-iso g-iso = record
5656
{ isLeftSemimoduleMonomorphism = isLeftSemimoduleMonomorphism F.isLeftSemimoduleMonomorphism G.isLeftSemimoduleMonomorphism
5757
; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
58-
} where module F = IsLeftSemimoduleIsomorphism f-iso; module G = IsLeftSemimoduleIsomorphism g-iso
58+
} where module F = IsLeftSemimoduleIsomorphism M₁ M₂ f-iso; module G = IsLeftSemimoduleIsomorphism M₂ M₃ g-iso
5959

6060
module _
6161
{R : Set r}
@@ -74,23 +74,23 @@ module _
7474
isLeftModuleHomomorphism f-homo g-homo = record
7575
{ +ᴹ-isGroupHomomorphism = isGroupHomomorphism ≈ᴹ₃-trans F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
7676
; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
77-
} where module F = IsLeftModuleHomomorphism f-homo; module G = IsLeftModuleHomomorphism g-homo
77+
} where module F = IsLeftModuleHomomorphism M₁ M₂ f-homo; module G = IsLeftModuleHomomorphism M₂ M₃ g-homo
7878

7979
isLeftModuleMonomorphism : IsLeftModuleMonomorphism M₁ M₂ f →
8080
IsLeftModuleMonomorphism M₂ M₃ g →
8181
IsLeftModuleMonomorphism M₁ M₃ (g ∘ f)
8282
isLeftModuleMonomorphism f-mono g-mono = record
8383
{ isLeftModuleHomomorphism = isLeftModuleHomomorphism F.isLeftModuleHomomorphism G.isLeftModuleHomomorphism
8484
; injective = F.injective ∘ G.injective
85-
} where module F = IsLeftModuleMonomorphism f-mono; module G = IsLeftModuleMonomorphism g-mono
85+
} where module F = IsLeftModuleMonomorphism M₁ M₂ f-mono; module G = IsLeftModuleMonomorphism M₂ M₃ g-mono
8686

8787
isLeftModuleIsomorphism : IsLeftModuleIsomorphism M₁ M₂ f →
8888
IsLeftModuleIsomorphism M₂ M₃ g →
8989
IsLeftModuleIsomorphism M₁ M₃ (g ∘ f)
9090
isLeftModuleIsomorphism f-iso g-iso = record
9191
{ isLeftModuleMonomorphism = isLeftModuleMonomorphism F.isLeftModuleMonomorphism G.isLeftModuleMonomorphism
9292
; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
93-
} where module F = IsLeftModuleIsomorphism f-iso; module G = IsLeftModuleIsomorphism g-iso
93+
} where module F = IsLeftModuleIsomorphism M₁ M₂ f-iso; module G = IsLeftModuleIsomorphism M₂ M₃ g-iso
9494

9595
module _
9696
{R : Set r}
@@ -109,23 +109,23 @@ module _
109109
isRightSemimoduleHomomorphism f-homo g-homo = record
110110
{ +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism ≈ᴹ₃-trans F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
111111
; *ᵣ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
112-
} where module F = IsRightSemimoduleHomomorphism f-homo; module G = IsRightSemimoduleHomomorphism g-homo
112+
} where module F = IsRightSemimoduleHomomorphism M₁ M₂ f-homo; module G = IsRightSemimoduleHomomorphism M₂ M₃ g-homo
113113

114114
isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism M₁ M₂ f →
115115
IsRightSemimoduleMonomorphism M₂ M₃ g →
116116
IsRightSemimoduleMonomorphism M₁ M₃ (g ∘ f)
117117
isRightSemimoduleMonomorphism f-mono g-mono = record
118118
{ isRightSemimoduleHomomorphism = isRightSemimoduleHomomorphism F.isRightSemimoduleHomomorphism G.isRightSemimoduleHomomorphism
119119
; injective = F.injective ∘ G.injective
120-
} where module F = IsRightSemimoduleMonomorphism f-mono; module G = IsRightSemimoduleMonomorphism g-mono
120+
} where module F = IsRightSemimoduleMonomorphism M₁ M₂ f-mono; module G = IsRightSemimoduleMonomorphism M₂ M₃ g-mono
121121

122122
isRightSemimoduleIsomorphism : IsRightSemimoduleIsomorphism M₁ M₂ f →
123123
IsRightSemimoduleIsomorphism M₂ M₃ g →
124124
IsRightSemimoduleIsomorphism M₁ M₃ (g ∘ f)
125125
isRightSemimoduleIsomorphism f-iso g-iso = record
126126
{ isRightSemimoduleMonomorphism = isRightSemimoduleMonomorphism F.isRightSemimoduleMonomorphism G.isRightSemimoduleMonomorphism
127127
; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
128-
} where module F = IsRightSemimoduleIsomorphism f-iso; module G = IsRightSemimoduleIsomorphism g-iso
128+
} where module F = IsRightSemimoduleIsomorphism M₁ M₂ f-iso; module G = IsRightSemimoduleIsomorphism M₂ M₃ g-iso
129129

130130
module _
131131
{R : Set r}
@@ -144,23 +144,23 @@ module _
144144
isRightModuleHomomorphism f-homo g-homo = record
145145
{ +ᴹ-isGroupHomomorphism = isGroupHomomorphism ≈ᴹ₃-trans F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
146146
; *ᵣ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
147-
} where module F = IsRightModuleHomomorphism f-homo; module G = IsRightModuleHomomorphism g-homo
147+
} where module F = IsRightModuleHomomorphism M₁ M₂ f-homo; module G = IsRightModuleHomomorphism M₂ M₃ g-homo
148148

149149
isRightModuleMonomorphism : IsRightModuleMonomorphism M₁ M₂ f →
150150
IsRightModuleMonomorphism M₂ M₃ g →
151151
IsRightModuleMonomorphism M₁ M₃ (g ∘ f)
152152
isRightModuleMonomorphism f-mono g-mono = record
153153
{ isRightModuleHomomorphism = isRightModuleHomomorphism F.isRightModuleHomomorphism G.isRightModuleHomomorphism
154154
; injective = F.injective ∘ G.injective
155-
} where module F = IsRightModuleMonomorphism f-mono; module G = IsRightModuleMonomorphism g-mono
155+
} where module F = IsRightModuleMonomorphism M₁ M₂ f-mono; module G = IsRightModuleMonomorphism M₂ M₃ g-mono
156156

157157
isRightModuleIsomorphism : IsRightModuleIsomorphism M₁ M₂ f →
158158
IsRightModuleIsomorphism M₂ M₃ g →
159159
IsRightModuleIsomorphism M₁ M₃ (g ∘ f)
160160
isRightModuleIsomorphism f-iso g-iso = record
161161
{ isRightModuleMonomorphism = isRightModuleMonomorphism F.isRightModuleMonomorphism G.isRightModuleMonomorphism
162162
; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
163-
} where module F = IsRightModuleIsomorphism f-iso; module G = IsRightModuleIsomorphism g-iso
163+
} where module F = IsRightModuleIsomorphism M₁ M₂ f-iso; module G = IsRightModuleIsomorphism M₂ M₃ g-iso
164164

165165
module _
166166
{R : Set r}
@@ -181,23 +181,23 @@ module _
181181
{ +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism ≈ᴹ₃-trans F.+ᴹ-isMonoidHomomorphism G.+ᴹ-isMonoidHomomorphism
182182
; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
183183
; *ᵣ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
184-
} where module F = IsBisemimoduleHomomorphism f-homo; module G = IsBisemimoduleHomomorphism g-homo
184+
} where module F = IsBisemimoduleHomomorphism M₁ M₂ f-homo; module G = IsBisemimoduleHomomorphism M₂ M₃ g-homo
185185

186186
isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism M₁ M₂ f →
187187
IsBisemimoduleMonomorphism M₂ M₃ g →
188188
IsBisemimoduleMonomorphism M₁ M₃ (g ∘ f)
189189
isBisemimoduleMonomorphism f-mono g-mono = record
190190
{ isBisemimoduleHomomorphism = isBisemimoduleHomomorphism F.isBisemimoduleHomomorphism G.isBisemimoduleHomomorphism
191191
; injective = F.injective ∘ G.injective
192-
} where module F = IsBisemimoduleMonomorphism f-mono; module G = IsBisemimoduleMonomorphism g-mono
192+
} where module F = IsBisemimoduleMonomorphism M₁ M₂ f-mono; module G = IsBisemimoduleMonomorphism M₂ M₃ g-mono
193193

194194
isBisemimoduleIsomorphism : IsBisemimoduleIsomorphism M₁ M₂ f →
195195
IsBisemimoduleIsomorphism M₂ M₃ g →
196196
IsBisemimoduleIsomorphism M₁ M₃ (g ∘ f)
197197
isBisemimoduleIsomorphism f-iso g-iso = record
198198
{ isBisemimoduleMonomorphism = isBisemimoduleMonomorphism F.isBisemimoduleMonomorphism G.isBisemimoduleMonomorphism
199199
; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
200-
} where module F = IsBisemimoduleIsomorphism f-iso; module G = IsBisemimoduleIsomorphism g-iso
200+
} where module F = IsBisemimoduleIsomorphism M₁ M₂ f-iso; module G = IsBisemimoduleIsomorphism M₂ M₃ g-iso
201201

202202
module _
203203
{R : Set r}
@@ -218,23 +218,23 @@ module _
218218
{ +ᴹ-isGroupHomomorphism = isGroupHomomorphism ≈ᴹ₃-trans F.+ᴹ-isGroupHomomorphism G.+ᴹ-isGroupHomomorphism
219219
; *ₗ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ₗ-homo r x)) (G.*ₗ-homo r (f x))
220220
; *ᵣ-homo = λ r x → ≈ᴹ₃-trans (G.⟦⟧-cong (F.*ᵣ-homo r x)) (G.*ᵣ-homo r (f x))
221-
} where module F = IsBimoduleHomomorphism f-homo; module G = IsBimoduleHomomorphism g-homo
221+
} where module F = IsBimoduleHomomorphism M₁ M₂ f-homo; module G = IsBimoduleHomomorphism M₂ M₃ g-homo
222222

223223
isBimoduleMonomorphism : IsBimoduleMonomorphism M₁ M₂ f →
224224
IsBimoduleMonomorphism M₂ M₃ g →
225225
IsBimoduleMonomorphism M₁ M₃ (g ∘ f)
226226
isBimoduleMonomorphism f-mono g-mono = record
227227
{ isBimoduleHomomorphism = isBimoduleHomomorphism F.isBimoduleHomomorphism G.isBimoduleHomomorphism
228228
; injective = F.injective ∘ G.injective
229-
} where module F = IsBimoduleMonomorphism f-mono; module G = IsBimoduleMonomorphism g-mono
229+
} where module F = IsBimoduleMonomorphism M₁ M₂ f-mono; module G = IsBimoduleMonomorphism M₂ M₃ g-mono
230230

231231
isBimoduleIsomorphism : IsBimoduleIsomorphism M₁ M₂ f →
232232
IsBimoduleIsomorphism M₂ M₃ g →
233233
IsBimoduleIsomorphism M₁ M₃ (g ∘ f)
234234
isBimoduleIsomorphism f-iso g-iso = record
235235
{ isBimoduleMonomorphism = isBimoduleMonomorphism F.isBimoduleMonomorphism G.isBimoduleMonomorphism
236236
; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
237-
} where module F = IsBimoduleIsomorphism f-iso; module G = IsBimoduleIsomorphism g-iso
237+
} where module F = IsBimoduleIsomorphism M₁ M₂ f-iso; module G = IsBimoduleIsomorphism M₂ M₃ g-iso
238238

239239
module _
240240
{R : Set r}
@@ -252,23 +252,23 @@ module _
252252
IsSemimoduleHomomorphism M₁ M₃ (g ∘ f)
253253
isSemimoduleHomomorphism f-homo g-homo = record
254254
{ isBisemimoduleHomomorphism = isBisemimoduleHomomorphism ≈ᴹ₃-trans F.isBisemimoduleHomomorphism G.isBisemimoduleHomomorphism
255-
} where module F = IsSemimoduleHomomorphism f-homo; module G = IsSemimoduleHomomorphism g-homo
255+
} where module F = IsSemimoduleHomomorphism M₁ M₂ f-homo; module G = IsSemimoduleHomomorphism M₂ M₃ g-homo
256256

257257
isSemimoduleMonomorphism : IsSemimoduleMonomorphism M₁ M₂ f →
258258
IsSemimoduleMonomorphism M₂ M₃ g →
259259
IsSemimoduleMonomorphism M₁ M₃ (g ∘ f)
260260
isSemimoduleMonomorphism f-mono g-mono = record
261261
{ isSemimoduleHomomorphism = isSemimoduleHomomorphism F.isSemimoduleHomomorphism G.isSemimoduleHomomorphism
262262
; injective = F.injective ∘ G.injective
263-
} where module F = IsSemimoduleMonomorphism f-mono; module G = IsSemimoduleMonomorphism g-mono
263+
} where module F = IsSemimoduleMonomorphism M₁ M₂ f-mono; module G = IsSemimoduleMonomorphism M₂ M₃ g-mono
264264

265265
isSemimoduleIsomorphism : IsSemimoduleIsomorphism M₁ M₂ f →
266266
IsSemimoduleIsomorphism M₂ M₃ g →
267267
IsSemimoduleIsomorphism M₁ M₃ (g ∘ f)
268268
isSemimoduleIsomorphism f-iso g-iso = record
269269
{ isSemimoduleMonomorphism = isSemimoduleMonomorphism F.isSemimoduleMonomorphism G.isSemimoduleMonomorphism
270270
; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
271-
} where module F = IsSemimoduleIsomorphism f-iso; module G = IsSemimoduleIsomorphism g-iso
271+
} where module F = IsSemimoduleIsomorphism M₁ M₂ f-iso; module G = IsSemimoduleIsomorphism M₂ M₃ g-iso
272272

273273
module _
274274
{R : Set r}
@@ -286,20 +286,20 @@ module _
286286
IsModuleHomomorphism M₁ M₃ (g ∘ f)
287287
isModuleHomomorphism f-homo g-homo = record
288288
{ isBimoduleHomomorphism = isBimoduleHomomorphism ≈ᴹ₃-trans F.isBimoduleHomomorphism G.isBimoduleHomomorphism
289-
} where module F = IsModuleHomomorphism f-homo; module G = IsModuleHomomorphism g-homo
289+
} where module F = IsModuleHomomorphism M₁ M₂ f-homo; module G = IsModuleHomomorphism M₂ M₃ g-homo
290290

291291
isModuleMonomorphism : IsModuleMonomorphism M₁ M₂ f →
292292
IsModuleMonomorphism M₂ M₃ g →
293293
IsModuleMonomorphism M₁ M₃ (g ∘ f)
294294
isModuleMonomorphism f-mono g-mono = record
295295
{ isModuleHomomorphism = isModuleHomomorphism F.isModuleHomomorphism G.isModuleHomomorphism
296296
; injective = F.injective ∘ G.injective
297-
} where module F = IsModuleMonomorphism f-mono; module G = IsModuleMonomorphism g-mono
297+
} where module F = IsModuleMonomorphism M₁ M₂ f-mono; module G = IsModuleMonomorphism M₂ M₃ g-mono
298298

299299
isModuleIsomorphism : IsModuleIsomorphism M₁ M₂ f →
300300
IsModuleIsomorphism M₂ M₃ g →
301301
IsModuleIsomorphism M₁ M₃ (g ∘ f)
302302
isModuleIsomorphism f-iso g-iso = record
303303
{ isModuleMonomorphism = isModuleMonomorphism F.isModuleMonomorphism G.isModuleMonomorphism
304304
; surjective = Func.surjective _ _ (_≈ᴹ_ M₃) F.surjective G.surjective
305-
} where module F = IsModuleIsomorphism f-iso; module G = IsModuleIsomorphism g-iso
305+
} where module F = IsModuleIsomorphism M₁ M₂ f-iso; module G = IsModuleIsomorphism M₂ M₃ g-iso

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ module Algebra.Module.Morphism.LeftModuleMonomorphism
1414
(isLeftModuleMonomorphism : IsLeftModuleMonomorphism M N ⟦_⟧)
1515
where
1616

17-
open IsLeftModuleMonomorphism isLeftModuleMonomorphism
17+
open IsLeftModuleMonomorphism M N isLeftModuleMonomorphism
1818
private
1919
module M = RawLeftModule M
2020
module N = RawLeftModule N

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ module Algebra.Module.Morphism.LeftSemimoduleMonomorphism
1414
(isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism M₁ M₂ ⟦_⟧)
1515
where
1616

17-
open IsLeftSemimoduleMonomorphism isLeftSemimoduleMonomorphism
17+
open IsLeftSemimoduleMonomorphism M₁ M₂ isLeftSemimoduleMonomorphism
1818
private
1919
module M = RawLeftSemimodule M₁
2020
module N = RawLeftSemimodule M₂

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ module Algebra.Module.Morphism.ModuleMonomorphism
1414
(isModuleMonomorphism : IsModuleMonomorphism M N ⟦_⟧)
1515
where
1616

17-
open IsModuleMonomorphism isModuleMonomorphism
17+
open IsModuleMonomorphism M N isModuleMonomorphism
1818
private
1919
module M = RawModule M
2020
module N = RawModule N

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ module Algebra.Module.Morphism.RightModuleMonomorphism
1414
(isRightModuleMonomorphism : IsRightModuleMonomorphism M N ⟦_⟧)
1515
where
1616

17-
open IsRightModuleMonomorphism isRightModuleMonomorphism
17+
open IsRightModuleMonomorphism M N isRightModuleMonomorphism
1818
module M = RawRightModule M
1919
module N = RawRightModule N
2020

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ module Algebra.Module.Morphism.RightSemimoduleMonomorphism
1414
(isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism M N ⟦_⟧)
1515
where
1616

17-
open IsRightSemimoduleMonomorphism isRightSemimoduleMonomorphism
17+
open IsRightSemimoduleMonomorphism M N isRightSemimoduleMonomorphism
1818
private
1919
module M = RawRightSemimodule M
2020
module N = RawRightSemimodule N

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ module Algebra.Module.Morphism.SemimoduleMonomorphism
1414
(isSemimoduleMonomorphism : IsSemimoduleMonomorphism M N ⟦_⟧)
1515
where
1616

17-
open IsSemimoduleMonomorphism isSemimoduleMonomorphism
17+
open IsSemimoduleMonomorphism M N isSemimoduleMonomorphism
1818
private
1919
module M = RawSemimodule M
2020
module N = RawSemimodule N

0 commit comments

Comments
 (0)