Commit 2022-10-25 06:39 1a5e56f2
View on Github →feat(category_theory/localization): basic API for localization of categories (#16969)
In this PR, the basic API for the localization of categories is introduced. If a functor L : C ⥤ D
is a localization functor for W : morphism_property C
, we shall say that a functor F' : D ⥤ E
lifts a functor F : C ⥤ E
if an isomorphism L ⋙ F' ≅ F
is given: this is the class [lifting L W F F']
. The basic API for lifting of functors and lifting of natural transformations is included.