{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} 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)] →
            [inst_2 :
                ∀ (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))] →
              (E.inter F).Hom F