∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : Cᵒᵖ) (X_1 : CategoryTheory.Sheaf J (Type v))
  (a : ((J.yoneda.op.comp CategoryTheory.coyoneda).obj X).obj X_1),
  ((J.yonedaOpCompCoyoneda.hom.app X).app X_1 a).down =
    CategoryTheory.yonedaEquiv
      (CategoryTheory.CategoryStruct.comp (J.yonedaCompSheafToPresheaf.inv.app (Opposite.unop X)) a.hom)