### What is Homotopy Type Theory Good For?

#### Posted by Urs Schreiber

The current situation of homotopy type theory reminds me a bit of the dot-com bubble at the turn of the millenium.

Back then a technology had appeared which was as powerful as it was new: while everybody had a sure *feeling* that the technology would have dramatically valuable impact, because it was so new nobody had an actual *idea* of what that would be. As opposed to other bubbles, that one did not burst because overly optimistic hopes had been unjustifed as such, but because it took a while to understand just how these hopes would be materialized in detail (for instance that today I would send a message as this here from a café via my webbook from my dropbox account).

With homotopy type theory the situation currently seems to be similar to me. On the one hand it is clear that some dramatic breakthrough right at the heart of mathematics has occured. One hears the sound of something big happening. But: what is the impact? It feels like after 1995 – when it was clear that the internet is going to be *something* big – but still before, say, 2003, when we started getting a good idea of *how* it changes our lives.

How will homotopy type theory change our lives?

Currently most research in homotopy type theory revolves around the fine-tuning of the formulation itself and completing the understanding of its relation to traditional homotopy theory. That’s necessary and good. (It’s great, I am enthusiastic about it!) But if the excitement about HoTT is not to be an illusion, then something will follow after that. The traditional homotopy theorist currently may complain (and some do) that much of what is happening is that facts already known are being re-formulated in a new language, not always yet to an effect a homotopy theorist would find noteworthy.

So I am wondering: how will the traditional homotopy theorist eventually benefit from homotopy type theory? How the researcher who *uses* homotopy theory for something else?

I am asking for personal reasons, too. Since, somewhat inadvertently, I have been investing some of my time into learning about it, I am naturally wondering: how will that time investment pay off for me? What does homotopy type theory do for my research?

I am not sure yet. But I have some first ideas. One of these I want to share here.

## An example

My research, you may have noticed, is motivated from understanding basic structural phenomena in theoretical physics as incarnations of natural mathematical structures. What I will try to indicate in the following is a certain kind of problem that poses itself in the context of string theory, which – I think it is fair to say – was generally regarded to be among the more subtle problems in a field rich in subtle mathematical effects, and how it finds an elegant and simple solution once you regard it from the perspective of homotopy type theory.

What I say in the following I have said in different words before, together with my coauthors Domenico Fiorenza and Hisham Sati: in section 2 of an article titled *The E8-moduli 3-stack of the C-field in M-theory*. There we point out that the solution which we propose and study in the article, to some problem in string theory, can naturally be understood simply by reformulating a well-known equation – known as the *flux quantization condition* – first as a fiber product of sets of certain field configurations and then refining that to a homotopy fiber product of moduli ∞-stacks of certain field configurations.

Here I will just observe that if you come to this from homotopy type theory, then the solution looks even more elegant than this: one arrives there simply by taking verbatim the symbols denoting the solution set to the equation, but now interpreting these not in the ordinary logic of sets, but in the homotopy logic of homotopy types. It is then homotopy type theory which automatically produces the correct answer, the “$E_8$-moduli 3-stack of the supergravity C-field in M-theory”. A solution that looks subtle to the eye of classical logic becomes self-evident from the point of view of homotopy logic / homotopy type theory.

From these remarks everybody with just basic training in category theory and homotopy theory can already deduce what I will say below. And what I say next is not hard to see, once you see it. It is one of those cases where a simple change of perspective leads with great ease to a solution of what seemed to be a difficult technical problem. Nevertheless, or because of this, I thought I’d say this explicitly.

## Formulation in ordinary logic

The situation studied in that article concerns a hypothetical physical system in which on spacetime $X$ three different species of fields propagate: 1. the field of gravity, 2. a gauge field for the gauge group E8, and 3. a higher gauge field called (part of) the supergravity C-field. It is not important for the following what exactly these fields are and why. Important are the following two aspects only.

Since all of them are gauge fields, there is

**no naive notion of**between different field configurations. Instead, there is a sensible notion of*equality**equivalence*of field configurations. (In physics this is called*gauge equivalence*.)Moreover, since these are higher gauge fields, there is no naive notion of equality even between the gauge equivalences themselves. Instead there are higher order equialences between them. (Physicists describe this state of affairs by saying that there are

*higher order ghosts*.)In the problem under consideration in the above article, there is a

**constraint equation**that is required to be satisfied by the gauge equivalence classes of the three fields, the “flux quantization condition”.

The question is then: what is the right collection of field configurations that satisfy the constraint equation? What are the gauge equivalences between these? *What is the mathematical model for the supergravity $C$-field?*

