∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S}
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)]
  [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
      CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
        (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))]
  {G : CategoryTheory.PreOneHypercover S} (f : G.Hom E) (g : G.Hom F) {i j : G.I₀} (k : G.I₁ i j),
  CategoryTheory.Limits.HasPullback
    (CategoryTheory.CategoryStruct.comp (E.p₁ (f.s₁ k, g.s₁ k).1)
      (E.f ((CategoryTheory.PreZeroHypercover.interLift f.toHom g.toHom).s₀ i).1))
    (CategoryTheory.CategoryStruct.comp (F.p₁ (f.s₁ k, g.s₁ k).2)
      (F.f ((CategoryTheory.PreZeroHypercover.interLift f.toHom g.toHom).s₀ i).2))