mathlib3

bd385fbf - chore(category_theory/limits/functor_category): shuffle limits in functor cats (#4124)

chore(category_theory/limits/functor_category): shuffle limits in functor cats (#4124) Give `is_limit` versions for statements about limits in the functor category, and write the `has_limit` versions in terms of those. This also generalises the universes a little. As usual, suggestions for better docstrings or better names appreciated!