mathlib3

1588d81e - feat(category_theory): remove nearly all universe annotations (#3221)

feat(category_theory): remove nearly all universe annotations (#3221) Due to some recent changes to mathlib (does someone know the relevant versions/commits?) most of the universe annotations `.{v}` and `include 𝒞` statements that were previously needed in the category_theory library are no longer necessary. This PR removes them! Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>