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 unions, 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 groupoids. Our goal in the rest of the chapter is to make explicit how this higher structure 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{=}_{A}y$ 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\times C$, and $x\equiv (b,c)$ and $y\equiv (b^{\prime },c^{\prime })$, then we have an equivalence

$$((b,c)=(b^{\prime },c^{\prime }))\simeq ((b=b^{\prime })\times (c=c^{\prime })).$$ (2.5.1)

In more traditional language, two ordered pairs 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 concatenation.

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

$${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^P(p,(b,c))=({\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^B(p,b),{\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^C(p,c)).$$

Finally, the type forming rules are also functorial, and if a function $f$ is built from this functoriality, then the operations ${\mathrm{𝖺𝗉}}_f$ and ${\mathrm{𝖺𝗉𝖽}}_f$ can be computed based on the corresponding ones on the data going into $f$. For instance, if $g:B\to B^{\prime }$ and $h:C\to C^{\prime }$ and we define $f:B\times C\to B^{\prime }\times C^{\prime }$ by $f(b,c):\equiv (g(b),h(c))$, then modulo the equivalence (2.5.1), we can identify ${\mathrm{𝖺𝗉}}_f$ with “$({\mathrm{𝖺𝗉}}_g,{\mathrm{𝖺𝗉}}_h)$”.

The next few sections (§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 theories; 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 induction 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: $\mathrm{\Pi }$-types and universes. 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 $\mathrm{\Pi }$-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 homotopic 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 equivalent 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.

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