∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  (c : CategoryTheory.Limits.Cone F),
  Nonempty (CategoryTheory.Limits.IsLimit c) ↔ Function.Bijective (CategoryTheory.Limits.Types.sectionOfCone c)