mathlib

350a3817 - feat(category_theory): construction of the localized category (#14422)

feat(category_theory): construction of the localized category (#14422) When `W : morphism_property C` is a class of morphisms in a category `C`, this PR constructs the localized category `localization W` obtained by adding formal inverses to the morphisms in `W`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>