∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} (I : S.Arrow) {Z : C} (g : Z ⟶ I.Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (I.precomp g).Y) (I.precomp g).f =
    CategoryTheory.CategoryStruct.comp g I.f