∀ {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)] (x : (E.inter F).I₀),
  (E.interFst F).h₀ x =
    CategoryTheory.Limits.pullback.fst (E.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm x).fst)
      (F.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm x).snd)