1.1 Type theory versus set theory\u00a0<\/b><\/p>\n
Homotopy type theory<\/a> is (among other things) a foundational language for mathematics, i.e., an alternative to Zermelo\u2013Fraenkel set theory<\/a>. However, it behaves differently from set theory in several important ways, and that can take some getting used to. Explaining these differences carefully requires us to be more formal here than we will be in the rest of the book. As stated in the introduction, our goal is to write type theory informally; but for a mathematician accustomed to set theory, more precision at the beginning can help avoid some common misconceptions and mistakes.<\/p>\n We note that a set-theoretic foundation has two \u201clayers\u201d: the deductive system of first-order logic, and, formulated inside this system, the axioms of a particular theory, such as ZFC. Thus, set theory is not only about sets, but rather about the interplay between sets (the objects of the second layer) and propositions (the objects of the first layer).<\/p>\n By contrast, type theory is its own deductive system: it need not be formulated inside any superstructure, such as first-order logic<\/a>. Instead of the two basic notions of set theory, sets and propositions, type theory has one basic notion: types. Propositions (statements which we can prove, disprove, assume, negate, and so on1) are identified with particular types, via the correspondence shown in Table 1 on page 11. Thus, the mathematical activity of proving a theorem is identified with a special case of the mathematical activity of constructing an object\u2014in this case, an inhabitant of a type that represents a proposition.<\/p>\n This leads us to another difference between type theory and set theory, but to explain it we must say a little about deductive systems in general. Informally, a deductive system is a collection of\u00a0rules\u00a0<\/b>for deriving things called\u00a0judgments<\/b>. If we think of a deductive system as a formal game, then the judgments are the \u201cpositions\u201d in the game which we reach by following the game rules. We can also think of a deductive system as a sort of algebraic theory, in which case the judgments are the elements (like the elements of a group) and the deductive rules are the operations (like the group multiplication). From a logical point of view, the judgments can be considered to be the \u201cexternal\u201d statements, living in the metatheory, as opposed to the \u201cinternal\u201d statements of the theory itself.<\/p>\n In the deductive system of first-order logic (on which set theory is based), there is only one kind of judgment: that a given proposition has a proof. That is, each proposition A gives rise to a judgment \u201cA has a proof\u201d, and all judgments are of this form. A rule of first-order logic such as \u201cfrom A and B infer A\u2227 B\u201d is actually a rule of \u201cproof construction<\/a>\u201d which says that given the judgments \u201cA has a proof\u201d and \u201cB has a proof\u201d, we may deduce that \u201cA \u2227 B has a proof\u201d. Note that the judgment \u201cA has a proof\u201d exists at a different level from the proposition A itself, which is an internal statement of the theory.<\/p>\n