Let’s formulate this a bit more in symbols. Naively, we would say that there is a *set* of configurations of the field of gravity. I’ll write that set “$[X, \mathbf{B}Spin_{conn}]$”, but this is just notation which you need not care about for the following, if you don’t want to. (If you do, see the above article for details!) Similarly there is a set $[X, \mathbf{B}E_8]$ of configurations of the gauge field. And a set, to be denoted, $[X, \mathbf{B}^3 U(1)_{conn}]$, of configurations of (part of) the $C$-field. So we’d write

$\begin{aligned} \phi_{gr} & \in [X, \mathbf{B}Spin_{conn}] \\ \phi_{ga} & \in [X, \mathbf{B}E_8] \\ \phi_{hg} & \in [X, \mathbf{B}^3 U(1)_{conn}] \end{aligned}$

to denote elements of these sets, representing configurations of each of these fields.

Now, each of these fields induces yet another field, much like the field of, say, electrons induces a magnetic field. We have functions that send the above field configurations to configurations of that induced field. These functions go by the following names (but again, these are just names, here we only need that there are three such functions):

$\begin{aligned} \frac{1}{2}p_1 & : [X, \mathbf{B}Spin_{conn}] \to [X, \mathbf{B}^3 U(1)] \\ 2 a & : [X, \mathbf{B}E_8] \to [X, \mathbf{B}^3 U(1)] \\ 2 G_4 & : [X, \mathbf{B}^3 U(1)_{conn}] \to [X, \mathbf{B}^3 U(1)] \end{aligned} \,.$

In terms of this notation, that constraint equation to be satisfied by the three type of fields which I mentioned, the “flux quantization condition”, says that

$\frac{1}{2}p_1(\phi_{gr}) + 2 a(\phi_{ga}) = 2 G_4(\phi_{hg}) \,.$

This is just some equation in the set $[X, \mathbf{B}^3 U(1)]$ (which happens to come equipped with the structure of an abelian group,with respect to which the addition in the above equation is formed), for the present discussion it is not important what this means, as long as you can imagine that it may happen that three gauge fields are related by some such equation.

Given all this now, one might naïvely think that the *collection of fields that satisfy the flux quantization condition* is the set that in traditional ZFC logic one denotes by the right hand side of

$CField(X) := \left\{ \phi_{gr}, \phi_{ga}, \phi_{hg} | \frac{1}{2}p_1(\phi_{gr}) + 2 a(\phi_{ga}) = 2 G_4(\phi_{hg}) \right\} \,.$

However, this answer turns out to be physically wrong.

There are some evident deficiencies: this answer does not resolve the gauge transformations between fields and is hence unsuited for describing the actual quantum physics of the problem. But it is worse than that. In the correct answer there is yet one more field on $X$.

## Formulation in $\infty$-logic / homotopy type theory

Where is that extra field supposed to come from if we are imposing a constraint equation, thus seemingly *reducing* the degrees of freedom?

The answer is of course in the notion of *homotopy* or *gauge transformation*, which ordinary logic ignores. But this is precisely what homotopy type theory corrects. The *same* symbolic logical expressions are interpreted by homotopy type theory in a way that makes them *correct for higher gauge theory*. Automatically.

In that article we discuss how those “sets” of field configurations, $[X, \mathbf{B}Spin_{conn}]$ etc., are in fact objects not of $Set$, but of some (∞,1)-topos: they are smooth moduli ∞-stacks.

In the language of homotopy type theory the statement that there is a field configuration of, say, gravity

$\phi_{gr} \in [X, \mathbf{B}Spin_{conn}]$

becomes the statement that $\phi_{gr}$ is a term of type $[X, \mathbf{B}Spin_{conn}]$. Of course that’s just terminology.

Now comes the key point: we form now the solution set to the flux quantization condition as we did before. But now we do so in homotopy type theory. This means we use *precisely the same logical symbols* as before, which I repeat for emphasis on the right of

$\mathbf{CField}(X) \coloneqq \left\{ \phi_{gr} , \phi_{ga} , \phi_{hg} | \frac{1}{2}p_1(\phi_{gr}) + 2 a(\phi_{ga}) = 2 G_4(\phi_{hg}) \right\} \,,$

where now the boldface on the left is to indicate that we take this expression no longer to evaluate to a set (a subset of $[X, \mathbf{B} Spin_conn] \times [X, \mathbf{B} E_8] \times [X, \mathbf{B}^3 U(1)_{conn}]$), but now to a homotopy type. In fact, thus, to a smooth ∞-stack.

Taken apart, the above notation in homotopy type theory means

the dependent sum $\{ \cdot \; | \; \cdots \}$

over the product type $[X, \mathbf{B} Spin_conn] \times [X, \mathbf{B} E_8] \times [X, \mathbf{B}^3 U(1)_{conn}]$

