∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))}
  (x : F.obj (Opposite.op X)) (Y : Cᵒᵖ) (y : (CategoryTheory.uliftYoneda.{w, v₁, u₁}.obj X).obj Y),
  (CategoryTheory.uliftYonedaEquiv.symm x).app Y y = F.map y.down.op x