Since their inception in the 1970s, various constructions of the surreal numbers have been discovered. In the classical setting, they were defined as a special class of so-called Games. They were also constructed as expansions of \(\{−, +\}\) of ordinal length. As another example, J. Conway constructed a field isomorphism between the surreals and the field of Hahn Series with real coefficients on the value group of the surreals.

This talk will present a more recent construction, first done in the HoTT book, defining the surreals as a higher-inductive type. The talk is intended for an audience that is not yet familiar with homotopy type theory. Thus, the main part of the talk will be spent introducing the basic concepts of homotopy type theory with the two aims of formalizing first-order logic inside homotopy type theory and defining the surreals as a higher-inductive type.

In the last part, we will look at a consequence of the constructive nature of homotopy type theory, namely that the surreals defined this way fail to be (weakly) totally ordered.