2.5 The higher groupoid structure of type formers


In http://planetmath.org/node/87533Chapter 1, we introduced many ways to form new types: cartesian products, disjoint unionsMathworldPlanetmath, dependent products, dependent sums, etc. In §2.1 (http://planetmath.org/21typesarehighergroupoids),§2.2 (http://planetmath.org/22functionsarefunctors),§2.3 (http://planetmath.org/23typefamiliesarefibrations), we saw that all types in homotopy type theory behave like spaces or higher groupoidsPlanetmathPlanetmathPlanetmath. Our goal in the rest of the chapter is to make explicit how this higher structureMathworldPlanetmath behaves in the case of the particular types defined in http://planetmath.org/node/87533Chapter 1.

It turns out that for many types A, the equality types x=Ay can be characterized, up to equivalence, in terms of whatever data was used to construct A. For example, if A is a cartesian product B×C, and x(b,c) and y(b,c), then we have an equivalence

((b,c)=(b,c))((b=b)×(c=c)). (2.5.1)

In more traditional languagePlanetmathPlanetmath, two ordered pairsMathworldPlanetmath are equal just when their components are equal (but the equivalence (2.5.1) says rather more than this). The higher structure of the identity types can also be expressed in terms of these equivalences; for instance, concatenating two equalities between pairs corresponds to pairwise concatenationMathworldPlanetmath.

Similarly, when a type family P:A𝒰 is built up fiberwise using the type forming rules from http://planetmath.org/node/87533Chapter 1, the operationMathworldPlanetmath 𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍P(p,) can be characterized, up to homotopyMathworldPlanetmath, in terms of the corresponding operations on the data that went into P. For instance, if P(x)B(x)×C(x), then we have

𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍P(p,(b,c))=(𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍B(p,b),𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍C(p,c)).

Finally, the type forming rules are also functorial, and if a function f is built from this functoriality, then the operations 𝖺𝗉f and 𝖺𝗉𝖽f can be computed based on the corresponding ones on the data going into f. For instance, if g:BB and h:CC and we define f:B×CB×C by f(b,c):(g(b),h(c)), then modulo the equivalence (2.5.1), we can identify 𝖺𝗉f with “(𝖺𝗉g,𝖺𝗉h)”.

The next few sectionsPlanetmathPlanetmathPlanetmathPlanetmath (§2.6 (http://planetmath.org/26cartesianproducttypes) to §2.13 (http://planetmath.org/213naturalnumbers)) will be devoted to stating and proving theorems of this sort for all the basic type forming rules, with one section for each basic type former. Here we encounter a certain apparent deficiency in currently available type theoriesPlanetmathPlanetmath; as will become clear in later chapters, it would seem to be more convenient and intuitive if these characterizations of identity types, transport, and so on were judgmental equalities. However, in the theory presented in http://planetmath.org/node/87533Chapter 1, the identity types are defined uniformly for all types by their inductionMathworldPlanetmath principle, so we cannot “redefine” them to be different things at different types. Thus, the characterizations for particular types to be discussed in this chapter are, for the most part, theorems which we have to discover and prove, if possible.

Actually, the type theory of http://planetmath.org/node/87533Chapter 1 is insufficient to prove the desired theorems for two of the type formers: Π-types and universesPlanetmathPlanetmath. For this reason, we are forced to introduce axioms into our type theory, in order to make those “theorems” true. Type-theoretically, an axiom (c.f. §1.1 (http://planetmath.org/11typetheoryversussettheory)) is an “atomic” element that is declared to inhabit some specified type, without there being any rules governing its behavior other than those pertaining to the type it inhabits.

The axiom for Π-types (§2.9 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom)) is familiar to type theorists: it is called function extensionality, and states (roughly) that if two functions are homotopicMathworldPlanetmath in the sense of §2.4 (http://planetmath.org/24homotopiesandequivalences), then they are equal. The axiom for universes (§2.10 (http://planetmath.org/210universesandtheunivalenceaxiom)), however, is a new contribution of homotopy type theory due to Voevodsky: it is called the univalence axiom, and states (roughly) that if two types are equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath in the sense of §2.4 (http://planetmath.org/24homotopiesandequivalences), then they are equal. We have already remarked on this axiom in the introduction; it will play a very important role in this book.11We have chosen to introduce these principles as axioms, but there are potentially other ways to formulate a type theory in which they hold. See the Notes to this chapter.

It is important to note that not all identity types can be “determined” by induction over the construction of types. Counterexamples include most nontrivial higher inductive types (see http://planetmath.org/node/87579Chapter 6,http://planetmath.org/node/87582Chapter 8). For instance, calculating the identity types of the types 𝕊n (see §6.4 (http://planetmath.org/64circlesandspheres)) is equivalent to calculating the higher homotopy groups of spheres, a deep and important field of research in algebraic topology.

Title 2.5 The higher groupoid structure of type formers
\metatable