∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] (J : CategoryTheory.GrothendieckTopology C)
  (D : Type u_4) [inst_1 : CategoryTheory.Category.{u_2, u_4} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  (X : C) {X_1 Y Z : CategoryTheory.Functor Cᵒᵖ D} (f : X_1 ⟶ Y) (g : Y ⟶ Z),
  J.diagramNatTrans (CategoryTheory.CategoryStruct.comp f g) X =
    CategoryTheory.CategoryStruct.comp (J.diagramNatTrans f X) (J.diagramNatTrans g X)