∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D),
  CategoryTheory.Limits.Cocone.functoriality F G =
    { obj := fun A => { pt := G.obj A.pt, ι := CategoryTheory.NatTrans.mk' (fun j => G.map (A.ι.app j)) ⋯ },
      map := fun {x x_1} f => { hom := G.map f.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }