∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat)
  [inst_1 : CategoryTheory.Limits.HasColimit F],
  (CategoryTheory.Limits.colimit F).str =
    ⨆ j,
      TopologicalSpace.coinduced (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)))
        (F.obj j).str