∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat)
  (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Cat.HasLimits.limitConeLift F s).toFunctor =
    {
      obj :=
        CategoryTheory.Limits.limit.lift (F.comp CategoryTheory.Cat.objects)
          { pt := ↑s.pt, π := { app := fun j => (s.π.app j).toFunctor.obj, naturality := ⋯ } },
      map := fun {X Y} f =>
        CategoryTheory.Limits.Types.Limit.mk
          (CategoryTheory.Cat.HasLimits.homDiagram
            (CategoryTheory.Limits.limit.lift (F.comp CategoryTheory.Cat.objects)
              { pt := ↑s.pt, π := { app := fun j => (s.π.app j).toFunctor.obj, naturality := ⋯ } } X)
            (CategoryTheory.Limits.limit.lift (F.comp CategoryTheory.Cat.objects)
              { pt := ↑s.pt, π := { app := fun j => (s.π.app j).toFunctor.obj, naturality := ⋯ } } Y))
          (fun j =>
            CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
              (CategoryTheory.CategoryStruct.comp ((s.π.app j).toFunctor.map f) (CategoryTheory.eqToHom ⋯)))
          ⋯,
      map_id := ⋯, map_comp := ⋯ }