As many of you may know, the Institute for Advanced Study is sponsoring a year-long program, called “Univalent Foundations for Mathematics” (UF), which is developing the theory and applications of Homotopy Type Theory (HTT). The UF program is organized by Steve Awodey (CMU), Thierry Coquand (Chalmers), and Vladimir Voevodsky (IAS). About two dozen people are in residence at the Institute to participate in the program, including Peter Aczel, Andrej Bauer, Peter Dybjer, Dan Licata, Per Martin-Löf, Peter Lumsdaine, Mike Shulman, and many others. I have been shuttling back and forth between the Institute and Carnegie Mellon, and will continue to do so next semester.

The excitement surrounding the program is palpable. We all have the sense that we are doing something *important* that will change the world. A typical day consists of one or two lectures of one or two hours, with the rest of the day typically spent in smaller groups or individuals working at the blackboard. There are many strands of work going on simultaneously, including fundamental type theory, developing proof assistants, and formulating a body of informal type theory. As visitors come and go we have lectures on many topics related to HTT and UF, and there is constant discussion going on over lunch, tea, and dinner each day. While there I work each day to the point of exhaustion, eager to pursue the many ideas that are floating around.

So, why is homotopy type theory so exciting? For me, and I think for many of us, it is the most exciting development in type theory since its inception. It brings together two seemingly disparate topics, algebraic topology and type theory, and provides a gorgeous framework in which to develop both mathematics and computer science. Many people have asked me why it’s so important. My best answer is that it’s too beautiful to be ignored, and such a beautiful concept bmust be good for something! We’ll be at this for years, but it’s too soon to say yet where the best applications of HTT will arise. But I am sure in my bones that it’s as important as type theory itself.

Homotopy type theory is based on two closely related concepts:

*Constructivity*. Proofs of propositions are mathematical objects classified by their types.*Homotopy.*Paths between objects of a type are proofs of their interchangeability in all contexts. Paths in a type form a type whose paths are homotopies (deformations of paths).

Homotopy type theory is organized so that maps and families *respect homotopy*, which, under the identification of paths with equality proofs, means that they respect equality. The force of this organization arises from axioms that specify what are the paths within a type. There are two major sources of non-trivial paths within a type, the *univalence axiom*, and *higher inductive types*.

The univalence axiom specifies that there is an equivalence between equivalences and equalities of the objects of a universe. Unravelling a bit, this means that for any two types inhabiting a universe, evidence for their equivalence (a pair of maps that are inverse up to higher homotopy, called *weak equivalence*) is evidence for their equality. Put another way, weak equivalences are paths in the universe. So, for example, a bijection between two elements of the universe of sets constitutes a proof of the *equality* (universal interchangeability) of the two sets.

Higher inductive types allow one to define types by specifying their elements, any paths between their elements, any paths between those paths, and so on to any level, or *dimension*. For example, the interval, , has as elements the endpoints , and a path between and within . The circle, has an element and a path from to itself within .

Respect for homotopy means that, for example, a family of types indexed by the type must be such that if and are isomorphic sets, then there must be an equivalence between the types and allowing us to transport objects from one “fiber” to the other. And any function with domain must respect bijection—it could be the cardinality function, for example, but it cannot be a function that would distinguish from .

Univalence allows us to formalize the informal convention of identifying things “up to isomorphism”. In the presence of univalence equivalence types (spaces) are, in fact, *equal*. So rather than rely on convention, we have a formal account of such identifications.

Higher inductives generalize ordinary inductive definitions to higher dimensions. This means that we can now define maps (computable functions!) between, say, the 4-dimensional sphere and the 3-dimensional sphere, or between the interval and the torus. HTT makes absolutely clear what this even means, thanks to higher inductive types. For example, a map out of is given by two pieces of data:

- What to do with the base point. It must be mapped to a point in the target space.
- What to do with the loop. It must be mapped to a loop in the target space based at the target point.

A map out of is given similarly by specifying

- What to do with the endpoints. These must be specified points in the target space.
- What to do with the segment. It must be a path between the specified points in the target space.

It’s all just good old functional programming! Or, rather, it *would* be, if we were to have a good computational semantics for HTT, a topic of intense interest at the IAS this year. It’s all sort-of-obvious, yet also sort-of-non-obvious, for reasons that are difficult to explain briefly. (If I could, they would probably be considered obvious, and not in need of much explanation!)

