Now that the Homotopy Type Theory book is out, a lot of people are asking “What’s the big deal?”. The full answer lies within the book itself (or, at any rate, the fullest answer to date), but I am sure that many of us who were involved in its creation will be fielding this question in our own ways to help explain why we are so excited by it. In fact what I think is really fascinating about HoTT is precisely that there are so many different ways to think about it, according to one’s interests and backgrounds. For example, one might say it’s a nice way to phrase arguments in homotopy theory that avoids some of the technicalities in the classical proofs by treating spaces and paths synthetically, rather than analytically. Or one might say that it’s a good language for mechanization of mathematics that provides for the concise formulation of proofs in a form that can be verified by a computer. Or one might say that it points the way towards a vast extension of the concept of computation that enables us to compute with abstract geometric objects such as spheres or toruses. Or one might say that it’s a new foundation for mathematics that subsumes set theory by generalizing types from mere sets to arbitrary infinity groupoids, sets being but particularly simple types (those with no non-trivial higher-dimensional structure).

But what is it about HoTT that makes all these interpretations and applications possible? What is the key idea that separates HoTT from other approaches that seek to achieve similar ends? What makes HoTT so special?

In a word the answer is *constructivity.* The distinctive feature of HoTT is that it is based on Per Martin-Löf’s Intuitionistic Theory of Types, which was formulated as a foundation for *intuitionistic mathematics* as originally put forth by Brouwer in the 1930′s, and further developed by Bishop, Gentzen, Heyting, Kolmogorov, Kleene, Lawvere, and Scott, among many others. Briefly put, the idea of type theory is to codify and systematize the concept of a *mathematical construction* by characterizing the abstract properties, rather than the concrete realizations, of the objects used in everyday mathematics. Brouwer’s key insight, which lies at the heart of HoTT, is that *proofs are a form of construction* no different in kind or character from numbers, geometric figures, spaces, mappings, groups, algebras, or any other mathematical structure. Brouwer’s dictum, which distinguished his approach from competing alternatives, is that *logic is a part of mathematics*, rather than *mathematics is an application of logic*. Because for him the concept of a construction, including the concept of a proof, is prior to any other form of mathematical activity, including the study of proofs themselves (*i.e.*, logic).

So under Martin-Löf’s influence HoTT starts with the notion of *type* as a classification of the notion of *construction*, and builds upwards from that foundation. Unlike competing approaches to foundations, *proofs are mathematical objects* that play a central role in the theory. This conception is *central* to the homotopy-theoretic interpretation of type theory, which enriches types to encompass spaces with higher-dimensional structure. Specifically, the type is the type of *identifications* of and within the space . Identifications may be thought of as *proofs* that and are *equal* as elements of $A$, or, equivalently, as *paths* in the space between points and . The fundamental principles of abstraction at the heart of type theory ensure that *all constructs of the theory respect these identifications*, so that we may treat them as proofs of equality of two elements. There are three main sources of identifications in HoTT:

- Reflexivity, stating that everything is equal to itself.
- Higher inductive types, defining a type by giving its points, paths, paths between paths, and so on to any dimension.
- Univalence, which states that an equivalence between types determines a path between them.

I will not attempt here to explain each of these in any detail; everything you need to know is in the HoTT book. But I will say a few things about their consequences, just to give a flavor of what these new principles give us.

Perhaps the most important conceptual point is that mathematics in HoTT emphasizes the *structure of proofs* rather than their mere existence. Rather than settle for a mere logical equivalence between two types (mappings back and forth stating that each implies the other), one instead tends to examine the *entire space* of proofs of a proposition and how it relates to others. For example, the univalence axiom itself does not merely state that every equivalence between types gives rise to a path between them, but rather that there is an *equivalence* between the type of equivalences between two types and the type of paths between them. Familiar patterns such as “ iff ” tend to become ““, stating that the proofs of and the proofs of are equivalent. Of course one may *choose *neglect this additional information, stating only weaker forms of it using, say, truncation to suppress higher-dimensional information in a type, but the tendency is to *embrace* the structure and characterize the space of proofs as fully as possible.

A close second in importance is the *axiomatic freedom* afforded by constructive foundations. This point has been made many times by many authors in many different settings, but has particular bite in HoTT. The theory does not commit to (nor does it refute) the infamous *Law of the Excluded Middle* for arbitrary types: the type need not always be inhabited. This property of HoTT is absolutely essential to its expressive power. Not only does it admit a wider range of interpretations than are possible with the Law included, but it also allows for the *selective imposition* of the Law where it is needed to recover a classical argument, or where it is important to distinguish the implications of decidability in a given situation. (Here again I defer to the book itself for full details.) Similar considerations arise in connection with the many forms of Choice that can be expressed in HoTT, some of which are outright provable, others of which are independent as they are in axiomatic set theory.

Thus, what makes HoTT so special is that it is a* constructive* theory of mathematics. Historically, this has meant that it has a *computational* interpretation, expressed most vividly by the *propositions as types* principle. And yet, for all of its promise, what HoTT currently lacks is a computational interpretation! What, exactly, does it mean to *compute* with higher-dimensional objects? At the moment it is difficult to say for sure, though there seem to be clear intuitions in at least some cases of how to “implement” such a rich type theory. Alternatively, one may ask whether the term “constructive”, when construed in such a general setting, must inevitably involve a notion of computation. While it seems obvious on computational grounds that the Law of the Excluded Middle should not be considered universally valid, it becomes less clear why it is so important to omit this Law (and, essentially, no other) in order to obtain the richness of HoTT when no computational interpretation is extant. From my point of view understanding the *computational *meaning of higher-dimensional type theory is of paramount importance, because, for me, type theory is and always has been a *theory of computation* on which the entire edifice of mathematics ought to be built.

I see.

I’m not so sure that ‘Gödel numbering’ entails any such presupposition though. That is more of a consequence of a [desirable] property of the numbering system which Gödel designed the system to have (so that his ‘Incompleteness’ proofs could follow) [which was only possible because of certain properties of prime numbers]. And, even if GN did include such a presupposition it seems theoretically possible to construct a similar numbering system without such.

Also, if you could briefly provide more details about the nuance between Brouwer et al & Hilbert’s (and later Gödel’s) codification that would be great. [Of course, 'read the book' is an acceptable answer if this topic is touched on in the book]. :-)

Thanks and regards!

[Also, apologies if this message starts a new thread. I could see no way to reply to the existing thread without creating a wordpress account].

I’ll try to get to this soon, after I return from a conference.

‘Brouwer’s key insight’ sounds an awful lot like ‘Gödel numbering’ as theorems are just ‘well formed formulae’.

No, it’s not at all related to Goedel-numbering, because there is no presupposition of an enumeration of all possible proofs (nor can there be). The constructive viewpoint is a bit more subtle than that, and is not reducible to thinking about formal derivations as syntactic objects.