mathlib3

feat(category/equiv_functor): type-level functoriality w.r.t. equiv

#2255

Merged