∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X : C} {F : CategoryTheory.Sheaf J (Type (max v v'))} (x : F.obj.obj (Opposite.op X))
  (Y : Cᵒᵖ) (f : Opposite.unop Y ⟶ X), (J.uliftYonedaEquiv.symm x).hom.app Y { down := f } = F.obj.map f.op x