Commit 2022-07-28 01:01 350a3817
View on Github →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
.