mathlib

1a5e56f2 - feat(category_theory/localization): basic API for localization of categories (#16969)

feat(category_theory/localization): basic API for localization of categories (#16969) In this PR, the basic API for the localization of categories is introduced. If a functor `L : C ⥤ D` is a localization functor for `W : morphism_property C`, we shall say that a functor `F' : D ⥤ E` lifts a functor `F : C ⥤ E` if an isomorphism `L ⋙ F' ≅ F` is given: this is the class `[lifting L W F F']`. The basic API for lifting of functors and lifting of natural transformations is included.