∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (A : CategoryTheory.Functor Cᵒᵖ (Type u_2))
  (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type u_2)) (X : Cᵒᵖ),
  CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F (CategoryTheory.CategoryStruct.id X).unop =
    CategoryTheory.CategoryStruct.id (CategoryTheory.OverPresheafAux.YonedaCollection F (Opposite.unop X))