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