{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  (S : AlgebraicGeometry.Scheme) →
    [inst : P.IsStableUnderBaseChange] →
      [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
        [inst_2 : P.IsStableUnderComposition] →
          {X : AlgebraicGeometry.Scheme} →
            (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
              (𝒱 : (x : 𝒰.I₀) → AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) (𝒰.X x)) →
                [inst_3 : X.Over S] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] →
                    [(x : 𝒰.I₀) → AlgebraicGeometry.Scheme.Cover.Over S (𝒱 x)] →
                      (j : (CategoryTheory.Precoverage.ZeroHypercover.bind 𝒰 𝒱).I₀) →
                        ((CategoryTheory.Precoverage.ZeroHypercover.bind 𝒰 𝒱).X j).Over S