∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u_1)} {ι : Type u_1}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.val}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) (i j k : ι),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (⋯.lift₃ (f k) (f i) (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂ ⋯ (f j) (f k))
          (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃ ⋯ (f j) (f k))
          (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ ⋯ (f j) (f k)) ⋯ ⋯)
        (CategoryTheory.Limits.pullback.snd (⋯.fst' (f k)) (⋯.fst' (f i))))
      (⋯.snd (f i)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (⋯.fst' (f j)) (⋯.fst' (f k)))
        (⋯.symmetry ⋯))
      (⋯.snd (f i))