∀ {C : Type u} [inst : CategoryTheory.Category.{max w v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : C) (X_1 : Cᵒᵖ)
  (a :
    ((CategoryTheory.sheafToPresheaf J (Type (max v w))).obj
          ((CategoryTheory.GrothendieckTopology.uliftYoneda.{w, max v w, u} J).obj X)).obj
      X_1),
  (J.uliftYonedaIsoYoneda.hom.app X).hom.app X_1 a = a.down