∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y : C}
  {η : CategoryTheory.yoneda.obj Y ⟶ A} {X : C} {s : CategoryTheory.yoneda.obj X ⟶ A} {f : X ⟶ Y}
  (hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) η = s),
  (CategoryTheory.OverPresheafAux.OverArrows.yonedaArrow f hf).val = f