mathlib3

e99518b2 - feat(category_theory): braided and symmetric categories (#3550)

feat(category_theory): braided and symmetric categories (#3550) Just the very basics: * the definition of braided and symmetric categories * braided functors, and compositions thereof * the symmetric monoidal structure coming from products * upgrading `Type u` to a symmetric monoidal structure This is prompted by the desire to explore modelling sheaves of modules as the monoidal category of module objects for an internal commutative monoid in sheaves of `Ab`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>