feat(category_theory/monoidal): Drinfeld center (#7186)
# Half braidings and the Drinfeld center of a monoidal category
We define `center C` to be pairs `⟨X, b⟩`, where `X : C` and `b` is a half-braiding on `X`.
We show that `center C` is braided monoidal,
and provide the monoidal functor `center.forget` from `center C` back to `C`.
## Future work
Verifying the various axioms here is done by tedious rewriting.
Using the `slice` tactic may make the proofs marginally more readable.
More exciting, however, would be to make possible one of the following options:
1. Integration with homotopy.io / globular to give "picture proofs".
2. The monoidal coherence theorem, so we can ignore associators
(after which most of these proofs are trivial;
I'm unsure if the monoidal coherence theorem is even usable in dependent type theory).
3. Automating these proofs using `rewrite_search` or some relative.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
