feat(category_theory/sums): sums (disjoint unions) of categories (#1357)
* feat(category_theory/sum): direct sums of categories
* minor
* tidying
* Fix white space, remove old comments
* rearranging, associator
* add TODO comment about unitors
* fix import
* create /basic.lean files