{X Y : AlgebraicGeometry.Scheme} →
  {f : X ⟶ Y} →
    {motive : AlgebraicGeometry.GeometricallyReduced f → Sort u} →
      (t : AlgebraicGeometry.GeometricallyReduced f) →
        ((geometrically_isReduced : AlgebraicGeometry.geometrically AlgebraicGeometry.IsReduced f) → motive ⋯) →
          motive t