∀ {J : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} J] (F : CategoryTheory.Functor J (Type u_1))
  [inst_1 : Small.{u_1, max u_1 u_2} F.ColimitType],
  Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.colimitCocone F))