∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasCoproduct F.obj],
  CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.colimit.ι F))