∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C] {J : CategoryTheory.GrothendieckTopology C}
  {D : Type u_5} [inst_1 : CategoryTheory.Category.{u_4, u_5} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  {K : Type u_1} [inst_3 : CategoryTheory.SmallCategory K] [CategoryTheory.Limits.HasLimitsOfShape K D]
  (F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)) (X : C),
  CategoryTheory.Limits.HasLimit (F.comp (J.diagramFunctor D X))