∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (A : CategoryTheory.Functor Cᵒᵖ (Type u_1))
  {X Y : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda A).comp
            (CategoryTheory.OverPresheafAux.restrictedYoneda A)).map
        f)
      ((fun s =>
            CategoryTheory.NatIso.ofComponents
              (fun x => CategoryTheory.OverPresheafAux.OverArrows.costructuredArrowIso s (Opposite.unop x)) ⋯)
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun s =>
            CategoryTheory.NatIso.ofComponents
              (fun x => CategoryTheory.OverPresheafAux.OverArrows.costructuredArrowIso s (Opposite.unop x)) ⋯)
          X).hom
      (CategoryTheory.yoneda.map f)