feat(category_theory/braided): braiding and unitors (#4075)
The interaction between braidings and unitors in a braided category.
Requested by @cipher1024 for some work he's doing on monads.
I've changed the statements of some `@[simp]` lemmas, in particular `left_unitor_tensor`, `left_unitor_tensor_inv`, `right_unitor_tensor`, `right_unitor_tensor_inv`. The new theory is that the components of a unitor indexed by a tensor product object are "more complicated" than other unitors. (We already follow the same principle for simplifying associators using the pentagon equation.)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
