∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  [CategoryTheory.Limits.HasInitial J] {F : CategoryTheory.Functor J C}
  [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)], CategoryTheory.Limits.HasColimit F