Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I started an article, surreal number. I’ve run out of energy to put in all the links that should be in there.
I want to get at Conway games at some point, as they are more basic than Conway numbers, and fit well within an nPOV. Conway discovered numbers after games, and it seems only right to establish that priority also within the Lab. In particular, one should mention Joyal’s description of the category of games, and what this has to do with the ordering on numbers.
I added a comment to surreal number about how to make the definition constructive, and a brief reference to the HoTT version.
1 to 2 of 2