{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) →
      CategoryTheory.yoneda.op.comp (CategoryTheory.yoneda.obj P) ≅ P.comp CategoryTheory.uliftFunctor.{u₁, v₁}