mathlib

a52be2a5 - feat(category_theory/localization): whiskering_left_equivalence and definition of the predicate (#16646)

feat(category_theory/localization): whiskering_left_equivalence and definition of the predicate (#16646) In this PR, an equivalence `localization.construction.whiskering_left_equivalence W D : (W.localization ⥤ D) ≌ W.functors_inverting D` is obtained and the predicate `L.is_localization W` is defined for a functor `L : C ⥤ D`.