One of the most striking differences between classical foundations and type theory is the idea of proof relevance, according to which mathematical statements, and even their proofs, become first-class mathematical objects. In type theory, we represent mathematical statements by types, which can be regarded simultaneously as both mathematical constructions and mathematical assertions, a conception also known as propositions as types. Accordingly, we can regard a term as both an element of the type (or in homotopy type theory, a point of the space ), and at the same time, a proof of the proposition . To take an example, suppose we have sets and (discrete spaces), and consider the statement “ is isomorphic to .” In type theory, this can be rendered as:
Reading the type constructors here as “there exists”, “for all”, and “and” respectively yields the usual formulation of “ and are isomorphic”; on the other hand, reading them as sums and products yields the type of all isomorphisms between and ! To prove that and are isomorphic, one constructs a proof , which is therefore the same as constructing an isomorphism between and , i.e., exhibiting a pair of functions together with proofs that their composites are the respective identity maps. The latter proofs, in turn, are nothing but homotopies of the appropriate sorts. In this way, proving a proposition is the same as constructing an element of some particular type.
In particular, to prove a statement of the form “ and ” is just to prove and to prove , i.e., to give an element of the type . And to prove that implies is just to find an element of , i.e. a function from to (determining a mapping of proofs of to proofs of ). This “constructive” conception (for more on which, see ,,) is what gives type theory its good computational character. For instance, every proof that something exists carries with it enough information to actually find such an object; and from a proof that “ or ” holds, one can extract either a proof that holds or one that holds. Thus, from every proof we can automatically extract an algorithm; this can be very useful in applications to computer programming.
However, this conception of logic does behave in ways that are unfamiliar to most mathematicians. On one hand, a naive translation of the axiom of choice yields a statement that we can simply prove. Essentially, this notion of “there exists” is strong enough to ensure that, by showing that for every there exists a such that , we automatically construct a function such that, for all , we have .
On the other hand, this notion of “or” is so strong that a naive translation of the law of excluded middle is inconsistent with the univalence axiom. For if we assume “for all , either or not ”, then since proving “” means exhibiting an element of it, we would have a uniform way of selecting an element from every nonempty type — a sort of Hilbertian choice operator. However, univalence implies that the element of selected by such a choice operator must be invariant under all self-equivalences of , since these are identified with self-identities and every operation must respect identity. But clearly some types have automorphisms with no fixed points, e.g. we can swap the elements of a two-element type.
Thus, the logic of “proposition as types” suggested by traditional type theory is not the “classical” logic familiar to most mathematicians. But it is also different from the logic sometimes called “intuitionistic”, which may lack both the law of excluded middle and the axiom of choice. For present purposes, it may be called constructive logic (but one should be aware that the terms “intuitionistic” and “constructive” are often used differently).
The computational advantages of constructive logic imply that we should not discard it lightly; but for some purposes in classical mathematics, its non-classical character can be problematic. Many mathematicians are, of course, accustomed to rely on the law of excluded middle; while the “axiom of choice” that is available in constructive logic looks superficially similar to its classical namesake, but does not have all of its strong consequences. Fortunately, homotopy type theory gives a finer analysis of this situation, allowing various different kinds of logic to coexist and intermix.
The new insight that makes this possible is that the system of all types, just like spaces in classical homotopy theory, is “stratified” according to the dimensions in which their higher homotopy structure exists or collapses. In particular, Voevodsky has found a purely type-theoretic definition of homotopy -types, corresponding to spaces with no nontrivial homotopy information above dimension . (The -types are the “sets” mentioned previously as satisfying Lawvere’s axioms.) Moreover, with higher inductive types, we can universally “truncate” a type into an -type; in classical homotopy theory this would be its Postnikov section.
With these notions in hand, the homotopy -types, which we call (mere) propositions, support a logic that is much more like traditional “intuitionistic” logic. (Classically, every -type is empty or contractible; we interpret these possibilities as the truth values “false” and “true” respectively.) The “-truncated axiom of choice” is not automatically true, but is a strong assumption with the same sorts of consequences as its counterpart in classical set theory. Similarly, the “-truncated law of excluded middle” may be assumed, with many of the same consequences as in classical mathematics. Thus, the homotopical perspective reveals that classical and constructive logic can coexist, as endpoints of a spectrum of different systems, with an infinite number of possibilities in between (the homotopy -types for ). We may speak of “” and “”, with being provable and inconsistent with univalence, while and are the versions familiar to classical mathematicians (hence in most cases it is appropriate to assume the subscript when none is given). Indeed, one can even have useful systems in which only certain types satisfy such further “classical” principles, while types in general remain “constructive.”
It is worth emphasizing that univalent foundations does not require the use of constructive or intuitionistic logic. Most of classical mathematics which depends on the law of excluded middle and the axiom of choice can be performed in univalent foundations, simply by assuming that these two principles hold (in their proper, -truncated, form). However, type theory does encourage avoiding these principles when they are unnecessary, for several reasons.
First of all, every mathematician knows that a theorem is more powerful when proven using fewer assumptions, since it applies to more examples. The situation with and is no different: type theory admits many interesting “nonstandard” models, such as in sheaf toposes, where classicality principles such as and tend to fail. Homotopy type theory admits similar models in higher toposes, such as are studied in ,,. Thus, if we avoid using these principles, the theorems we prove will be valid internally to all such models.
Secondly, one of the additional virtues of type theory is its computable character. In addition to being a foundation for mathematics, type theory is a formal theory of computation, and can be treated as a powerful programming language. From this perspective, the rules of the system cannot be chosen arbitrarily the way set-theoretic axioms can: there must be a harmony between them which allows all proofs to be “executed” as programs. We do not yet fully understand the new principles introduced by homotopy type theory, such as univalence and higher inductive types, from this point of view, but the basic outlines are emerging; see, for example, . It has been known for a long time, however, that principles such as and are fundamentally antithetical to computability, since they assert baldly that certain things exist without giving any way to compute them. Thus, avoiding them is necessary to maintain the character of type theory as a theory of computation.
Fortunately, constructive reasoning is not as hard as it may seem. In some cases, simply by rephrasing some definitions, a theorem can be made constructive and its proof more elegant. Moreover, in univalent foundations this seems to happen more often. For instance:
In set-theoretic foundations, at various points in homotopy theory and category theory one needs the axiom of choice to perform transfinite constructions. But with higher inductive types, we can encode these constructions directly and constructively. In particular, none of the “synthetic” homotopy theory in http://planetmath.org/node/87582Chapter 8 requires or .
In set theory, various circumlocutions are required to obtain notions of “cardinal number” and “ordinal number” which canonically represent isomorphism classes of sets and well-ordered sets, respectively — possibly involving the axiom of choice or the axiom of foundation. But with univalence and higher inductive types, we can obtain such representatives directly by truncating the universe; see http://planetmath.org/node/87584Chapter 10.
In set-theoretic foundations, the definition of the real numbers as equivalence classes of Cauchy sequences requires either the law of excluded middle or the axiom of (countable) choice to be well-behaved. But with higher inductive types, we can give a version of this definition which is well-behaved and avoids any choice principles; see http://planetmath.org/node/87585Chapter 11.
Of course, these simplifications could as well be taken as evidence that the new methods will not, ultimately, prove to be really constructive. However, we emphasize again that the reader does not have to care, or worry, about constructivity in order to read this book. The point is that in all of the above examples, the version of the theory we give has independent advantages, whether or not and are assumed to be available. Constructivity, if attained, will be an added bonus.
Given this discussion of adding new principles such as univalence, higher inductive types, , and , one may wonder whether the resulting system remains consistent. (One of the original virtues of type theory, relative to set theory, was that it can be seen to be consistent by proof-theoretic means). As with any foundational system, consistency is a relative question: “consistent with respect to what?” The short answer is that all of the constructions and axioms considered in this book have a model in the category of Kan complexes, due to Voevodsky  (see  for higher inductive types). Thus, they are known to be consistent relative to ZFC (with as many inaccessible cardinals as we need nested univalent universes). Giving a more traditionally type-theoretic account of this consistency is work in progress (see, e.g., ,).
We summarize the different points of view of the type-theoretic operations in Table 1.
|predicate||family of sets||fibration|
|conditional proof||family of elements||section|
|set of pairs||product space|
|set of functions||function space|
|disjoint sum||total space|
|product||space of sections|
- 1 Bruno Barras and Thierry Coquand and Simon Huber. A Generalization of Takeuti-Gandy Interpretation. \urlhttp://uf-ias-2012.wikispaces.com/file/view/semi.pdf, 2013.
- 2 Chris Kapulkin and Peter LeFanu Lumsdaine and Vladimir Voevodsky. The Simplicial Model of Univalent Foundations, 2012. \hrefhttp://arxiv.org/abs/1211.2851/arXiv:1211.2851.
- 3 Andrey Kolmogorov. Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift, 35:58–65 1932
- 4 Licata,Daniel R. and Harper,Robert. Canonicity for 2-dimensional type theory. In emphProceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 337–348ACM, .
- 5 Licata,Daniel R. and Harper,Robert. Canonicity for 2-dimensional type theory. In emphProceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 337–348ACM, .
- 6 Peter LeFanu Lumsdaine and Michael Shulman. Higher inductive types. In preparation, 2013.
- 7 Jacob Lurie, Higher topos theory Princeton University Press,2009
- 8 Charles Rezk. Toposes and homotopy toposes. \urlhttp://www.math.uiuc.edu/ rezk/homotopy-topos-sketch.pdf, 2005.
- 9 Bertrand Toën and Gabriele Vezzosi. Homotopical Algebraic Geometry I: Topos theory, 2002. \hrefhttp://arxiv.org/abs/math/0207028/arXiv:math/0207028.
- 10 Troelstra,Anne Sjerp and van Dalen,Dirk, Constructivism in mathematics. Vol. I North-Holland Publishing Co.,1988
- 11 Troelstra,Anne Sjerp and van Dalen,Dirk, Constructivism in mathematics. Vol. II North-Holland Publishing Co.,1988