∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat}
  (c : CategoryTheory.Limits.Cocone F)
  (hc : CategoryTheory.Limits.IsColimit ((CategoryTheory.forget TopCat).mapCocone c)),
  Nonempty (CategoryTheory.Limits.IsColimit c) ↔
    c.pt.str = ⨆ j, TopologicalSpace.coinduced (⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j))) (F.obj j).str