∀ (P : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme),
  AlgebraicGeometry.geometrically P =
    CategoryTheory.MorphismProperty.universally fun X Y x => AlgebraicGeometry.IsIntegral Y → Subsingleton ↥Y → P X