∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] {i j : E.I₀ × F.I₀} {W : C}
  {p₁ : W ⟶ CategoryTheory.Limits.pullback (E.f i.1) (F.f i.2)}
  {p₂ : W ⟶ CategoryTheory.Limits.pullback (E.f j.1) (F.f j.2)},
  CategoryTheory.CategoryStruct.comp p₁
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (E.f i.1) (F.f i.2)) (E.f i.1)) =
      CategoryTheory.CategoryStruct.comp p₂
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (E.f j.1) (F.f j.2)) (E.f j.1)) →
    (E.inter F).sieve₁ p₁ p₂ =
      CategoryTheory.Sieve.bind
        (E.sieve₁ (CategoryTheory.CategoryStruct.comp p₁ (CategoryTheory.Limits.pullback.fst (E.f i.1) (F.f i.2)))
            (CategoryTheory.CategoryStruct.comp p₂ (CategoryTheory.Limits.pullback.fst (E.f j.1) (F.f j.2)))).arrows
        fun x f x_1 =>
        CategoryTheory.Sieve.pullback f
          (F.sieve₁ (CategoryTheory.CategoryStruct.comp p₁ (CategoryTheory.Limits.pullback.snd (E.f i.1) (F.f i.2)))
            (CategoryTheory.CategoryStruct.comp p₂ (CategoryTheory.Limits.pullback.snd (E.f j.1) (F.f j.2))))