mathlib

1baf7017 - feat(category_theory/Fintype): Adds the category of finite types and its "standard" skeleton. (#4809)

feat(category_theory/Fintype): Adds the category of finite types and its "standard" skeleton. (#4809) This PR adds the category `Fintype` of finite types, as well as its "standard" skeleton whose objects are `fin n`. Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>