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.