What’s the Big Deal About HoTT?

June 22, 2013

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 textsf{Id}_A(M,N) is the type of identifications of M and N within the space A.  Identifications may be thought of as proofs that M and N are equal as elements of $A$, or, equivalently, as paths in the space A between points M and N.  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:

  1. Reflexivity, stating that everything is equal to itself.
  2. Higher inductive types, defining a type by giving its points, paths, paths between paths, and so on to any dimension.
  3. 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 “A iff B” tend to become “Asimeq B“, stating that the proofs of A and the proofs of B 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 A+(Ato textbf{0}) 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.

Update: re-title to conform with other posts.