feat(category_theory/monoidal): 位_ (饾煓_ C) = 蟻_ (饾煓_ C) (#3556)
The incredibly tedious proof from the axioms that `位_ (饾煓_ C) = 蟻_ (饾煓_ C)` in any monoidal category.
One would hope that it falls out from a coherence theorem, but we're not close to having one, and I suspect that this result might be a step in any proof.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
