of_type_functor m converts from Lean's Type-based category to category_theory. This allows us to use these functors in category theory.