(P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) →
  {S : AlgebraicGeometry.Scheme} →
    [P.IsStableUnderBaseChange] →
      [P.IsMultiplicative] →
        [P.RespectsIso] →
          [inst : Q.IsStableUnderComposition] →
            [inst_1 : Q.IsStableUnderBaseChange] →
              [inst_2 : Q.HasOfPostcompProperty Q] → CategoryTheory.Pretopology (Q.Over ⊤ S)