Chapter 1 notes

The type theory presented here is a version of Martin-Löf’s intuitionistic type theory [14],[16],[18],[20], which itself is based on and influenced by the foundational work of Brouwer [1], Heyting [8], Scott [scott70], de Bruijn [7], Howard [10], Tait [26],[28], and Lawvere [11]. Three principal variants of Martin-Löf’s type theory underlie the NuPRL [3], Coq [5], and Agda [23] computer implementations of type theory. The theory given here differs from these formulations in a number of respects, some of which are critical to the homotopy interpretation, while others are technical conveniences or involve concepts that have not yet been studied in the homotopical setting.

Most significantly, the type theory described here is derived from the intensional version of Martin-Löf’s type theory [16], rather than the extensional version [18]. Whereas the extensional theory makes no distinction between judgmental and propositional equality, the intensional theory regards judgmental equality as purely definitional, and admits a much broader, proof-relevant interpretation of the identity type that is central to the homotopy interpretation. From the homotopical perspective, extensional type theory confines itself to homotopically discrete sets (see §3.1 (http://planetmath.org/31setsandntypes)), whereas the intensional theory admits types with higher-dimensional structure. The NuPRL system [3] is extensional, whereas both Coq [5] and Agda [23] are intensional. Among intensional type theories, there are a number of variants that differ in the structure of identity proofs. The most liberal interpretation, on which we rely here, admits a proof-relevant interpretation of equality, whereas more restricted variants impose restrictions such as uniqueness of identity proofs (UIP) [25], stating that any two proofs of equality are judgmentally equal, and Axiom K [25], stating that the only proof of equality is reflexivity (up to judgmental equality). These additional requirements may be selectively imposed in the Coq and Agda systems.

Another point of variation among intensional theories is the strength of judgmental equality, particularly as regards objects of function type. Here we include the uniqueness principle ($\eta$-conversion) $f\equiv \lambda x.f(x)$, as a principle of judgmental equality. This principle is used, for example, in §4.9 (http://planetmath.org/49univalenceimpliesfunctionextensionality), to show that univalence implies propositional function extensionality. Uniqueness principles are sometimes considered for other types. For instance, the uniqueness principle for cartesian products would be a judgmental version of the propositional equality $\mathrm{𝗎𝗉𝗉𝗍}$ which we constructed in §1.5 (http://planetmath.org/15producttypes), saying that $u\equiv ({\mathrm{𝗉𝗋}}_1(u),{\mathrm{𝗉𝗋}}_2(u))$. This and the corresponding version for dependent pairs would be reasonable choices (which we did not make), but we cannot include all such rules, because the corresponding uniqueness principle for identity types would trivialize all the higher homotopical structure. So we are forced to leave it out, and the question then becomes where to draw the line. With regards to inductive types, we discuss these points further in §5.5 (http://planetmath.org/55homotopyinductivetypes).

It is important for our purposes that (propositional) equality of functions is taken to be extensional (in a different sense than that used above!). This is not a consequence of the rules in this chapter; it will be expressed by Axiom 1 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#Thmaxiom1). This decision is significant for our purposes, because it specifies that equality of functions is as expected in mathematics. Although we include Axiom 1 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#Thmaxiom1) as an axiom, it may be derived from the univalence axiom and the uniqueness principle for functions (see §4.9 (http://planetmath.org/49univalenceimpliesfunctionextensionality)), as well as from the existence of an interval type (see Lemma 6.3.2 (http://planetmath.org/63theinterval#Thmprelem2)).

Regarding inductive types such as products, $\mathrm{\Sigma }$-types, coproducts, natural numbers, and so on (see http://planetmath.org/node/87578Chapter 5), there are additional choices regarding precisely how to formulate induction and recursion. Formally, one may describe type theory by taking either pattern matching or induction principles as basic and deriving the other; see http://planetmath.org/node/87881Appendix A. However, pattern matching in general is not yet well understood from the homotopical perspective (in particular, “nested” or “deep” pattern matching is difficult to make general sense of for higher inductive types). Moreover, it can be dangerous unless sufficient care is taken: for instance, the form of pattern matching implemented by default in Agda allows proving Axiom K. For these reasons, we have chosen to regard the induction principle as the basic property of an inductive definition, with pattern matching justified in terms of induction.

Unlike the type theory of Coq, we do not include a primitive type of propositions. Instead, as discussed in §1.11 (http://planetmath.org/111propositionsastypes), we embrace the propositions-as-types (PAT) principle, identifying propositions with types. This was suggested originally by de Bruijn [7], Howard [10], Tait [28], and Martin-Löf [14]. (Our decision is explained more fully in §3.2 (http://planetmath.org/32propositionsastypes),§3.3 (http://planetmath.org/33merepropositions).)

We do, however, include a full cumulative hierarchy of universes, so that the type formation and equality judgments become instances of the membership and equality judgments for a universe. As a convenience, we regard objects of a universe as types, rather than as codes for types; in the terminology of [20], this means we use “Russell-style universes” rather than “Tarski-style universes”. An alternative would be to use Tarski-style universes, with an explicit coercion function required to make an element $A:𝒰$ of a universe into a type $\mathrm{𝖤𝗅}(A)$, and just say that the coercion is omitted when working informally.

We also treat the universe hierarchy as cumulative, in that every type in ${𝒰}_i$ is also in ${𝒰}_j$ for each $j\ge i$. There are different ways to implement cumulativity formally: the simplest is just to include a rule that if $A:{𝒰}_i$ then $A:{𝒰}_j$. However, this has the annoying consequence that for a type family $B:A\to {𝒰}_i$ we cannot conclude $B:A\to {𝒰}_j$, although we can conclude $\lambda a.B(a):A\to {𝒰}_j$. A more sophisticated approach that solves this problem is to introduce a judgmental subtyping relation generated by , but this makes the type theory more complicated to study. Another alternative would be to include an explicit coercion function $\uparrow :{𝒰}_i\to {𝒰}_j$, which could be omitted when working informally.

It is also not necessary that the universes be indexed by natural numbers and linearly ordered. For some purposes, it is more appropriate to assume only that every universe is an element of some larger universe, together with a “directedness” property that any two universes are jointly contained in some larger one. There are many other possible variations, such as including a universe “${𝒰}_{\omega }$” that contains all ${𝒰}_i$ (or even higher “large cardinal” type universes), or by internalizing the hierarchy into a type family $\lambda i.{𝒰}_i$. The latter is in fact done in Agda.

The path induction principle for identity types was formulated by Martin-Löf [14]. The based path induction rule in the setting of Martin-Löf type theory is due to Paulin-Mohring [21]; it can be seen as an intensional generalization of the concept of “pointwise functionality” for hypothetical judgments from NuPRL [3, Section 8.1]. The fact that Martin-Löf’s rule implies Paulin-Mohring’s was proved by Streicher using Axiom K (see §7.2 (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem)), by Altenkirch and Goguen as in §1.12 (http://planetmath.org/112identitytypes), and finally by Hofmann without universes (as in http://planetmath.org/node/87560Exercise 1.7); see [25], §1.3 (http://planetmath.org/13universesandfamilies) and Addendum.

Title	Chapter 1 notes