∀ {J : Type u_2} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteAddGrp.{max u_2 u_1})
  (cone : CategoryTheory.Limits.Cone F), TotallyDisconnectedSpace ↑cone.1.toProfinite.toTop