Counit morphisms for multivariate polynomials
One may consider the ring of multivariate polynomials
mv_polynomial A R with coefficients in
and variables indexed by
A is not just a type, but an algebra over
then there is a natural surjective algebra homomorphism
mv_polynomial A R →ₐ[R] A
X a ↦ a.