mathlib3

31ef79d3 - feat(category_theory/functorial): unbundled functors