A game-changing aspect of all of this is that HTT provides a very nice foundation for mathematics in which types (-groupoids) play a fundamental role as classifying all mathematical objects, including proofs of propositions, which are just types. Types may be classified according to the structure of their paths—and hence propositions may be classified according to the structure of their proofs. For example, any two proofs of equivalence of two natural numbers are themselves equivalent; there’s only one way to say that , for example. Of course there is no path between and . And these two situations exhaust the possibilities: any two paths between natural numbers are equal (but there may not even be one). This unicity of paths property lifts to function spaces by extensionality, paths between functions being just paths between the range elements for each choice of domain element. But the universe of Sets is not like this: there are many paths between sets (one for each bijection), and these are by no means equivalent. However, there is at most one way to show that two bijections between sets are equivalent, so the structure “peters out” after dimension 2.

The idea to apply this kind of analysis to proofs of propositions is a distinctive feature of HTT, arising from the combination of constructivity, which gives proofs status as mathematical objects, and homotopy, which provides a powerful theory of the equivalence of proofs. Conventional mathematics ignores proofs as objects of study, and is thus able to express certain ideas only indirectly. HTT brings out the latent structure of proofs, and provides an elegant framework for expressing these concepts directly.

*Update*: edited clumsy prose and added concluding paragraph.

Are you sure that there is only one proof of 2+2=4? I can see at least two: by normalization (i.e. 1+(1+(1+(1+0))) = 1+(1+(1+(1+0))) ), and also the following:

first, pull out common factor of lhs 2+2 as 2*(1+1), then apply isomorphism to get 2*2; also, factor rhs as 2*2. These are equal (by refl).

As far as I can tell, these 2 proofs are not equal, and their equivalence is not straightforward either. [At least, in the Agda code that I and colleagues have for doing this, these proofs are not equal.]

All of these machinations are just definitional equivalences (because they’re all about closed terms), and are therefore transparent. Yes, 4 is the same as 2*(1+1), but these are just calculations (even if they arose from more general lemmas that are not).

I was not questioning if 2+2=4=2*(1+1). I was questioning your statement that the *proofs* of these facts are equivalent. You stated that they are, and I gave proofs that seem different. In your reply, you seem to agree with me that the lemmas involved are different.

I believe the Lemmas you are talking about are universally quantified statements about numbers. These lemmas may well have different proofs (e.g., differ in the induction variable or pattern of argument). But once specialized to specific numbers, they are just statements of reflexivity. So, for example, we may have a lemma stating that for every x, y, x+y is y+x. If we choose m and n to be specific numbers, we’re just calculating that m+n calculates to n+m, so the evidence for their equality is trivial.

Put another way, Nat is a homotopy set, which is to say that its path structure is discrete. For each n there is exactly one path from n to itself, reflexivity, and there are no other paths.

Monsieur Carette, Actually, there is some equivocation on “proof”, “+”, “*”, and perhaps “2″ and “4″, here. In the above post, our host is using “proof” in the sense that Type theorists seem to use the word, which boils down to: having interpreted as natural numbers the several expressions you mention, the natural numbers object itself knows that the interpretations themselves are the same natural number, and it knows this in exactly one way. But you are reasoning about various terms in an equational theory before considering their natural semantics, which is to say you’re looking first at some quotient object — a potentially-nasty higher-inductive-type which happens to have a map to the natural numbers. It may well be that you have distinct paths between the representations 2+2 and 4 in your quotient object, but after mapping down to the naturals that distinction becomes irrelevant.

I’ve heard a lot of buzz about HTT and about this IAS programme, but still have no idea what it’s all about. Are there likely to be any “popular” outputs from the programme, that would make the reasons for the buzz more accessible?

Um, isn’t that the point of my article?

