mathlib3

9f525c74 - chore(category_theory/limits/types): cleanup (#3871)

chore(category_theory/limits/types): cleanup (#3871) Backporting some cleaning up work from `prop_limits`, while it rumbles onwards. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>