{P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [P.RespectsIso] →
    [P.ContainsIdentities] →
      [P.IsStableUnderComposition] →
        {X Y : AlgebraicGeometry.Scheme} →
          AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X →
            (f : X ⟶ Y) →
              [CategoryTheory.IsIso f] → AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) Y