∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C],
  (∀ (α : Type w), CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete α) C) →
    CategoryTheory.AB4OfSize.{w, v, u} C