In view of Robert Haper’s comment below (http://existentialtype.wordpress.com/2012/12/03/univalent-foundations-program/#comment-1125) I can maybe expand more on the above question:

“Are there likely to be any ‘popular’ outputs from the programme, that would make the reasons for the buzz more accessible?”

What is now called “higher topos theory” or rather “infinity-topos theory” (http://ncatlab.org/nlab/show/%28infinity,1%29-topos) is the unification of two fundamental strands of mathematics, namely homotopy theory and geometry. People also speak of “higher geometry” or “derived geometry” (http://ncatlab.org/nlab/show/higher+geometry) or the theory of “infinity-stacks” or “derived stacks”.

Every since the mechanisms of oo-topos theory have been more fully understood just a few years back, there has been an enormous activity in this direction which is bearing fruit in all kinds of fields of mathematics. Famous examples are Voevodsky’s very own “A1-homotopy theory” (http://ncatlab.org/nlab/show/A1-homotopy%20theory) used to prove the Bloch-Kato conjecture and used for motivic cohomology theory, as well as Jacob Lurie’s construction of the long-sought tmf spectrum (the “universal elliptic cohomology theory”) by realizing the moduli stack of elliptic curves as an object in higher geometry (http://ncatlab.org/nlab/show/A+Survey+of+Elliptic+Cohomology), as well as the classification and construction of extended higher dimensional topological quantum field theories (http://ncatlab.org/nlab/show/cobordism%20hypothesis). All of these examples, but the last one most explicitly, have some connection to deep questions in modern theoretical physics of quantum field theory. Myself, I have been working on axiomatic descriptions and realizations of higher differential geometry and its quantum field theoretic applications using infinity-toposes for a while (http://ncatlab.org/schreiber/show/differential+cohomology+in+a+cohesive+topos).

All of this work flows out of infinity-topos theory. But handling infinity-toposes is not always entirely easy. Already a cursory look at the fundamental textbook on the matter, Jacob Lurie’s book (http://ncatlab.org/nlab/show/Higher%20Topos%20Theory) reveals that the way these are regarded as objects that themselves are or at least are built out of simplicial sets can tend to be somewhat intricate and technical.

On the other hand, it has long been known that ordinary toposes have in addition to their external description as systems of (large) sets with extra structure a powerful and elegant internal description by way of their internal logic (http://ncatlab.org/nlab/show/internal%20logic). In fact the internal logic of locally cartesian closed categories such as toposes is equivalent to dependent type theory (http://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory) IF one constrains the identity types (http://ncatlab.org/nlab/show/identity%20type) to make them “extensional” (http://ncatlab.org/nlab/show/extensional%20type%20theory).

Not making that restriction leads to something more general (http://ncatlab.org/nlab/show/intensional%20type%20theory), which for decades nobody new what to make of, as far as the categorical semantics goes. The shock of excitement that occurred when Vovodsky and Awodey and others suddenly noticed (http://ncatlab.org/nlab/show/homotopy+type+theory#Introductions) that not making that restriction, hence sticking with a _simpler axiomatics_, in fact yields the internal language of those infinity-toposes and hence of higher/homotopical/derived geometry is what still causes the “buzz” that Jeremy Gibbons is wondering about above.

And strikingly, many statements about infinity-toposes become much simpler in their internal homotopy type theory language. A young colleague of mine in Nijmegen, Egbert Rijke, just recently rediscovered, just working in HoTT, the full esteemed theory of relative Moore-Postnikov towers (http://ncatlab.org/nlab/show/Postnikov+system) without ever having heard himself of the traditional theory before. And since he did so in homotopy type theory he actually re-discovered this way not just this traditional theory, but its generalization to arbitrary infinity-toposes (http://ncatlab.org/nlab/show/%28n-connected%2C+n-truncated%29+factorization+system). Moreover, his proofs and definition fit neatly on two pages, and are much simpler, much more concise and much more transparent than the traditional ones.

Due this simplification of aspects of infinity-topos theory brought about by its internal formulation in homotopy type theory, we are now beginning to see HoTT derive new theorems and statements about homotopy theory and generally infinity-topos. It is, for some purpose, a more well-adapted language that enormously simplifies certain constructions. And it has a computer proof asistant behind it…

For instance just recently I ran into a technical problem when formalizing certain objects called “higher moduli stacks of differential cocycles” in infinity-topos theory, which we need for the formulation of quantum field theories of higher Chern-Simons type (http://ncatlab.org/schreiber/show/infinity-Chern-Simons+theory). I like to think that I could have solved it with a bit of work, but I was being lazy and just walked over to my homotopy type theory colleage. While he knows little about physics and higher geometry, I can use the dictionary between infinity-topos theory and homotopy type theory to easily explain to him the technical problem that I am facing. And sure enough, just the other day he sends me the solution and the proof. (This refers to material now in section 3.9.6.3 and 4.4.14.3 of http://ncatlab.org/schreiber/files/cohesivedocumentv032.pdf).

I think it is clear that this is only the beginning of a very fruitful interaction between homotopy type theory and infinity-topos theory/higher geometry/parameterized homotopy theory, and hence a vast amount of mathematics (http://ncatlab.org/nlab/show/applications+of+%28higher%29+category+theory). Homotopy type theory simply is the natural language for reasoning in modern geometry/homotopy theory, and that natural language has begun to to provide new insights and will soon provide plenty more.

Hey, Robert

Very enjoyable article. Since I’ve been looking into Category Theory recently, I was wondering, how HTT relates to Cat.Theory? Could you spare a few words on that?

Thanks,

Vladimir

Homotopy type theory is the internal language of those higher categories which are higher toposes. A quick dictionary showing the relation is here:

http://ncatlab.org/nlab/show/homotopy%20type%20theory#DictionaryToCoq

For a bit more see

http://ncatlab.org/nlab/show/HoTT+methods+for+homotopy+theorists

(Looking back at both I see that both deserve to be further expanded…)

Thanks for the reference, Urs. I suspect that this is more what Jeremy is looking for.