∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P]
  {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  (f : W ⟶ X) [inst_2 : W.Over S] [inst_3 : X.Over S] [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰]
  [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  [inst_6 : Q.HasOfPostcompProperty Q] [inst_7 : Q.IsStableUnderBaseChange] [inst_8 : Q.IsStableUnderComposition]
  (hX : Q (X ↘ S)) (hW : Q (W ↘ S)) (hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)),
  { I₀ := 𝒰.I₀,
        X := fun x =>
          (CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Hom.asOverProp f S)
              (AlgebraicGeometry.Scheme.Hom.asOverProp (𝒰.f x) S)).left,
        f := fun x =>
          (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Hom.asOverProp f S)
              (AlgebraicGeometry.Scheme.Hom.asOverProp (𝒰.f x) S)).left }.presieve₀ ∈
    (AlgebraicGeometry.Scheme.precoverage P).coverings W