Commit 2020-08-02 11:46 e99518b2

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.