∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] (X Y : C)
  [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (m m' n : M),
  CategoryTheory.Localization.HasSmallLocalizedHom W
    ((CategoryTheory.shiftFunctor C m').obj ((CategoryTheory.shiftFunctor C m).obj X))
    ((CategoryTheory.shiftFunctor C n).obj Y)