{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : PartialOrder J] →
        (F : CategoryTheory.Functor J C) →
          [F.IsWellOrderContinuous] →
            (m : J) → Order.IsSuccLimit m → CategoryTheory.Limits.IsColimit ((Set.principalSegIio m).cocone F)