Homotopy Type Theory, I
Posted by Mike Shulman
Last week I was at a mini-workshop at Oberwolfach entitled “The Homotopy Interpretation of Constructive Type Theory.” Some aspects of this subject have come up here a few times before, but mostly as a digression from other topics; now I want to describe it in a more structured way.
Roughly, the goal of this project is to develop a formal language and semantics, similar to the language and semantics of set theory, but in which the fundamental objects are homotopy types (a.k.a. -groupoids) rather than sets. There are several motivations for this, which I’ll mention below, but the most radical hope (which has been put forward most strongly by Voevodsky) is to create a new foundation for all of mathematics which is natively homotopical—that is, in which homotopy types are the basic objects, rather than being built up out of other basic objects such as sets.
I find this idea extremely exciting; at times I think it has the potential to transform the practice of everyday mathematics in a way that no foundational development has done since (probably) Cantor. But the most exciting thing of all is that the essential core of this language already exists in a completely different area of mathematics: intensional type theory. All that needs to be done is to reinterpret some words and perhaps add some additional axioms. (I especially enjoy the coincidence of terminology which allows me to say “homotopy type theory” and mean both “the homotopy version of type theory” and “the theory of homotopy types”!)
One reason this is especially exciting is that intensional type theory is (with good reason) the foundation of some of the most successful proof assistants for computer-verified mathematics, such as Coq and Agda. Thus, the -categorical revolution, if carried out in the language of homotopy type theory, will support and be supported by the inevitable advent of better computer-aided tools for doing mathematics. I never would have guessed that the computerization of mathematics would be best carried out, not by set-theory-like reductionism, but by an enrichment of mathematics to be natively -categorical.
Obviously there are more facets to this story than will fit in one blog post. Today, I’ll lay the groudwork by talking about the correspondence between homotopical semantics and intensional type theory; this is due to Steve Awodey, Nicola Gambino, Richard Garner, Peter Lumsdaine, Benno van den Berg, Michael Warren, and perhaps others I have forgotten (the original inspiration can be traced back at least to Hofmann and Streicher). In subsequent posts, I’ll say a bit about what mathematics looks like when done in homotopy type theory, and about some homotopically motivated axioms we may want to add to intensional type theory; this is the direction of Voevodsky’s recent work.
To start with, let’s recall a bit about set-theoretic language. Consider the following three ways to formalize set-theoretic reasoning:
Axiomatizing sets with a global membership relation between them, as in ZFC.
Axiomatizing the category of sets and functions, as in ETCS.
Axiomatizing sets and elements equipped with operations, such as constructions of products, exponentials, power sets, etc.
The first two have been called “material” and “structural” set theory, respectively, while the third is basically a funny way to describe extensional type theory. I’ll come back to the meaning of “extensional” in a bit; if you aren’t comfortable with type theory, you can think of extensional type theory as an “algebraicization” of the structure of a category, which says “type” instead of “object” or “set”. Where a category has a cartesian product determined up to isomorphism by a universal property, an extensional type theory has a specified type , with term-formation and computation rules that express essentially the same universal property, but in a set-like way involving elements. See also the nlab entry.
We also care particularly about dependent type theories, which we’ve talked about here before in general terms. Recall that this means that for any type we have a notion of “-indexed family of types,” so that if is such a thing we have a type for each . The basic operations on dependent types are the dependent sum , which is the type of pairs , and the dependent product , which is the type of functions such that for all , . When is constant (independent of ), the dependent sum reduces to the binary product , and the dependent product reduces to the function type .
In the “structural/categorial” approach we think of a type dependent on as a morphism , whose fiber over is . There are a couple of subtleties here. Firstly, in basic dependent type theory nothing requires that every morphism be interpretable as the projection of a dependent type. Thus, for a categorial theory of equal generality we should consider categories equipped with a special class of maps, often called display maps (and satisfying some axioms). Secondly, since substitution in type theory is strictly functorial, the display maps should have strictly functorial pullbacks. Of course strictly functorial pullbacks are hard to find in nature, but there are standard techniques for strictifying things.
The dependent sum and dependent product are modeled categorially by left and right adjoints to pullback. Thus, the “natural” semantics of (extensional) dependent type theory with dependent sums and products is in a locally cartesian closed category—although to be more precise we should consider the and functors only acting on the display maps.
Now suppose we want to axiomatize -groupoids instead of sets. It’s hard (for me) to imagine a way to do that based on a membership relation, but we could consider axioms on an -category that make it behave like , or we could extend the syntax of extensional type theory to describe -groupoids rather than sets.
We do have a pretty good idea of what -categorical axioms we should use, coming from the theory of Grothendieck (∞,1)-topoi. Specifically, we have the -categorical Giraud exactness axioms, and also the notion of an object classifier, and probably we’ll want a notion of local cartesian closure as well. However, -categories (using any model) are somewhat technical to work with directly. Moreover, since they include infinitely many sorts of data (-morphisms for all ), they can’t serve as a fully “elementary” foundational theory; they need a metatheory which at least knows about natural numbers.
However, in homotopy theory we have tools for working with -categories in a simpler way: we present them using structures on 1-categories, such as model categories or other weaker things. Amazingly, one particular categorical structure of this sort turns out to correspond fairly closely to a particular already existing version of type theory, called intensional type theory.
The categorical structure in question looks roughly like this. We have a category equipped with a single weak factorization system, which we think of as like the (acyclic cofibration, fibration) factorization system in a model structure. The class of “fibrations” also plays the role of the “display maps” mentioned above, which represent dependent types. Since every type can be considered as dependent on the unit type (or more precisely, dependent on the empty context), every morphism is a fibration/display-map, i.e. “every object is fibrant.” (We don’t assume the category has even finite limits or colimits, but we do assume it has a terminal object and pullbacks of fibrations. Combined with every object being fibrant, this implies it has finite products.) For a type theory with dependent products, we also want the category to be locally cartesian closed, or at least to have -functors acting on the fibrations.
This looks very much like a category of fibrant objects, except that we don’t postulate a separate class of “weak equivalences.” In fact, the only equivalences we’re interested in are the homotopy equivalences (which suggests that in a sense “all objects are cofibrant” as well, although we don’t actually have a notion of “cofibration”). The notion of “homotopy” here is defined in the usual way for a category of fibrant objects: every object has a path object obtained by factoring the diagonal as an acyclic-cofibration followed by a fibration, and a homotopy is a map which projects to .
Now, what is “intensional type theory” and how does it correspond to categories with weak factorization systems? Recall that one use of dependent types is to represent logic: a proposition with a free variable of type can be represented by a type dependent on , whose fibers might be subsingletons representing truth values, or they might contain more information, such as collecting all proofs of . In either case, the operations on dependent types correspond to logical operations on propositions: is “ and ,” is “ implies ”, is “for all , ,” and is either “there exists an such that ” or “the type of all such that ” (the latter being the type of witnesses, or proofs, of the former).
Now one of the most basic propositions in mathematics is an assertion of equality, “”. Thus, for any type , we should have a type dependent on two variables expressing this proposition. This type is usually written as and called an identity type. If each type is always a subsingleton (i.e. if two things can be equal in at most one way), then the identity types are called extensional; otherwise they are intensional.
Type theory with extensional identity is the most appropriate for a correspondence with set theory and 1-category theory; in that case the identity type is represented by the diagonal . However, extensional type theory is poorly behaved in ways that type theorists care about, so intensional type theory is also well studied, but for completely separate reasons from ours. What we care about right now is that the axioms for intensional identity types correspond very closely to saying that is a path object!
Specifically, the rules for identity types say:
For each , there is a specified element (every point is equal to itself in a canonical way); and
Given a type which may depend on two points and an equality between them, if we have a way to produce an element of for any , then we can “transport” it along any equality to produce a canonical element of (and in such a way that if we transport it along then it doesn’t change).
The first rule says that we have a map which factors the diagonal as . Since is a type dependent on , the second map in that factorization is a display map, a.k.a. fibration. And the “transport” property of the second rule is at least intuitively analogous to the “path-lifting” property of a fibration; it implies, among other things, that satisfies the left lifting property with respect to all display maps. In fact, for any suitable weak factorization system, the path objects satisfy the rules of identity types, although there are tricky coherence questions to be addressed; see this overview by Awodey and Warren, Warren’s thesis, and more recently this paper by van den Berg and Garner. Conversely, Gambino and Garner showed that the identity type rules imply a whole weak factorization system.
To conclude, I should mention one further aspect of this correspondence. We know that any object in a model category has a “simplicial resolution” which encodes all paths, paths-between-paths, etc. in . The simplicial object is Reedy fibrant, which implies that it is “internally a Kan complex” in the sense that is a Kan complex for any cofibrant . We can then use these -groupoid hom-spaces to make the model category into an -category.
We only need the one (acyclic cofibration, fibration) factorization system to construct , but we do need finite limits and colimits, which the syntactic category of a type theory doesn’t necessarily have. I believe the pullbacks of fibrations that it has are sufficient to construct a “semi-simplicial” Kan complex (one lacking degeneracies), and since any “semi-simplicial” Kan complex admits a choice of degeneracies, this is probably enough to capture the homotopy theory. However, we can construct a similar reflexive globular resolution without using any colimits, and (using some special properties of the identity type weak factorization system) the resulting globular object admits the structure of a Batanin/Leinster ω-groupoid. This was shown independently by Lumsdaine and van den Berg and Garner. In Peter Lumsdaine’s thesis, he extends these hom--groupoids to make the category of types/contexts into Batanin-Leinster -category.
It should have been obvious that these are two viewpoints on the same thing, but I didn’t realize it until Urs pointed it out. People are now thinking about ways to relate them directly.
Re: Homotopy Type Theory, I
Very nice summary, Mike!
I guess part II of the story is about how Vladimir Voevodsky has been really pushing things forward lately. His Univalent Foundations page is here:
http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations.html