You can combine ZFC and simple type theory to give you something in which you can comfortably do surreal numbers. This is done by embedding ZFC as a simple type

You can combine ZFC and simple type theory to give you something in which you can comfortably do surreal numbers. This is done by embedding ZFC as a simple type. For example, here this is done for Partizan Games (which contain the surreal numbers): http://link.springer.com/chapter/10.1007/11921240_19 http://link.springer.com/chapter/10.1007/11921240_19