mathlib

318cb4bc - feat(category_theory): essentially_small categories (#6801)

feat(category_theory): essentially_small categories (#6801) Preparation for `well_powered`, then for `complete_semilattice_Inf|Sup` on `subobject X`, then for work on chain complexes. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>