category_theory.limits.fin_category
A category with a
fintype
of objects, and a
fintype
for each morphism space.