{X Y : AlgebraicGeometry.Scheme} →
  {f : X ⟶ Y} →
    {motive : AlgebraicGeometry.ValuativeCommSq f → Sort u_1} →
      (t : AlgebraicGeometry.ValuativeCommSq f) →
        ((R : Type u) →
            [commRing : CommRing R] →
              [domain : IsDomain R] →
                [valuationRing : ValuationRing R] →
                  (K : Type u) →
                    [field : Field K] →
                      [algebra : Algebra R K] →
                        [isFractionRing : IsFractionRing R K] →
                          (i₁ :
                              AlgebraicGeometry.Spec { carrier := K, commRing := Field.toEuclideanDomain.toCommRing } ⟶
                                X) →
                            (i₂ : AlgebraicGeometry.Spec { carrier := R, commRing := commRing } ⟶ Y) →
                              (commSq :
                                  CategoryTheory.CommSq i₁
                                    (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))) f i₂) →
                                motive
                                  { R := R, commRing := commRing, domain := domain, valuationRing := valuationRing,
                                    K := K, field := field, algebra := algebra, isFractionRing := isFractionRing,
                                    i₁ := i₁, i₂ := i₂, commSq := commSq }) →
          motive t