∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max u_3 u_2)))
  {x₁ x₂ : P.Elementsᵒᵖ} (f : x₁ ⟶ x₂),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Presheaf.functorToRepresentables P).map f)
      (CategoryTheory.uliftYonedaEquiv.symm (Opposite.unop x₂).snd) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYonedaEquiv.symm (Opposite.unop x₁).snd)
      (((CategoryTheory.Functor.const P.Elementsᵒᵖ).obj P).map f)