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.

Estimated changes