Further, these limits are preserved by the forgetful functor --- that is, the underlying types are just the limits in the category of types.
A lot of this should be generalised / automated, as it's quite common for concrete categories that the forgetful functor preserves limits.
Construction of a limit cone in CommRing. (Internal use only; use the limits API.)
Witness that the limit cone in CommRing is a limit cone. (Internal use only; use the limits API.)
The category of commutative rings has all limits.
The forgetful functor from commutative rings to types preserves all limits. (That is, the underlying types could have been computed instead as limits in the category of types.)