mathlib

c43486ec - feat(category_theory/limits): allow (co)limits over lower universes in algebraic categories (#13990)

feat(category_theory/limits): allow (co)limits over lower universes in algebraic categories (#13990) I'm concerned about the new universe annotations required in places. It was not so impossible to add them when proofs broke, but the proofs might have been hard to construct in the first place .... Co-authored-by: Scott Morrison <scott.morrison@gmail.com>