search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
446 stars 136 forks source link

SumMap in Algebra.Ring.BigOps should come from Semirings /Monoids #1088

Open mzeuner opened 7 months ago

mzeuner commented 7 months ago

The fact that morphisms preserve finite sums is proven for rings only but does already hold for monoids! The lemma should be proven in Monoid.BigOp first and then for semirings and rings using the result for monoids.

mzeuner commented 7 months ago

See: https://github.com/agda/cubical/pull/1082/files#diff-6fe4c83e4a023cad8085df9b73979dbf43c990f3f2987d9975c27931ac6c28d8R61