∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  (A : CategoryTheory.Functor C ℰ) {P Q : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))} (f : P ⟶ Q) (E : ℰ)
  (g : Q ⟶ (CategoryTheory.Presheaf.restrictedULiftYoneda A).obj E)
  (p : CategoryTheory.CostructuredArrow CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁} P),
  ((CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv' A P E).symm (CategoryTheory.CategoryStruct.comp f g)).app p =
    ((CategoryTheory.Presheaf.restrictedULiftYonedaHomEquiv' A Q E).symm g).app
      ((CategoryTheory.CostructuredArrow.map f).obj p)