## Surreal Numbers as Inductive Type?

Prompted by James Propp's recent question about surreal numbers, I was wondering whether anyone had investigated the idea of describing surreal numbers (as ordered class) in terms of a universal property, roughly along the following lines.

In categorical interpretations of type theories, it is common to describe inductive or recursive types as so-called initial algebras of endofunctors. The most famous example is the type of natural numbers, which is universal or initial among all sets $X$ which come equipped with an element $x$ and an function $f: X \to X$. In other words, initial among sets $X$ which come equipped with functions $1 + X \to X$ (the plus is coproduct); we say such sets are algebras of the endofunctor $F$ defined by $F(X) = 1 + X$. Another example is the type of binary trees, which can be described as initial with respect to sets that come equipped with an element and a binary operation, or in other words the initial algebra for the endofunctor $F(X) = 1 + X^2$.

In their book Algebraic Set Theory, Joyal and Moerdijk gave a kind of algebraic description of the cumulative hierarchy $V$. Under some reasonable assumptions on a background category (whose objects may be informally regarded as classes, and equipped with a structure which allows a notion of 'smallness'), they define a ZF-structure as an ordered object which has small sups (in particular, an empty sup with which to get started) and with a 'successor' function. Then, against such a background, they define the cumulative hierarchy $V$ as the initial ZF-structure, and show that it satisfies the axioms of ZF set theory (the possible backgrounds allow intuitionistic logic). By tweaking the assumptions on the successor function, they are able to describe other set-theoretic structures; for example, the initial ZF-structure with a monotone successor gives $O$, the class of ordinals, relative to the background.

Now it is well-known that surreal numbers generalize ordinals, or rather that ordinals are special numbers where player R has no options, or in different terms, where there are no numbers past the 'Dedekind cut' which divides L options from R options. In any case, on account of the highly recursive nature of surreal numbers, it is extremely tempting to believe that they too can be described as a recursive type, or as an initial algebraic structure of some sort (in a background category along the lines given by Joyal-Moerdijk, presumably). But what would it be exactly?

I suppose that if I knocked my head against a wall for a while, I might be able to figure it out or at least make a strong guess, but maybe someone else has already worked through the details?

-
 Is there anything useful in Mike Shulman's post golem.ph.utexas.edu/category/2009/11/…? Or this categories mailing list post facultypages.ecc.edu/alsani/ct99-00%288-12%29/…? – David Corfield Apr 29 2011 at 15:57 Hi, David, and thanks! I think you're right that it makes sense to look at games first. Both of those posts look very relevant; do you know whether Cruttwell's notes are written up? – Todd Trimble Apr 29 2011 at 16:39 Hi Todd. It looks like his talk is here pages.cpsc.ucalgary.ca/~gscruttw/…, and there is a paper there too - Combinatorial Game Categories. – David Corfield Apr 30 2011 at 21:04

This is just a bit too long to be a comment. I think that the class of well-founded Conway games is the initial algebra of the functor $X \mapsto P_s(X)\times P_s(X)$, just as the universe of well-founded ZF-sets is the initial algebra of $X\mapsto P_s(X)$. However, not only is this the class of games rather than surreals, it is the class of games up to identity, rather than up to equality (recall that "equality" of games and surreals is a recursively defined notion, somewhat like a bisimulation). I don't think I ever thought of any universal property along these lines that would make the notion of equality drop out automatically. The combinatorial-game-category approach seems like it may deal with that, but I don't know whether and how it is related to the algebraic set theory point of view.

-
 Thanks, Mike; the same thought occurred to me. However, getting back to numbers, I wonder whether one might have more luck dealing with sign expansions of surreals, or perhaps normal forms of surreals, where one can consider equality as identity? – Todd Trimble May 2 2011 at 14:38 Perhaps! It would be nice to have something that would also work for games up to equality, though. – Mike Shulman May 3 2011 at 5:32

Perhaps it would be useful to look at Lionel Mamane's Coq formalisation of surreal numbers, with a paper listed on http://www.cs.ru.nl/~lionelm/research.php (there are also slides at http://types2004.lri.fr/SLIDES/mamane.pdf or look at his homepage at http://www.mamane.lu/concoq/ ).

-
 Yes, some of this indeed looks useful; thanks. – Todd Trimble Jan 31 2012 at 16:21