mathlib3

43431be5 - chore(category_theory): remove functor.of (#2127)

chore(category_theory): remove functor.of (#2127) * chore(category_theory): remove functor.of * fix Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>