{X Y : AlgebraicGeometry.Scheme} →
  {f : X ⟶ Y} →
    {motive : AlgebraicGeometry.IsIntegralHom f → Sort u} →
      (t : AlgebraicGeometry.IsIntegralHom f) →
        ([toIsAffineHom : AlgebraicGeometry.IsAffineHom f] →
            (isIntegral_app :
                ∀ (U : Y.Opens),
                  AlgebraicGeometry.IsAffineOpen U →
                    (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U)).IsIntegral) →
              motive ⋯) →
          motive t