Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Open
mzeuner opened this issue Jan 16, 2024 · 1 comment
Open

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

mzeuner opened this issue Jan 16, 2024 · 1 comment

Comments

@mzeuner
Copy link
Contributor

mzeuner commented Jan 16, 2024

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.
@felixwellen felixwellen self-assigned this Jan 16, 2024
@mzeuner
Copy link
Contributor Author

mzeuner commented Jan 16, 2024

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

@felixwellen felixwellen removed their assignment Jan 16, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@felixwellen @mzeuner