Monoidal category theory

Repository-owned extensions of Mathlib's monoidal-category theory. Monoidal categories supply the base structure used by enriched categories. Compatibility with triangulated structure is an additional interface, not an assumption on all monoidal or all triangulated categories.