∀ (n : Type u_2) (S : AlgebraicGeometry.Scheme),
  CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.terminal.from S)
    (CategoryTheory.Limits.terminal.from
      (AlgebraicGeometry.Spec
        { carrier := MvPolynomial n (ULift.{max u_1 u_2, 0} ℤ), commRing := MvPolynomial.instCommRingMvPolynomial }))