∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3}
  {E : Type u_4} [inst_1 : CategoryTheory.Category.{max v u, u_3} D] [inst_2 : CategoryTheory.Category.{max v u, u_4} E]
  (F : CategoryTheory.Functor D E)
  [∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  {FD : D → D → Type u_5} {CD : D → Type (max v u)} {FE : E → E → Type u_6} {CE : E → Type (max v u)}
  [inst_9 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_10 : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)]
  [instCCD : CategoryTheory.ConcreteCategory D FD] [instCCE : CategoryTheory.ConcreteCategory E FE]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)]
  [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget E)] [(CategoryTheory.forget D).ReflectsIsomorphisms]
  [(CategoryTheory.forget E).ReflectsIsomorphisms], J.PreservesSheafification F