Commit 2020-09-11 15:53 377c7c91

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.)