∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor C (Type v₁)}
  (x : F.obj X) (Y : C) (f : X ⟶ Y), (CategoryTheory.coyonedaEquiv.symm x).app Y f = F.map f x