mathlib

8efef279 - feat(category_theory/localization): localization of the opposite category (#17199)

feat(category_theory/localization): localization of the opposite category (#17199) If a functor `L : C ⥤ D` is a localization functor for `W : morphism_property C`, it is shown in this PR that `L.op : Cᵒᵖ ⥤ Dᵒᵖ` is also a localization functor.