14
votes
2answers
803 views

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