∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.PreZeroHypercover S)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)],
  E.inter F =
    (E.bind fun i => CategoryTheory.PreZeroHypercover.pullback₁ (E.f i) F).reindex (Equiv.sigmaEquivProd E.I₀ F.1).symm