of (and that’s the key) the dependent identity type $Id_{[X, \mathbf{B}^3 U(1)]}$.

Here is where homotopy type theory automatically does some work for us that is quite non-trivial from the classical point of view: this type $\mathbf{CField}(X)$ automagically comes out as the homotopy pullback of $(\frac{1}{2} p_1 + 2 a)$ along $2 G_4$, the homotopy-universal way of completing the following diagram:

$\array{ \mathbf{CField}(X) &\stackrel{}{\to}& [X, \mathbf{B}^3 U(1)_{conn}] \\ \downarrow &\swArrow_{\simeq}& \downarrow^{\mathrlap{2 \mathbf{G}_4}} \\ [X, \mathbf{B}Spin_{conn} \times \mathbf{B}E_{8}] &\underset{\frac{1}{2}\mathbf{p}_1 + 2 \mathbf{a}}{\to}& [X, \mathbf{B}^3 U(1)] }$

of smooth $\infty$-stacks, up to that gauge transformation indicated as the double arrow filling the diagram.

That this is so, hence that in type theory with identity types dependent sums over identity types express in fact homotopy pullbacks, is not entirely obvious, a priori, and is one of the hallmarks of what makes homotopy type theory interesting. (For technical details see here.)

In our example, the claim is that this homotopy type $\mathbf{CField}(X)$ is the correct “type of $C$-field configurations”, being the answer to a subtle question in string theory. So in conclusion, amplifying the argument of our section 2 just a bit more with an emphasis on the homotopy-logic we find: formulating a higher gauge theoretic problem as one would naively, but then reading the result in the logic of homotopy type theory, automatically takes care of otherwise subtle phenomena.

## Outlook

What do we learn from the existence of homotopy type theory?

There is the explicit lesson, which drives the whole interest, it says: with just a tiny little adjustment (allowing for identity types), traditional logic / type theory is a language that captures homotopy theory.

But inside this there might be another lesson of potentially more interest in common practice. That says: not only is there *some* formal language to capture homotopy theory. No, moreover: it’s a *natural* language, potentially more natural than the language you have been using so far, and speaking this language may help to make more transparent phenomena in homotopy theory that are less transparent otherwise.

Or so it *feels*. I would like to see this materialize in more detail. Therefore I close with a question:

Can you come up with more examples where thinking about situations in homotopy theory / in higher topos theory concretely profits from reformulating them from a homotopy-*logical* perspective? Some construction of natural interest involving various homotopies, homotopy pullbacks, homotopy pushouts, etc where you can step back and say: look, with homotopy type theory we can equivalently think of this as expressing the following logical formula, and this is much simpler than the original formulation?

Many of the basic definitions of Voevodsky’s in the foundation files of homotopy type theory are of the form that I am after here. For instance that the geometric procedure of giving a contracting homotopy of an $\infty$-stack $X$ is equivalent to the homotopy-logical procedure of proving $\exists_{x \in X} \forall_{y \in X} (x = y)$ (see at *contractible type* for details) might be taken as an example.

Or consider the notion of free loop space objects (“derived loop spaces”) $\mathcal{L} X$ of an $\infty$-stack $X$. Often these are heuristically motivated as formalizing the idea that a point in them is given by “making two points in $X$ equal in two different ways” (such as to yield a loop). In terms of homotopy type theory, this heuristics becomes a theorem, which reads:

$\mathcal{L}X = \left\{ x,y : X \; | \; (x = y) \, and \, (x = y) \right\} \,.$

These first simple examples seem to suggest that there is a whole universe of similar, but more interesting (*even* more interesting, if you wish), homotopy-logical reformulations of familiar phenomena in homotopy theory… and hopefully eventually of unfamiliar and previously unknown phenomena. Eventually I want to collect such examples at a page like *HoTT methods for homotopy theorists*.

## Re: What is homotopy type theory good for?

This is very nice! It makes lots of sense why the ZFC-answer is wrong; although I don’t know exactly what it means to “resolve” gauge transformations, I can guess that it has something to do with invariance under gauge transformations, which that set is manifestly not. But can you say anything, at this level of precision, about why the homotopy-motivated answer is physically “correct” (or what that even means)?

I think this sort of thing also supports my argument that identity/path types in homotopy type theory should be denoted simply by an equals sign “$(x=y)$” as you are doing here, rather than something fancier like $Id(x,y)$ or $Paths(x,y)$ or $(x\rightsquigarrow y)$. It may take a little bit of getting used to, but any time you wanted to write “$=$” when talking about non-0-truncated types you almost certainly really meant to talk about paths/equivalences anyway, so why proliferate notations unnecessarily?