Ideas have their time, and it’s not for us to choose when they arrive. But when they do, they almost always occur to many people at more or less the same time, often in a slightly disguised form whose underlying unity becomes apparent only later. This is perhaps not too surprising, the same seeds taking root in many a fertile mind. A bit harder to explain, though, is the moment in time when an idea comes to fruition. Often all of the ingredients are available, and yet no one thinks to put two-and-two together and draw what seems, in retrospect, to be the obvious inference. Until, suddenly, everyone does. Why didn’t we think of that ages ago? Nothing was stopping us, we just didn’t notice the opportunity!

The recent development of higher-dimensional structure in type theory seems to be a good example. All of the ingredients have been present since the 1970′s, yet as far as I know no one, until quite recently, no one quite put together all the pieces to expose the beautiful structure that has been sitting there all along. Like many good ideas, one can see clearly that the ideas were foreshadowed by many earlier developments whose implications are only now becoming understood. My plan is to explain higher type theory (HTT) to the well-informed non-expert, building on ideas developed by various researchers, including Thorsten Altenkirch, Steve Awodey, Richard Garner, Martin Hofmann, Dan Licata, Peter Lumsdaine, Per Martin-Löf, Mike Shulman, Thomas Streicher, Vladimir Voevodsky, and Michael Warren. It will be useful in the sequel to be familiar with The Holy Trinity, at least superficially, and preferably well enough to be able to move back and forth between the three manifestations that I’ve previously outlined.

One-dimensional dependent type theory is defined by derivation rules for these four fundamental forms of judgement (and, usually, some others that we suppress here for the sake of concision):

A *context*, , consists of a sequence of declarations of variables of the form , where it is presupposed, for each , that is derivable.

The key notion of dependent type theory is that of a *family of types* indexed by (zero or more) variables ranging over a type. The judgement states that is a family of types indexed by the variables given by . For example, we may have , specifying that is a closed type (a degenerate family of types), and , specifying that is a type (say, of sequences of naturals of length ) for each . The rules of type theory ensure, either directly or indirectly, that the structural properties of the hypothetical/general judgement are valid. In particular *families of types respect equality of indices*:

In words, if is a family of types indexed by , and if and are equal members of type , then every member of is also a member of .

The generalization to two- (and higher-) dimensional type theory can be motivated in several ways. One natural source of higher-dimensional structure is a *universe*, a type whose elements correspond to types. For example, we may have a universe* *of *sets* given as follows:

and so forth, ensuring that is closed under typical set-forming operations whose interpretations are given by in terms of standard type-theoretic concepts.

In many situations, including much of informal (yet entirely rigorous) mathematics, it is convenient to *identify* sets that are *isomorphic*, so that, for example, the sets and would be interchangeable. In particular, these sets should have the “same” (type of) elements. But obviously these two sets do not have the *same* elements (one consists of pairs, the other of functions, under the natural interpretation of the sets as types), so we cannot hope to treat and as *equal*, though we may wish to regard them as *equivalent *in some sense. Moreover, since two sets can be isomorphic in different ways, isomorphism must be considered a *structure on sets*, rather than a *property of sets*. For example, is isomorphic to itself in two different ways, by the identity and by negation (swapping). Thus, equivalence of the elements of two isomorphic sets must take account of the isomorphism itself, and hence must have computational significance.

It is precisely the desire to accommodate equivalences such as this that gives rise to higher dimensions in type theory. Specifically, we introduce two-dimensional structure by adding a new judgement to type theory stating that two members of a type are related by a specified *transformation*:

Crucially, families of types must respect transformation:

A transformation should be thought of as *evidence of interchangeability* of the members of a type; the *map* operation puts the evidence to work.

Returning to our example of the universe of sets, let us specify that a transformation from one set to another is an *pair of functions* constituting a bijection between the elements of the two sets:

(The equational conditions here are rather strong; I will return to this point in a future post. For now, let us just take this as the defining criterion of isomorphism between two sets.)

Evidence for the isomorphism of two sets induces a transformation on types given by the following equation:

(suppressing the obvious typing premises for and ). In words an isomorphism between sets and induces a transformation between their elements given by the isomorphism itself.

This, then, is the basic structure of two-dimensional type theory, but there is much more to say! In future posts I intend to develop the ideas further, including a discussion of these topics:

- The definition of is given by induction over the structure of . The above equation covers only one case; there are more, corresponding to each way of forming a family of types . The extension to function types will expose the role of the inverse of the isomorphism between sets.
- The judgement may be
*internalized*as a type, which will turn out to correspond to the*identity type*in Martin-Löf’s type theory, albeit with a different interpretation given by Altenkirch. The identity type plays an important role in the extension to all higher dimensions. - To ensure coherence and to allow for greater expressiveness we must also discuss
*equality*and*equivalence of transformations*and how these influence the induced transformation of families of types. In particular transformations admit a*groupoid structure*which expresses reflexivity, symmetry, and transitivity of transformation; these conditions can be considered to hold*strongly*or*weakly*, giving rise to different applications and interpretations. - Higher-dimensional type theory admits a fascinating interpretation in terms of
*homotopy theory*which types are interpreted as spaces, members as points in those spaces, and transformations as*paths*, or*homotopies*. This, together with a generalization of the treatment of universes outlined above, is the basis for Voevodsky’s work on*univalent foundations of mathematics*. - One may consider relaxing the groupoid structure on transformations to a “monoidoid” (that is, category) structure by not requiring symmetry (inverses). The structure of type theory changes significantly in the absence of symmetry, posing significant open problems, but admitting a wider range of applications of higher-dimensional structure in both CS and mathematics.

Thanks for posting this.

Since Cartmell it’s been known that the contexts and open terms of a well-behaved type theory form a category. The notion of a (weak) $\omega$-category is newer, but seems well-accepted at this point.

Is higher-dimensional type theory something more or less than the study of those type theories whose context-term categories are $\omega$-categories? Obviously I am missing something here, because simply combining these two concepts wouldn’t merit a new name. Is there a quick way to explain what it is I’m missing, or at least the interesting part of it?

Also, would you care to expand a bit on the motives behind point #5? Why insist that all morphisms are iso — aside, perhaps, from wanting to make homotopy theorists more comfortable?

The groupoid structure arises from considering equivalences; if we instead consider approximations, then we’d get a category structure at higher dimensions. It’s not wholly to do with homotopy; as will become apparent, the structure of type theory itself relies on invertibility/symmetry.

Actually, little is settled about weak omega-groupoids, not even their definition! Type theory may provide insights into these issues; time will tell.

Nice post, and I look forward to the rest of them! Are there any papers you would recommend reading?

You have a typo in the 4th premise of the “iso” rule: it should end with Elt(b).