Essential surjectivity of the functor induced on composable arrows

Assuming that L : C ⥤ D is a localization functor for a class of morphisms W that has a calculus of left or right fractions, we show in this file that the functor L.mapComposableArrows n : ComposableArrows C n ⥤ ComposableArrows D n is essentially surjective for any n : ℕ.

theorem CategoryTheory.Localization.essSurj_mapComposableArrows_of_hasRightCalculusOfFractions {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] (n : ℕ) : (L.mapComposableArrows n).EssSurj

theorem CategoryTheory.Localization.essSurj_mapComposableArrows {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasLeftCalculusOfFractions] (n : ℕ) : (L.mapComposableArrows n).EssSurj