{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {ℰ : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ] →
        (A : CategoryTheory.Functor C ℰ) →
          (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))) →
            (E : ℰ) →
              ((CategoryTheory.CostructuredArrow.proj CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁} P).comp A ⟶
                  (CategoryTheory.Functor.const
                        (CategoryTheory.CostructuredArrow CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁} P)).obj
                    E) ≃
                (P ⟶ (CategoryTheory.Presheaf.restrictedULiftYoneda A).obj E)