{X Y : AlgebraicGeometry.Scheme} →
  {f : X ⟶ Y} →
    {motive : AlgebraicGeometry.IsAffineHom f → Sort u} →
      ((isAffine_preimage :
            ∀ (U : Y.Opens),
              AlgebraicGeometry.IsAffineOpen U →
                AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj U)) →
          motive ⋯) →
        (t : AlgebraicGeometry.IsAffineHom f) → motive t