∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {F : CategoryTheory.PreZeroHypercover S} {G : CategoryTheory.PreZeroHypercover S}
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] (f : G.Hom E) (g : G.Hom F)
  (i : G.I₀),
  CategoryTheory.CategoryStruct.comp (f.h₀ i) (E.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm (f.s₀ i, g.s₀ i)).fst) =
    CategoryTheory.CategoryStruct.comp (g.h₀ i) (F.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm (f.s₀ i, g.s₀ i)).snd)