Add `IdempotentMonoid` and `CommutativeBand`

[Taneb]

These feel fairly obvious omissions to the algebra hierarchy.

A commutative band is the same thing as a semilattice but I think it's worth duplicating

Example of a commutative band that is not an idempotent commutative monoid: minimum on naturals

Example of an idempotent monoid that is not an idempotent commtuative monoid: first non-nothing element on Maybe

[jamesmckinna]

v2.1, as per our current cutoff policy?

[Taneb]

I don't think there's any backwards compatibility issues here so I'm fine with that

[jamesmckinna]

Also: 'tropical' semiring(s)?

[Taneb]

I think from skimming the page you linked, that that's a particular idempotent semiring, which we already have in Algebra

[MatthewDaggitt]

Indeed, it's my favourite idempotent semiring 😄

[jamesmckinna]

Well, shortest-path routing... I guess it would be!?

[jamesmckinna]

@Taneb any progress towards a PR on this?

UPDATED: eg do you envisage a design which takes a base isMonoid : IsMonoid field and adds an idem : Idempotent one, or using a completely 'flattened' record type?
(Possible upstream issue for Agda's type theory/implementation: better support for mixins...)