Commit 2024-12-13 07:54 383b0748
View on Github →feat(CategoryTheory/Localization): liftings of bifunctors (#19894)
When a functor F : C ⥤ E inverts a class of morphisms W : MorphismProperty C and L : C ⥤ D is a localization functor for W, then F lifts as a functor D ⥤ E. In this PR, this is generalized to bifunctors (or "functors in two variables") F : C₁ ⥤ C₂ ⥤ E, which may be lifted as a functor D₁ ⥤ D₂ ⥤ E under similar assumptions.
(We shall also need a version of this in three variables.)