∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_5, u_4} C] {J : CategoryTheory.GrothendieckTopology C}
  {D : Type u_3} [inst_1 : CategoryTheory.Category.{u_2, u_3} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  {X : C} {K : Type u_1} [inst_3 : CategoryTheory.SmallCategory K]
  {F : CategoryTheory.Functor K (CategoryTheory.Functor Cᵒᵖ D)} {W : J.Cover X} (i : W.Arrow)
  (E :
    CategoryTheory.Limits.Cone
      (F.comp ((J.diagramFunctor D X).comp ((CategoryTheory.evaluation (J.Cover X)ᵒᵖ D).obj (Opposite.op W)))))
  ⦃X_1 Y : K⦄ (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp (((CategoryTheory.Functor.const K).obj E.pt).map f)
      (CategoryTheory.CategoryStruct.comp (E.π.app Y) (CategoryTheory.Limits.Multiequalizer.ι (W.index (F.obj Y)) i)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (E.π.app X_1)
        (CategoryTheory.Limits.Multiequalizer.ι (W.index (F.obj X_1)) i))
      ((F.comp ((CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op i.Y))).map f)