feat(category_theory): every category is essentially small... (#15874)
feat(category_theory): every category is essentially small... (#15874)

...if you look at it from far enough away.





leanprover-community/mathlib,leanprover-community/mathlib