∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : C) {X_1 Y : Cᵒᵖ} (f : X_1 ⟶ Y)
  (a : CategoryTheory.uliftFunctor.{w, v}.obj ((J.yoneda.obj X).val.obj X_1)),
  (((CategoryTheory.GrothendieckTopology.uliftYoneda.{w, v, u} J).obj X).val.map f a).down =
    CategoryTheory.CategoryStruct.comp f.unop a.down