∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  (X : CategoryTheory.Sheaf J D),
  ((CategoryTheory.sheafificationNatIso J D).hom.app X).hom = CategoryTheory.toSheafify J X.obj