Add `Algebra.Properties.IdempotentCommutativeMonoid`

agda / agda-stdlib

The Agda standard library

Other

575 stars 237 forks source link

Closed jamesmckinna closed 2 months ago

jamesmckinna commented 3 months ago

Cf. #2138 / #2402 as well as #2403 / #2407 together with

Algebra.Properties.IsBand
etc. Eg Algebra.Solver.IdempotentCommutativeMonoid.distr could/should be lifted out ... what else though?