mathlib3

7c09ed5e - feat(category_theory/*): define `Cat` and a fully faithful functor `Mon ⥤ Cat` (#1235)

feat(category_theory/*): define `Cat` and a fully faithful functor `Mon ⥤ Cat` (#1235) * feat(category_theory/*): define `Cat` and a fully faithful functor `Mon ⥤ Cat` * Drop 2 commas * Drop `functor.id_comp` etc, add `Cat.str` instance, adjust module-level comments * Make `α` and `β` arguments of `map_hom_equiv` explicit This way `e α β f` is automatically interpreted as `(e α β).to_fun f`.