∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_1)
  [W.RespectsIso],
  (∀ (X₁ X₂ : J → C) [inst_2 : CategoryTheory.Limits.HasCoproduct X₁] [inst_3 : CategoryTheory.Limits.HasCoproduct X₂]
      (f : (j : J) → X₁ j ⟶ X₂ j), (∀ (j : J), W (f j)) → W (CategoryTheory.Limits.Sigma.map f)) →
    W.IsStableUnderCoproductsOfShape J