@soaproot This is a special case of the adjunction between rigs (+, ×, 0, 1) to rings (+, ×, -, 0, 1). You could formalize the fact that any rig R gives a ring R* such that R embeds into R* universally. I believe this is how Unimath library formalizes reals.
@andrejbauer In Metamath we develop reals way before we do anything with rings (or rigs, or groups, or any other algebraic structures). Which I guess is to my taste, but I try not to be too dogmatic about whether one or the other is better. (In this case the order of topics was decided WAY before I was working on the project).
@andrejbauer @soaproot "*adjunction* between rigs (+, ×, 0, 1) to rings (+, ×, -, 0, 1)"???
@Paul_Taylor @andrejbauer It is called "completion" at https://ncatlab.org/nlab/show/rig , if I am reading that page correctly.
@Paul_Taylor @soaproot A reflection would be a better word to use (especially if we restrict to cancelative rigs so that the unit is monic).
Oct 29, 2026, 8:33 PM@andrejbauer Does the adjunction (nicely) factor through "cancellative rigs", i.e., rigs where the addition is a cancellative monoid?
Oct 29, 2026, 10:42 PM@andrejbauer Nor do I! The forgetful functor obviously so factors. Working with AFTs is not really my area of expertise.