∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {J : Type u_6}
  [inst_1 : CategoryTheory.Category.{u_5, u_6} J] {K : Type u_1} [inst_2 : CategoryTheory.Category.{u_4, u_1} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)) (j₁ j₂ : J) (g : j₁ ⟶ j₂),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Functor.const J).obj
            { obj := fun k => (c k).cone.pt,
              map := fun {k₁ k₂} f =>
                (c k₂).isLimit.lift
                  { pt := (c k₁).cone.pt, π := CategoryTheory.CategoryStruct.comp (c k₁).cone.π (F.flip.map f) },
              map_id := ⋯, map_comp := ⋯ }).map
        g)
      { app := fun k => (c k).cone.π.app j₂, naturality := ⋯ } =
    CategoryTheory.CategoryStruct.comp { app := fun k => (c k).cone.π.app j₁, naturality := ⋯ } (F.map g)