Homotopy Type Theory using the Agda HoTT library/Chapter 1: Type Theory

Section 1.1: Type Theory versus Set Theory edit

Homotopy type theory is a foundational language for mathematics. It is similar to set theory in some ways, but there are several key differences upon which the subject hinges. In this section, we will briefly explain these differences, but will leave most of the discussion to the actual Homotopy Type Theory book.

Broadly speaking, set theory is divided into two layers. First, there is the deductive system of first-order logic, which gives us the ability to prove assertions using assumptions and a fixed collection of deductive rules. Second, we have to choose a collection of axioms within first-order logic that define set theory. The most frequently used collection of axioms is ZFC. Because of this, there is a distinction between the mathematics of set theory and the proofs that statements in set theory are true or false. In type theory, there is no such distinction; logic and mathematics are unified under one framework. Whereas in set theory, there are propositions and sets, in type theory, there are only types.

In set theory, one proves a proposition using the rules of logic. In type theory, one proves a proposition by constructing an element of its corresponding type. The theme of constructing objects in order to prove statements is central to type theory.

Type theory treats equality differently than set theory. In set theory, two objects are either equal or unequal. No attention is payed to how they became equal. In type theory, there are two notions of equality: judgmental equality and propositional equality. Two objects are determined to be judgmentally equal in type theory if they are defined to be equal from the beginning. Two objects are propositionally equal if we have to prove that they're equal using the rules of type theory. In particular, to prove a propositional equality, we must explicitly construct a proof and provide that construction as a witness of truth, whereas no such witness is needed for judgmental equality.

Moving on to judgments in general, in first-order logic, there is one kind of judgment: the statement that theorem A has a proof. In set theory, there is also the statement (which is formulated in first-order logic) that a is an element of the set A. In type theory, there are two kinds of judgments: that a has type A and that x is judgmentally equal to y. The judgment a has type A encompasses both provability in logic and membership in set theory. In set theory, membership in a set is a proposition. We can say things like "if x is a member of set X, then y is a member of set Y." In type theory, the statement that a is of type A is not a proposition, it is a judgment, which means that it simply is or isn't by definition. We can't say things like "if a has type A, then b has type B." Judgments exist "outside" of type theory in the sense that they are taken as given. If we think about type theory as a programming language (which it is), then the rules of type theory define the execution of the program and the judgments are the initial values of the variables.

Moreover, in set theory, membership is a relationship that exists between pre-defined objects; we can speak of elements and sets independently. In type theory, every object must have a type. There is no notion of an object existing in isolation. In set theory, an object can be a member of multiple sets. In type theory, an object can have only one type.

In summary, set theory is divided into rules (of first-order logic) and axioms (of ZFC). Type theory only has rules. This has the advantage of making type theory entirely procedural, whereas set theory relies on the information content of its axioms to prove statements (this has the unfortunate consequence that to automate proofs in set theory, we need special software to apply the axioms, whereas no special software is needed to run the rules of type theory).

Homotopy type theory does have one axiom, the Univalence Axiom that will be described later. Ideally, Univalence would also be a rule, but we don't know how to formulate a type theory in which this is the case.

For a more detailed introduction, consult the HoTT book.

Section 1.2: Function types edit