Chapter 2 notes

The definition of identity types, with their induction principle, is due to Martin-Löf [12]. As mentioned in the notes to http://planetmath.org/node/87533Chapter 1, our identity types are those that belong to intensional type theory, by contrast with those of extensional type theory which have an additional “reflection rule” saying that if $p:x=y$, then in fact $x\equiv y$. This reflection rule implies that all the higher groupoid structure collapses (see http://planetmath.org/node/87645Exercise 2.14), so for nontrivial homotopy we must use the intensional version. One may argue, however, that homotopy type theory is in another sense more “extensional” than traditional extensional type theory, because of the function extensionality and univalence axioms.

The proofs of symmetry (inversion) and transitivity (concatenation) for equalities are well-known in type theory. The fact that these make each type into a 1-groupoid (up to homotopy) was exploited in [7] to give the first “homotopy” style semantics for type theory.

The actual homotopical interpretation, with identity types as path spaces, and type families as fibrations, is due to [2], who used the formalism of Quillen model categories. An interpretation in (strict) $\mathrm{\infty }$-groupoids was also given in the thesis [13]. For a construction of all the higher operations and coherences of an $\mathrm{\infty }$-groupoid in type theory, see [14] and [3].

Operations such as ${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^P(p,\text{–})$ and ${\mathrm{𝖺𝗉}}_f$, and one good notion of equivalence, were first studied extensively in type theory by Voevodsky, using the proof assistant Coq. Subsequently, many other equivalent definitions of equivalence have been found, which are compared in http://planetmath.org/node/87577Chapter 4.

The “computational” interpretation of identity types, transport, and so on described in §2.5 (http://planetmath.org/25thehighergroupoidstructureoftypeformers) has been emphasized by [10]. They also described a “1-truncated” type theory (see http://planetmath.org/node/87580Chapter 7) in which these rules are judgmental equalities. The possibility of extending this to the full untruncated theory is a subject of current research.

The naive form of function extensionality which says that “if two functions are pointwise equal, then they are equal” is a common axiom in type theory, going all the way back to [15]. Some stronger forms of function extensionality were considered in [5]. The version we have used, which identifies the identity types of function types up to equivalence, was first studied by Voevodsky, who also proved that it is implied by the naive version (and by univalence; see §4.9 (http://planetmath.org/49univalenceimpliesfunctionextensionality)).

The univalence axiom is also due to Voevodsky. It was originally motivated by semantic considerations; see [8].

In the type theory we are using in this book, function extensionality and univalence have to be assumed as axioms, i.e. elements asserted to belong to some type but not constructed according to the rules for that type. While serviceable, this has a few drawbacks. For instance, type theory is formally better-behaved if we can base it entirely on rules rather than asserting axioms. It is also sometimes inconvenient that the theorems of §2.6 (http://planetmath.org/26cartesianproducttypes) to §2.13 (http://planetmath.org/213naturalnumbers) are only propositional equalities (paths) or equivalences, since then we must explicitly mention whenever we pass back and forth across them. One direction of current research in homotopy type theory is to describe a type system in which these rules are judgmental equalities, solving both of these problems at once. So far this has only been done in some simple cases, although preliminary results such as [10] are promising. There are also other potential ways to introduce univalence and function extensionality into a type theory, such as having a sufficiently powerful notion of “higher quotients” or “higher inductive-recursive types”.

The simple conclusions in §2.12 (http://planetmath.org/212coproducts) to §2.13 (http://planetmath.org/213naturalnumbers) such as “$\mathrm{𝗂𝗇𝗅}$ and $\mathrm{𝗂𝗇𝗋}$ are injective and disjoint” are well-known in type theory, and the construction of the function $\mathrm{𝖾𝗇𝖼𝗈𝖽𝖾}$ is the usual way to prove them. The more refined approach we have described, which characterizes the entire identity type of a positive type (up to equivalence), is a more recent development; see e.g. [11].

The type-theoretic axiom of choice (2.15.6) (http://planetmath.org/215universalproperties#S0.E4) was noticed in William Howard’s original paper [6] on the propositions-as-types correspondence, and was studied further by Martin-Löf with the introduction of his dependent type theory. It is mentioned as a “distributivity law” in Bourbaki’s set theory [4].

For a more comprehensive (and formalized) discussion of pullbacks and more general homotopy limits in homotopy type theory, see [1]. Limits of diagrams over directed graphs are the easiest general sort of limit to formalize; the problem with diagrams over categories (or more generally $(\mathrm{\infty },1)$-categories) is that in general, infinitely many coherence conditions are involved in the notion of (homotopy coherent) diagram. Resolving this problem is an important open question in homotopy type theory.

Title	Chapter 2 notes