mathlib3

95e83ced - feat(category_theory/site/limits): generalise universes (#18817)

feat(category_theory/site/limits): generalise universes (#18817) The objects in category `C` in this file had type `Type max v u` but there's no reason they can't just have type `Type u`. There are no uses in this file of `u` as a universe by itself, so this does not make any results less general. This makes porting the file easier. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Universe.20issues.20with.20concrete.20categories/near/350340297)