∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat),
  ↑(CategoryTheory.Cat.HasLimits.limitConeX F) = CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)