{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [P.RespectsIso] →
    {X : AlgebraicGeometry.Scheme} →
      (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
        (J : Type u_1) →
          (obj : J → AlgebraicGeometry.Scheme) →
            (map : (i : J) → obj i ⟶ X) →
              (e₁ : J ≃ 𝒰.I₀) →
                (e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)) →
                  (∀ (i : J), map i = CategoryTheory.CategoryStruct.comp (e₂ i).hom (𝒰.f (e₁ i))) →
                    AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X