mathlib3

feat(category_theory/*): define `Cat` and a fully faithful functor `Mon ⥤ Cat`

#1235

Merged