∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (c : (k : K) → CategoryTheory.Limits.ColimitCocone (F.flip.obj k)) (j : J) (k : K),
  ((CategoryTheory.Limits.combineCocones F c).ι.app j).app k = (c k).cocone.ι.app j