Constructivity

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 $a:A$ as both an element of the type $A$ (or in homotopy type theory, a point of the space $A$), and at the same time, a proof of the proposition $A$. To take an example, suppose we have sets $A$ and $B$ (discrete spaces), and consider the statement “$A$ is isomorphic to $B$.” In type theory, this can be rendered as:

$$\mathrm{𝖨𝗌𝗈}(A,B):\equiv \sum _{(f:A\to B)}\sum _{(g:B\to A)}(({\prod }_{(x:A)}g(f(x))=x)\times ({\prod }_{(y:B)}f(g(y))=y)).$$

Reading the type constructors $\mathrm{\Sigma },\mathrm{\Pi },\times$ here as “there exists”, “for all”, and “and” respectively yields the usual formulation of “$A$ and $B$ are isomorphic”; on the other hand, reading them as sums and products yields the type of all isomorphisms between $A$ and $B$! To prove that $A$ and $B$ are isomorphic, one constructs a proof $p:\mathrm{𝖨𝗌𝗈}(A,B)$, which is therefore the same as constructing an isomorphism between $A$ and $B$, i.e., exhibiting a pair of functions $f,g$ 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 “$A$ and $B$” is just to prove $A$ and to prove $B$, i.e., to give an element of the type $A\times B$. And to prove that $A$ implies $B$ is just to find an element of $A\to B$, i.e. a function from $A$ to $B$ (determining a mapping of proofs of $A$ to proofs of $B$). This “constructive” conception (for more on which, see [3],[10],[11]) 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 “$A$ or $B$” holds, one can extract either a proof that $A$ holds or one that $B$ 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 $x:A$ there exists a $y:B$ such that $R(x,y)$, we automatically construct a function $f:A\to B$ such that, for all $x:A$, we have $R(x,f(x))$.

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 $A$, either $A$ or not $A$”, then since proving “$A$” 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 $A$ selected by such a choice operator must be invariant under all self-equivalences of $A$, 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 $n$-types, corresponding to spaces with no nontrivial homotopy information above dimension $n$. (The $0$-types are the “sets” mentioned previously as satisfying Lawvere’s axioms.) Moreover, with higher inductive types, we can universally “truncate” a type into an $n$-type; in classical homotopy theory this would be its $n^{\mathrm{th}}$ Postnikov section.

With these notions in hand, the homotopy $(-1)$-types, which we call (mere) propositions, support a logic that is much more like traditional “intuitionistic” logic. (Classically, every $(-1)$-type is empty or contractible; we interpret these possibilities as the truth values “false” and “true” respectively.) The “$(-1)$-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 “$(-1)$-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 $n$-types for ). We may speak of “${\mathrm{𝖫𝖤𝖬}}_n$” and “${\mathrm{𝖠𝖢}}_n$”, with ${\mathrm{𝖠𝖢}}_{\mathrm{\infty }}$ being provable and ${\mathrm{𝖫𝖤𝖬}}_{\mathrm{\infty }}$ inconsistent with univalence, while ${\mathrm{𝖠𝖢}}_{-1}$ and ${\mathrm{𝖫𝖤𝖬}}_{-1}$ are the versions familiar to classical mathematicians (hence in most cases it is appropriate to assume the subscript $(-1)$ 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, $(-1)$-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 $\mathrm{𝖠𝖢}$ and $\mathrm{𝖫𝖤𝖬}$ is no different: type theory admits many interesting “nonstandard” models, such as in sheaf toposes, where classicality principles such as $\mathrm{𝖠𝖢}$ and $\mathrm{𝖫𝖤𝖬}$ tend to fail. Homotopy type theory admits similar models in higher toposes, such as are studied in [9],[8],[7]. 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, [5]. It has been known for a long time, however, that principles such as $\mathrm{𝖠𝖢}$ and $\mathrm{𝖫𝖤𝖬}$ 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:

1. 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 $\mathrm{𝖫𝖤𝖬}$ or $\mathrm{𝖠𝖢}$.

2. In set-theoretic foundations, the statement “every fully faithful and essentially surjective functor is an equivalence of categories” is equivalent to the axiom of choice. But with the univalence axiom, it is just true; see http://planetmath.org/node/87583Chapter 9.

3. 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.

4. 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 $\mathrm{𝖫𝖤𝖬}$ and $\mathrm{𝖠𝖢}$ 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, $\mathrm{𝖠𝖢}$, and $\mathrm{𝖫𝖤𝖬}$, 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 [2] (see [6] 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., [5],[1]).

We summarize the different points of view of the type-theoretic operations in Table 1.

Types	Logic	Sets	Homotopy
$A$	proposition	set	space
$a:A$	proof	element	point
$B(x)$	predicate	family of sets	fibration
$b(x):B(x)$	conditional proof	family of elements	section
$\mathrm{𝟎},\mathrm{𝟏}$	$\perp ,\top$	$\mathrm{\varnothing },\{\mathrm{\varnothing }\}$	$\mathrm{\varnothing },*$
$A+B$	$A\vee B$	disjoint union	coproduct
$A\times B$	$A\wedge B$	set of pairs	product space
$A\to B$	$A\Rightarrow B$	set of functions	function space
${\sum }_{(x:A)}B(x)$	${\exists }_{x:A}B(x)$	disjoint sum	total space
${\prod }_{(x:A)}B(x)$	${\forall }_{x:A}B(x)$	product	space of sections
${\mathrm{𝖨𝖽}}_A$	equality $=$	$\{(x,x)|x\in A\}$	path space $A^I$

Table 1: Comparing points of view on type-theoretic operations

Title	Constructivity