Examples of the benefits of Homotopy Type Theory for computer aided proofs?

Solution 1:

Personally, I think the current benefits of HoTT for formalizing previously existing mathematics may be a little oversold. As Ingo says, since existing mathematics is done based on sets, and the sets in HoTT look more or less like any other kind of set, the mathematics therein isn't going to look very different from what you're used to. There are a few benefits, though; e.g. Ingo mentioned HITs as a convenient way to obtain quotients and free structures.

Another thing that HoTT buys you, relative to vanilla type theory, is "proof-irrelevance done right": the "propositions" are the types in which every two elements are equal, so that types built using propositions (like subsets, powersets, quotients, etc.) automatically have the correct equality. The computational behavior of those types also isn't forcibly hidden, so for instance you can define a finite set to be one for which there exists an isomorphic canonical finite set, and then prove theorems about the cardinality of finite sets which actually compute. Moreover, univalence means that equivalent propositions are equal, hence (for instance) one can rewrite from one to the other. This was all originally done by Voevodsky and can be found somewhere in UniMath, and also in the HoTT library. (There is also function extensionality, which is useful for many things, but of course that isn't the exclusive property of HoTT.)

We can also go current benefits for existing mathematics in the two obvious directions. If and when we get a computational interpretation of univalence, then many of us hope that it will greatly simplify the process of moving back and forth between isomorphic structures. (It has a bit of that benefit now, but because it doesn't compute definitionally, it's often more trouble than it's worth.) And Ingo also mentioned the potential for new mathematics such as synthetic homotopy theory, which is much easier to formalize in HoTT than classical set-based homotopy theory would be anywhere.

Solution 2:

I hope that experts will weigh in, but let me try a first stab at an answer.

I believe that, for purposes of computer formalization, there is indeed no great difference between the HoTT treatment of groups and the classical treatment. This is because groups are modeled as structured sets, i.e. 0-types, by definition; to a first approximation, sets in HoTT behave just like the sets of other foundational theories. However, even with algebraic structures modeled on sets, there are some nice new approaches: implementing free structures (free monoids, free groups, ...) as inductive types comes to my mind (see the HoTT book, chapter 6.11). Also, the general benefits of HoTT still apply, of course, for instance that isomorphic groups are rigorously identified.

A place where the HoTT approach really helps computer formalization, is with higher types. The Blakers–Massey theorem in homotopy theory is often cited as an example. This non-trivial theorem was completely formalized in HoTT, while apparently it would be an arduous task to formalize it in classical foundations. One reason for this is that the objects of the Blakers–Massey theorem, homotopy types and homotopy groups, are "built in" to HoTT and do not need complex encodings as sets. (Unfortunately, this theorem is not exactly undergraduate-level.)

You are asking for proofs and definitions which illustrate the power of HoTT. To this end, let me direct you to chapters 6 and 8 of the HoTT book. Chapter 6 contains an astoundingly short definition of the circle – it's the type freely generated by

• a point $\mathsf{base} : S^1$ and
• a path $\mathsf{loop} : (\mathsf{base} = \mathsf{base})$.

Note that this is the complete definition; no real numbers and no explicit mention of a topology is needed. Other important spaces and constructions with spaces have similar short definitions. Moreover, these definitions exactly reflect how one thinks about those spaces from a homotopy-theoretic perspective.

In Chapter 8, the fundamental group of $S^1$ is calculated. The proof doesn't need any prior lemmas from homotopy theory. Instead, it only uses the definitions (and the univalence axiom in a critical way). Accordingly, the proof is easily formalized in Coq+HoTT.