∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁)))
  {X Y : P.Elementsᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.Presheaf.functorToRepresentables P).map f = CategoryTheory.uliftYoneda.{w, v₁, u₁}.map (↑f.unop).unop