Category instances for monoid, add_monoid, comm_monoid, and add_comm_monoid.

We introduce the bundled categories:

• Mon
• AddMon
• CommMon
• AddCommMon along with the relevant forgetful functors between them.

Implementation notes

Note [locally reducible category instances]

We make SemiRing (and the other categories) locally reducible in order to define its instances. This is because writing, for example,

instance : concrete_category SemiRing := by { delta SemiRing, apply_instance }

results in an instance of the form id (bundled_hom.concrete_category _) and this id, not being [reducible], prevents a later instance search (once SemiRing is no longer reducible) from seeing that the morphisms of SemiRing are really semiring morphisms (→+*), and therefore have a coercion to functions, for example. It's especially important that the has_coe_to_sort instance not contain an extra id as we want the semiring ↥R instance to also apply to semiring R.α (it seems to be impractical to guarantee that we always access R.α through the coercion rather than directly).

TODO: Probably @[derive] should be able to create instances of the required form (without id), and then we could use that instead of this obscure local attribute [reducible] method.