×
The Univalent Foundations Program

Homotopy type theory. Univalent foundations of mathematics. (English) Zbl 1298.03002

Princeton, NJ: Institute for Advanced Study; Raleigh, NC: Lulu Press. ix, 468 p. (2013).
The book is the outcome of the special year on homotopy type theory (HoTT) held at the Institute of Advanced Study, Princeton. HoTT is presented as a foundation for mathematics, intended both as a formal theory able to describe mathematics as a whole, and as a new paradigm to conceive and study mathematical ideas. So, the first part of the book is a comprehensive introduction of all the foundational aspects of HoTT, while the second part describes a number of applications developed so far, all of them related, in different ways, to the foundational aim.
An important aspect is that the book introduces the theory along with the style of HoTT, resulting in a text that is rigorous but not strictly formal: although a mathematician can easily fill the gaps, it requires some effort to get used to the way of reasoning behind HoTT.
Another difficulty in the book is the required background: despite the efforts of the authors, it is not self-contained. Understanding the content requires some previous knowledge of, at least, dependent type theory, the basics of higher category theory, a few but solid notions of homotopy theory, and some acquaintance with constructive mathematics. In addition, HoTT is still under development, so the text should be read considering the content as a snapshot of the current knowledge of the subject, whose form is almost, but not completely, stable.
On the other hand, HoTT incorporates many ideas from very different fields, the glue being Voevodsky’s recently discovered connection between homotopy theory and type theory. The book tries to provide a systematic exposition of the subject. The general impression is that it succeeds in this goal: the book is fairly complete and it conveys a good picture of what HoTT really is.
As a type theory, HoTT descends from the intensional version of Martin-Löf type theory, extended with universes and a couple of principles: path induction and univalence. Thus, HoTT inherits the propositions-as-types interpretation, yielding an internal logic that is, essentially, intuitionistic in nature. On the other hand, the presence of equality types, i.e., types of the form \(a = b\) for \(a\), \(b\) terms of the same type \(C\), is rendered in a different way than in Martin-Löf type theory: in the latter theory, under the propositions-as-types interpretation, a term \(t: a = b\) is a ‘proof’ of the equality; in HoTT, \(t\) is both a witness of the truth of \(a = b\) and a path from \(a\) to \(b\) in the space \(C\). In fact, the first fundamental idea in HoTT is that any term \(t: A\) is a point in the space denoted by \(A\). The type constructors allow to form product spaces, co-product spaces, function spaces, and the dependent nature of the type theory allows to identify fibrations and sections. So, \(t: a = b\) becomes a map between ‘proofs’, i.e., points, thus a path, and so the type \(a = b\) denotes the space of paths from \(a\) to \(b\).
Chapter 1 introduces HoTT as a type theory, and emphasises the spatial interpretation sketched above. The last sections are devoted to introduce path induction, which is a fundamental feature of HoTT. In short, it states that the family of identity types is freely generated by the elements of the form \(\mathsf{refl}_x: x = x\), \(\mathsf{refl}_x\) being the term for reflexivity. In the spatial interpretation, (based) path induction expresses the fact that the space of paths from some given point is contractible to the constant loop on that point. It is clear that homotopies play a crucial role in the spatial interpretation, since they are the natural way to relate paths: hence, the name of the theory.
The second chapter introduces the central new idea of HoTT: types can be regarded as spaces in homotopy theory, or \(\infty\)-groupoids in category theory. In fact, the abstract description of HoTT in terms of \(\infty\)-groupoids is the precise and formal rendering of the rather intuitive spatial interpretation. The core idea is simple: a groupoid is a category whose arrows are all isomorphisms. But isomorphism is a concept too strict to compare paths, since we need to identify paths that may be continuously transformed one into another. Thus, relaxing the groupoid structure by allowing arrows between arrows, called \(2\)-arrows, and requiring them to be all isomorphisms, we get a categorical structure which is more apt to model the spatial interpretation. Nevertheless, homotopies are paths between paths, so comparing them raises the same problem: we really want to identify homotopies we can continuously transform one into another. So, iterating the abstraction process, we get \(k\)-arrows for each \(k\), where objects are \(0\)-arrows and every \(k\)-arrow is an isomorphism up to \((k + 1)\)-arrows, i.e., up to homotopies. This categorical structure is called \(\infty\)-groupoid.
Chapter 2 precisely illustrates the correspondence between types and spaces, and the identity types arising from their terms are described in detail. Although technically involved, the types are naturally characterised as \(\infty\)-groupoids in the way one may expect. In fact, there is one single point where HoTT is unsatisfactory and an additional ingredient is required: universes do not behave naturally, in the sense that, for any \(A, B:\mathcal{U}\) types in the universe \(\mathcal{U}\), there is a function \(A =_{\mathcal{U}} B \to A \simeq B\) mapping paths from \(A\) to \(B\) in the space \(\mathcal{U}\) into equivalences; unfortunately, the converse does not hold, so an additional axiom is needed, which states exactly the existence of a converse. This is Voevodsky’s univalence axiom.
It is clear that the foundation laid down so far is very distant from the reality of the working mathematician. Nevertheless, it provides enough power to reconstruct in a simple and effective way the world of set-theoretic mathematics and of classical logic. This is obtained in Chapter 3 by defining sets as those types \(A\) for which, for \(x, y: A\) and all \(p,q: x = y\), it holds that \(p = q\). The meaning of this definition is that a set is a type which has no higher homotopy information in it. The notion of set can be easily generalised admitting just a few levels of homotopy information: this allows to construct groupoids, for example. In the opposite way, it is possible to further limit the amount of homotopy information: a type \(P\) is a mere proposition if, for all \(x,y: P\), \(x = y\). The interesting fact is that mere propositions behave classically with respect to type constructors. And each type can be transformed into a mere proposition by flattening in an appropriate way the propositions-as-types interpretation. Interestingly, the latter can be extended one step down, below mere propositions: a type \(A\) is contractible if there is \(a: A\) such that \(a = x\) for all \(x: A\). Or, in topological terms, the type can be continuously reduced to a single point.
Actually, introducing sets, mere propositions, and contractible types has an internal motivation in HoTT: since each type carries a higher homotopy structure with itself, when this structure is non-trivial, it matters. This is particularly relevant in the case of equivalence of types. In fact, the obvious way of defining equivalences as quasi-inverses is unsatisfactory, because the predicate saying that \(f\) is a quasi-inverse, is not a mere proposition. Chapter 4 provides an analysis of this problem and a number of solutions. The key point here is that it matters which \(g\) is quasi-inverse to \(f\), while it should not when the purpose is to say that \(f\) is an equivalence: a type for equivalences which is a mere proposition ensures that the information about \(f\) being an equivalence is all contained in \(f\). However, although logically equivalent to quasi-inverses, there are other definitions of equivalence (half adjoint equivalence, bi-invertible maps, contractible maps) that form mere propositions. One consequence of these alternative definitions is that univalence implies function extensionality.
Chapter 5 discusses inductive types. The standard approach of type theory, that uses W-types providing both induction principles and recursion rules to perform actual computations, is still valid in HoTT, but a new possibility arises: homotopy inductive types, where all computation rules are stated up to a path. The novelty in this chapter is that identity types may be considered as inductive, their induction principle being exactly path induction.
Inductive types are just the simplest types one can generate in HoTT: their constructors generate points. But it is possible to conceive higher inductive definitions, where points are generated together with the paths between them, or even higher homotopy structure. For example, the type \(\mathbb{S}^1\) representing the \(1\)-sphere is generated by a base point \(b:\mathbb{S}^1\) and a loop \(l: b = b\). Higher inductive types are the subject of Chapter 6. The interval, suspensions, circles and spheres, cell complexes and other topological objects are defined following the general schema of higher induction. Interestingly, many of these types can be expressed as homotopy pushouts, showing that higher inductive types are an inner by-product of the categorical presentation of HoTT. This is confirmed by the fact that truncation, the basic operation to flatten any type into a mere proposition, is, in fact, a higher inductive definition. In turn, a generalised version of truncation yields quotients. Applying these constructions to algebra, it becomes evident that the constructive version of the usual algebraic theories can be fully reconstructed inside HoTT. Thus, higher inductive types provide a significant strengthening of constructive set theory. Combining higher inductive types with univalence yields many amazing results: the first is the ‘flattening lemma’. Given a type \(X\) in the universe \(\mathcal{U}\) and an equivalence \(e: X \simeq X\), a type family \(P: \mathbb{S}^1 \to \mathcal{U}\) can be defined by mapping the base point to \(X\) and the loop to, essentially, \(e\). Thus, the flattening lemma says that the space \(\sum_{x:\mathbb{S}^1}P(x)\) is equivalent to a flattened higher inductive type whose constructors may be deduced from those of \(\mathbb{S}^1\) and the definition of \(P\). It holds for general inductive types other than \(\mathbb{S}^1\), too.
The foundational presentation of HoTT concludes in Chapter 7, where \(n\)-types, i.e., spaces containing no interesting homotopy structure above dimension \(n\), are precisely defined and analysed, together with their dual notion, \(n\)-connected spaces, i.e., spaces containing no significant homotopy structure below dimension \(n\). By extending these notions to maps, that is, by requiring the property to hold for all fibers in the map, an orthogonal factorisation system appears: every map factors uniquely as an \(n\)-connected map followed by an \(n\)-truncated one. When \(n = -1\), this reduces to say that each map between sets can be factored into a surjection followed by an injection. An even more general result can be achieved by using modalities.
Not surprisingly, the first application of HoTT is homotopy theory (Chapter 8), intended as a branch of algebraic topology. HoTT allows to undertake a synthetic approach since spaces, points, paths and homotopies are basic notions. The authors claim that HoTT provides many advantages to the study of homotopy theory: the approach is both concrete and abstract, naturally combining the fundamental topological notions with the abstract theory of \(\infty\)-groupoids; new, type-theoretic methods become available, like path induction and the universal properties of higher inductive types; the theorems and their proofs are very amenable to computer formalisation and checking.
These claims are supported by an extensive series of results: the calculation of some homotopy groups of spheres, namely \(\pi_k(\mathbb{S}^1)\), \(\pi_k(\mathbb{S}^n)\) for \(k < n\), \(\pi_2(\mathbb{S}^2)\), and \(\pi_3(\mathbb{S}^2)\) by Hopf fibration and long-exact sequences, and \(\pi_n(\mathbb{S}^n)\) by the Freudenthal suspension theorem; the van Kampen theorem and the status of Whitehead’s principle; the Blakers-Massey theorem; a construction of Eilenberg-Mac Lane spaces; the calculation of \(\pi_{n + 1}(\mathbb{S}^n)\) for \(n \geq 3\).
The second application of HoTT is category theory, as illustrated in Chapter 9. The idea is to define a precategory as a type \(A_0\) for objects and, for each \(x, y: A_0\), a type \(\mathsf{hom}_A(x,y)\) along with identities and composition obeying the usual constraints. By imposing \(\mathsf{hom}_A(x,y)\) to be a set, in the technical sense of HoTT, the attention is restricted to \(1\)-categories; by requiring \(A_0\) to be a set, too, the notion of strict category is enforced; finally, by identifying the type \(x =_{A_0} y\) with the type of isomorphisms from \(x\) to \(y\) in a precategory, the type-theoretic version of a usual category is constructed. It is worth noticing how the condition for a precategory to be a category is an instance of a generalised univalence principle.
The chapter illustrates how these notions can be used to construct category theory inside HoTT: functors, natural transformations, adjunctions and equivalences are defined and analysed; the Yoneda lemma is shown to hold; finally, the so-called Rezk completion is presented, which provides a universal way to replace a precategory with a category – the Rezk completion corresponds to the stack completion in higher topos models.
Chapter 10 illustrates how set theory in rendered inside HoTT. As already said, a set is a type with no homotopy structure besides points: sets in some fixed universe form a category, in the HoTT sense, whose arrows are the maps between them. Actually, such a category is a \(\Pi W\)-pretopos, the predicative notion of topos; assuming propositional resizing, it becomes an elementary topos; furthermore, assuming the axiom of choice and the law of excluded middle, it becomes a model of Lawvere’s elementary theory of the category of sets, thus ensuring that the sets in HoTT behave like sets as used by most mathematicians.
In the category of sets, the book introduces cardinals and ordinals, constructing them out of univalence rather than using a global membership relation. It turns out that, assuming the axiom of choice and excluded middle, cardinals and ordinals are equivalent to their classical counterparts, but equipped with a more ‘structural’ view.
Finally, a cumulative hierarchy of all sets in a given universe is constructed as a higher inductive type in such a way that the hierarchy is again a set in a larger universe, and such that a global membership relation is present for all the sets in the smaller universe, which satisfies the usual laws of set theory.
The final chapter of the book defines real numbers inside HoTT. In the tradition of constructive mathematics, real numbers are formalised either by completion of Cauchy sequences, or by requiring closure under Dedekind cuts. In HoTT, being part of this tradition, both possibilities are available: in fact, the chapter shows how to perform both constructions in HoTT. Of particular interest is the construction of Cauchy reals since they are defined as a higher inductive type, which requires neither power sets nor countable choice.
In HoTT, the Dedekind reals are characterised as the final Archimedean ordered field, while the Cauchy reals are the initial Cauchy-complete Archimedean ordered field. Comparing the two constructions of reals, it follows that the Cauchy reals are included in the Dedekind reals, and they coincide if excluded middle or countable choice holds.
Not assuming excluded middle or the axiom of choice (or variants), the theory of real numbers in HoTT is computationally significant. In this framework, the compactness of the interval \([0,1]\) is analysed: it is shown that \([0,1]\) is metrically compact; but the Bolzano-Weierstrass property that every sequence has a convergent subsequence requires the limited principle of omniscience, i.e., an instance of excluded middle; the naive Heine-Borel compactness does not hold, but a proof-relevant notion of inductive cover does. The chapter closes with the construction of Conway’s surreal numbers as a higher inductive type.
As the reader may see from the above summary of the main novelties in the book, HoTT is a rich foundational theory, and a refined instrument to study mathematics. The amount of new ideas in the book and the consequent revisiting of well-known results from a different point of view suggest that the book would eventually become a reference for those interested in this approach.
As a curiosity, it is remarkable that the publication has been done with Lulu press, a self-publishing system, outside the usual circuits of scholarly publications: probably to make the book available to most readers at no cost for the electronic edition, and at an affordable cost for the printed one.

MSC:

03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations
55-02 Research exposition (monographs, survey articles) pertaining to algebraic topology
03B15 Higher-order logic; type theory (MSC2010)
03G30 Categorical logic, topoi
18A15 Foundations, relations to logic and deductive systems
18B05 Categories of sets, characterizations
55U40 Topological categories, foundations of homotopy theory
PDFBibTeX XMLCite
Full Text: arXiv Link