∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] (J : CategoryTheory.GrothendieckTopology C)
  {D : Type u_6} [inst_1 : CategoryTheory.Category.{u_5, u_6} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D)
  (A : Type u_4) [inst_2 : CategoryTheory.Category.{u_2, u_4} A] [CategoryTheory.Functor.IsDenseSubsite K J e.inverse]
  (F : CategoryTheory.Sheaf K A), CategoryTheory.Presheaf.IsSheaf J (e.functor.op.comp F.val)