(R : Type w) →
  [inst : Ring R] →
    {C : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          (W : CategoryTheory.MorphismProperty C) →
            [CategoryTheory.Linear R C] →
              [inst_4 : W.HasLocalization] →
                [inst_5 : CategoryTheory.Preadditive W.Localization'] →
                  [W.Q'.Additive] → CategoryTheory.Linear R W.Localization'