∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] (C : Type u₃) [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) {X Y : Cᵒᵖ} (f : X ⟶ Y)
  (a : (CategoryTheory.yoneda.obj F).obj ((CategoryTheory.Functor.const J).op.obj X)) (X_1 : J),
  (((CategoryTheory.cones J C).obj F).map f a).app X_1 = CategoryTheory.CategoryStruct.comp f.unop (a.app X_1)