∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y)
  (U : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i => ↑i) ⋯)).I₀),
  CategoryTheory.Limits.HasPullback f (↑U).ι