mathlib

ceacf541 - feat(category_theory/filtered): filtered categories, and filtered colimits in `Type` (#3960)

feat(category_theory/filtered): filtered categories, and filtered colimits in `Type` (#3960) This is some work @rwbarton did last year. I've merged master, written some comments, and satisfied the linter. Co-authored-by: Reid Barton <rwbarton@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>