∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : C) {F F' : CategoryTheory.Sheaf J (Type (max v v'))} (f : F ⟶ F')
  (x : F.val.obj (Opposite.op X)),
  CategoryTheory.CategoryStruct.comp (J.uliftYonedaEquiv.symm x) f =
    J.uliftYonedaEquiv.symm (f.val.app (Opposite.op X) x)