∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : ι → C} {c : CategoryTheory.Limits.Cofan X}
  (hc : CategoryTheory.Limits.IsColimit c) [∀ (i : ι), CategoryTheory.Mono (c.inj i)]
  (s : {i j : ι} → i ≠ j → CategoryTheory.Limits.PullbackCone (c.inj i) (c.inj j))
  (hs : {i j : ι} → (hij : i ≠ j) → CategoryTheory.Limits.IsLimit (s hij))
  (H : {i j : ι} → (hij : i ≠ j) → CategoryTheory.Limits.IsInitial (s hij).pt),
  CategoryTheory.Limits.CoproductDisjoint X