∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {T : CategoryTheory.Over A} {X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A}
  (f : (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda A).obj X ⟶ T),
  (CategoryTheory.overEquivPresheafCostructuredArrow A).inverse.map
      ((CategoryTheory.CostructuredArrow.toOverCompYoneda A T).hom.app (Opposite.op X) f) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow A).isoCompInverse.inv.app X)
      (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.overEquivPresheafCostructuredArrow A).unit.app T))