∀ {S : AlgebraicGeometry.Scheme} (𝒰 : CategoryTheory.PreZeroHypercover S) [AlgebraicGeometry.QuasiCompactCover 𝒰]
  {T : AlgebraicGeometry.Scheme} (f : T ⟶ S),
  AlgebraicGeometry.QuasiCompactCover (CategoryTheory.PreZeroHypercover.pullback₁ f 𝒰)