Multivariable polynomials on a type is the left adjoint of the forgetful functor from commutative rings to types.

CommRing.free

The free functor Type u тед CommRing.{u} sending a type X to the multivariable (commutative) polynomials with variables x : X.

CommRing.adj

The free-forgetful adjunction for commutative rings.