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.

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

Introduce Semiring and refactor finite sums #1042

Merged
merged 13 commits into from
Sep 11, 2023
Prev Previous commit
Next Next commit
Semiring: reexport better names
felixwellen committed Sep 10, 2023

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
commit 55e8633beba010a82ecea92793ab71426c001efb
6 changes: 5 additions & 1 deletion Cubical/Algebra/Semiring/Base.agda
Original file line number Diff line number Diff line change
@@ -25,7 +25,11 @@ record IsSemiring {R : Type ℓ}
open IsCommMonoid +IsCommMonoid public
renaming
( isSemigroup to +IsSemigroup
; isMonoid to +IsMonoid)
; isMonoid to +IsMonoid
; ·Comm to +Comm
; ·Assoc to +Assoc
; ·IdR to +IdR
; ·IdL to +IdL)

open IsMonoid ·IsMonoid public
renaming