pufferffish / agda-symmetries

MIT License
5 stars 1 forks source link

Define free commutative rig (or semiring) #57

Open vikraman opened 8 months ago

vikraman commented 8 months ago

These should have 0, ⊕, 1, ⊗, which are both commutative monoid structures, and ⊗ distributes over ⊕.