Category instances for has_mul, has_add, semigroup and add_semigroup #
We introduce the bundled categories:
This closely follows
- Limits in these categories
- free/forgetful adjunctions
The category of additive magmas and additive magma morphisms.
The category of additive semigroups and semigroup morphisms.
Once we've shown that the forgetful functors to type reflect isomorphisms,
we automatically obtain that the
forget₂ functors between our concrete categories