Surreal Numbers as Inductive Type?

Question

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?

Answer 1

Heh, I just ran across this old question again and realized that I now know an answer: it's in section 11.6 of the HoTT Book. It's written out there as a higher inductive-inductive type; in other language it says roughly that $\mathbf{No}$ is the initial object among classes $X$ equipped with the following.

1. Two binary relations $<$ and $\le$.
2. For any two sub-sets $L,R\subseteq X$ such that $x^L<x^R$ for all $x^L\in L$ and $x^R\in R$, a specified element $x\in X$, written $\{x^L\mid x^R\}$.
3. If $x,y\in X$ satisfy $x\le y$ and $y\le x$, then $x=y$.
4. Given $x = \{x^L\mid x^R\}$ and $y = \{y^L\mid y^R\}$, if every $x^L<y$ and every $x<y^R$, then $x\le y$.
5. Given $x = \{x^L\mid x^R\}$ and $y = \{y^L\mid y^R\}$, if some $x\le y^L$, then $x<y$.
6. Given $x = \{x^L\mid x^R\}$ and $y = \{y^L\mid y^R\}$, if some $x^R\le y$, then $x<y$.

The first innovation is that in place of the single order relation of a ZF-structure, we specify the strict and non-strict order relations as separate data. The second is that we include in the above list of axioms a way to make two surreal numbers equal; categorically this means we consider not initial algebras for an endofunctor, but initial algebras for a presented monad (type-theoretically it corresponds to using higher inductive types rather than ordinary inductive types).

Answer 2

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.

Answer 3

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/ ).