We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 5d40c06 commit 7709591Copy full SHA for 7709591
Cubical/Algebra/Module/Properties.agda
@@ -68,7 +68,7 @@ module _ {R : Ring ℓ'} {M N P : LeftModule R ℓ} where
68
69
pres0 : fg 0M ≡ 0P
70
pres0 = cong (g .fst) (f .snd .IsLeftModuleHom.pres0) ∙ g .snd .IsLeftModuleHom.pres0
71
-
+
72
pres+ : (x y : M .fst) → fg (x +M y) ≡ fg x +P fg y
73
-- g(f(x+y)) ≡ g(f(x)+f(y)) ≡ g(f(x))+g(f(y))
74
pres+ x y =
@@ -91,4 +91,4 @@ module _ {R : Ring ℓ'} {M N P : LeftModule R ℓ} where
91
let p = refl {x = g .fst (f .fst (r ⋆M y))} in
92
let p = p ∙ cong (g .fst) (f .snd .IsLeftModuleHom.pres⋆ r y) in
93
let p = p ∙ g .snd .IsLeftModuleHom.pres⋆ r (f .fst y) in
94
- p
+ p
0 commit comments