How to read this book

This book is divided into two parts. I, “Foundations”, develops the fundamental concepts of homotopy type theory. This is the mathematical foundationPlanetmathPlanetmath on which the development of specific subjects is built, and which is required for the understanding of the univalent foundations approach. To a programmer, this is “library code”. Since univalent foundations is a new and different kind of mathematics, its basic notions take some getting used to; thus I is fairly extensive. II, “Mathematics”, consists of four chapters that build on the basic notions of I to exhibit some of the new things we can do with univalent foundations in four different areas of mathematics: homotopy theory ( 8), category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath ( 9), set theoryMathworldPlanetmath ( 10), and real analysis ( 11). The chapters in II are more or less independent of each other, although occasionally one will use a lemma proven in another.

A reader who wants to seriously understand univalent foundations, and be able to work in it, will eventually have to read and understand most of I. However, a reader who just wants to get a taste of univalent foundations and what it can do may understandably balk at having to work through over 200 pages before getting to the “meat” in II. Fortunately, not all of I is necessary in order to read the chapters in II. Each chapter in II begins with a brief overview of its subject, what univalent foundations has to contribute to it, and the necessary background from I, so the courageous reader can turn immediately to the appropriate chapter for their favorite subject. For those who want to understand one or more chapters in II more deeply than this, but are not ready to read all of I, we provide here a brief summary of I, with remarks about which parts are necessary for which chapters in II. 1 is about the basic notions of type theory, prior to any homotopical interpretationMathworldPlanetmathPlanetmath. A reader who is familiar with Martin-Löf type theoryPlanetmathPlanetmath can quickly skim it to pick up the particulars of the theory we are using. However, readers without experience in type theory will need to read 1, as there are many subtle differencesPlanetmathPlanetmath between type theory and other foundations such as set theory. 2 introduces the homotopical viewpoint on type theory, along with the basic notions supporting this view, and describes the homotopical behavior of each component of the type theory from 1. It also introduces the univalence axiom (§2.10 ( — the first of the two basic innovations of homotopy type theory. Thus, it is quite basic and we encourage everyone to read it, especially §2.1 ( to §2.4 ( 3 describes how we represent logic in homotopy type theory, and its connection to classical logic as well as to constructive and intuitionistic logicMathworldPlanetmath. Here we define the law of excluded middleMathworldPlanetmathPlanetmath, the axiom of choiceMathworldPlanetmath, and the axiom of propositional resizing (although, for the most part, we do not need to assume any of these in the rest of the book), as well as the propositional truncation which is essential for representing traditional logic. This chapter is essential background for 10, 11, less important for 9, and not so necessary for 8. 4, 5 study two special topics in detail: equivalences (and related notions) and generalized inductive definitions. While these are important subjects in their own rights and provide a deeper understanding of homotopy type theory, for the most part they are not necessary for II. Only a few lemmas from 4 are used here and there, while the general discussions in §5.1 (,§5.6 (,§5.7 ( are helpful for providing the intuition required for 6. The generalized sorts of inductive definition discussed in §5.7 ( are also used in a few places in 10, 11. 6 introduces the second basic innovation of homotopy type theory — higher inductive types — with many examples. Higher inductive types are the primary object of study in 8, and some particular ones play important roles in 10, 11. They are not so necessary for 9, although one example is used in §9.9 (

Finally, 7 discusses homotopyMathworldPlanetmath n-types and related notions such as n-connected types. These notions are important for 8, but not so important in the rest of II, although the case n=-1 of some of the lemmas are used in §10.1 (

This completesPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath I. As mentioned above, II consists of four largely unrelated chapters, each describing what univalent foundations has to offer to a particular subject.

Of the chapters in II, 8 (Homotopy theory) is perhaps the most radicalPlanetmathPlanetmathPlanetmath. Univalent foundations has a very different “synthetic” approach to homotopy theory in which homotopy typesMathworldPlanetmath are the basic objects (namely, the types) rather than being constructed using topological spacesMathworldPlanetmath or some other set-theoretic model. This enables new styles of proof for classical theoremsMathworldPlanetmath in algebraic topology, of which we present a sampling, from π1(𝕊1)= to the Freudenthal suspension theorem.

In 9 (Category theory), we develop some basic (1-)category theory, adhering to the principle of the univalence axiom that equality is isomorphismMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath. This has the pleasant effect of ensuring that all definitions and constructions are automatically invariant under equivalence of categories: indeed, equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath categoriesMathworldPlanetmath are equal just as equivalent types are equal. (It also has connections to higher category theory and higher topos theory.) 10 (Set theory) studies sets in univalent foundations. The category of sets has its usual properties, hence provides a foundation for any mathematics that doesn’t need homotopical or higher-categorical structures. We also observe that univalence makes cardinal and ordinal numbersMathworldPlanetmath a bit more pleasant, and that higher inductive types yield a cumulative hierarchy satisfying the usual axioms of Zermelo–Fraenkel set theory.

In 11 (Real numbers), we summarize the construction of Dedekind real numbers, and then observe that higher inductive types allow a definition of Cauchy real numbers that avoids some associated problems in constructive mathematics. Then we sketch a similar approach to Conway’s surreal numbersMathworldPlanetmath.

Each chapter in this book ends with a Notes sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, which collects historical comments, references to the literature, and attributions of results, to the extent possible. We have also included Exercises at the end of each chapter, to assist the reader in gaining familiarity with doing mathematics in univalent foundations.

Finally, recall that this book was written as a massively collaborative effort by a large number of people. We have done our best to achieve consistency in terminology and notation, and to put the mathematics in a linear sequencePlanetmathPlanetmath that flows logically, but it is very likely that some imperfections remain. We ask the reader’s forgiveness for any such infelicities, and welcome suggestions for improvement of the next edition.


  • 1
Title How to read this book