Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-14 00:14 bd385fbf

View on Github →

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!

Estimated changes