mathlib3

0e1387bb - feat(category_theory): the category of small categories has all small limits (#12979)