∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : DecidableEq J], Small.{w, max u w} (AddCommGrpCat.Colimits.Quot F) → CategoryTheory.Limits.HasColimit F