How to read this book

This book is divided into two parts. http://planetmath.org/node/87878Part I, “Foundations”, develops the fundamental concepts of homotopy type theory. This is the mathematical foundation 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 http://planetmath.org/node/87878Part I is fairly extensive.

http://planetmath.org/node/87879Part II, “Mathematics”, consists of four chapters that build on the basic notions of http://planetmath.org/node/87878Part I to exhibit some of the new things we can do with univalent foundations in four different areas of mathematics: homotopy theory (http://planetmath.org/node/87582Chapter 8), category theory (http://planetmath.org/node/87583Chapter 9), set theory (http://planetmath.org/node/87584Chapter 10), and real analysis (http://planetmath.org/node/87585Chapter 11). The chapters in http://planetmath.org/node/87879Part 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 http://planetmath.org/node/87878Part 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 http://planetmath.org/node/87879Part II. Fortunately, not all of http://planetmath.org/node/87878Part I is necessary in order to read the chapters in http://planetmath.org/node/87879Part II. Each chapter in http://planetmath.org/node/87879Part II begins with a brief overview of its subject, what univalent foundations has to contribute to it, and the necessary background from http://planetmath.org/node/87878Part 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 http://planetmath.org/node/87879Part II more deeply than this, but are not ready to read all of http://planetmath.org/node/87878Part I, we provide here a brief summary of http://planetmath.org/node/87878Part I, with remarks about which parts are necessary for which chapters in http://planetmath.org/node/87879Part II.

http://planetmath.org/node/87533Chapter 1 is about the basic notions of type theory, prior to any homotopical interpretation. A reader who is familiar with Martin-Löf type theory 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 http://planetmath.org/node/87533Chapter 1, as there are many subtle differences between type theory and other foundations such as set theory.

http://planetmath.org/node/87569Chapter 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 http://planetmath.org/node/87533Chapter 1. It also introduces the univalence axiom (§2.10 (http://planetmath.org/210universesandtheunivalenceaxiom)) — 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 (http://planetmath.org/21typesarehighergroupoids) to §2.4 (http://planetmath.org/24homotopiesandequivalences).

http://planetmath.org/node/87576Chapter 3 describes how we represent logic in homotopy type theory, and its connection to classical logic as well as to constructive and intuitionistic logic. Here we define the law of excluded middle, the axiom of choice, 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 http://planetmath.org/node/87584Chapter 10,http://planetmath.org/node/87585Chapter 11, less important for http://planetmath.org/node/87583Chapter 9, and not so necessary for http://planetmath.org/node/87582Chapter 8.

http://planetmath.org/node/87577Chapter 4,http://planetmath.org/node/87578Chapter 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 http://planetmath.org/node/87879Part II. Only a few lemmas from http://planetmath.org/node/87577Chapter 4 are used here and there, while the general discussions in §5.1 (http://planetmath.org/51introductiontoinductivetypes),§5.6 (http://planetmath.org/56thegeneralsyntaxofinductivedefinitions),§5.7 (http://planetmath.org/57generalizationsofinductivetypes) are helpful for providing the intuition required for http://planetmath.org/node/87579Chapter 6. The generalized sorts of inductive definition discussed in §5.7 (http://planetmath.org/57generalizationsofinductivetypes) are also used in a few places in http://planetmath.org/node/87584Chapter 10,http://planetmath.org/node/87585Chapter 11.

http://planetmath.org/node/87579Chapter 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 http://planetmath.org/node/87582Chapter 8, and some particular ones play important roles in http://planetmath.org/node/87584Chapter 10,http://planetmath.org/node/87585Chapter 11. They are not so necessary for http://planetmath.org/node/87583Chapter 9, although one example is used in §9.9 (http://planetmath.org/99therezkcompletion).

Finally, http://planetmath.org/node/87580Chapter 7 discusses homotopy $n$-types and related notions such as $n$-connected types. These notions are important for http://planetmath.org/node/87582Chapter 8, but not so important in the rest of http://planetmath.org/node/87879Part II, although the case $n=-1$ of some of the lemmas are used in §10.1 (http://planetmath.org/101thecategoryofsets).

This completes http://planetmath.org/node/87878Part I. As mentioned above, http://planetmath.org/node/87879Part II consists of four largely unrelated chapters, each describing what univalent foundations has to offer to a particular subject.

Of the chapters in http://planetmath.org/node/87879Part II, http://planetmath.org/node/87582Chapter 8 (Homotopy theory) is perhaps the most radical. Univalent foundations has a very different “synthetic” approach to homotopy theory in which homotopy types are the basic objects (namely, the types) rather than being constructed using topological spaces or some other set-theoretic model. This enables new styles of proof for classical theorems in algebraic topology, of which we present a sampling, from ${\pi }_1({𝕊}^1)=\mathbb{Z}$ to the Freudenthal suspension theorem.

In http://planetmath.org/node/87583Chapter 9 (Category theory), we develop some basic (1-)category theory, adhering to the principle of the univalence axiom that equality is isomorphism. This has the pleasant effect of ensuring that all definitions and constructions are automatically invariant under equivalence of categories: indeed, equivalent categories are equal just as equivalent types are equal. (It also has connections to higher category theory and higher topos theory.)

http://planetmath.org/node/87584Chapter 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 numbers a bit more pleasant, and that higher inductive types yield a cumulative hierarchy satisfying the usual axioms of Zermelo–Fraenkel set theory.

In http://planetmath.org/node/87585Chapter 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 numbers.

Each chapter in this book ends with a Notes section, 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 sequence 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.

Title	How to read this book