Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

May 10, 2012

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 8E_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 XX 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.

  1. Since all of them are gauge fields, there is no naive notion of equality between different field configurations. Instead, there is a sensible notion of 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.)

  2. 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 CC-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,BSpin conn] [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,BE 8][X, \mathbf{B}E_8] of configurations of the gauge field. And a set, to be denoted, [X,B 3U(1) conn][X, \mathbf{B}^3 U(1)_{conn}], of configurations of (part of) the CC-field. So we’d write

ϕ gr [X,BSpin conn] ϕ ga [X,BE 8] ϕ hg [X,B 3U(1) conn] \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):

12p 1 :[X,BSpin conn][X,B 3U(1)] 2a :[X,BE 8][X,B 3U(1)] 2G 4 :[X,B 3U(1) conn][X,B 3U(1)]. \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

12p 1(ϕ gr)+2a(ϕ ga)=2G 4(ϕ hg). \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,B 3U(1)][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):={ϕ gr,ϕ ga,ϕ hg|12p 1(ϕ gr)+2a(ϕ ga)=2G 4(ϕ hg)}. 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 XX.

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,BSpin conn][X, \mathbf{B}Spin_{conn}] etc., are in fact objects not of SetSet, 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

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

becomes the statement that ϕ gr\phi_{gr} is a term of type [X,BSpin conn][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

CField(X){ϕ gr,ϕ ga,ϕ hg|12p 1(ϕ gr)+2a(ϕ ga)=2G 4(ϕ hg)}, \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,BSpin conn]×[X,BE 8]×[X,B 3U(1) conn][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

  1. the dependent sum {|}\{ \cdot \; | \; \cdots \}

  2. over the product type [X,BSpin conn]×[X,BE 8]×[X,B 3U(1) conn][X, \mathbf{B} Spin_conn] \times [X, \mathbf{B} E_8] \times [X, \mathbf{B}^3 U(1)_{conn}]

  3. of (and that’s the key) the dependent identity type Id [X,B 3U(1)]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 CField(X)\mathbf{CField}(X) automagically comes out as the homotopy pullback of (12p 1+2a)(\frac{1}{2} p_1 + 2 a) along 2G 42 G_4, the homotopy-universal way of completing the following diagram:

CField(X) [X,B 3U(1) conn] 2G 4 [X,BSpin conn×BE 8] 12p 1+2a [X,B 3U(1)] \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 CField(X)\mathbf{CField}(X) is the correct “type of CC-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 XX is equivalent to the homotopy-logical procedure of proving xX yX(x=y)\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”) X\mathcal{L} X of an \infty-stack XX. Often these are heuristically motivated as formalizing the idea that a point in them is given by “making two points in XX equal in two different ways” (such as to yield a loop). In terms of homotopy type theory, this heuristics becomes a theorem, which reads:

X={x,y:X|(x=y)and(x=y)}. \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.

Posted at May 10, 2012 12:33 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2526

48 Comments & 0 Trackbacks

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)(x=y)” as you are doing here, rather than something fancier like Id(x,y)Id(x,y) or Paths(x,y)Paths(x,y) or (xy)(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?

Posted by: Mike Shulman on May 10, 2012 4:12 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

I don’t know exactly what it means to “resolve” gauge transformations,

I should probably try to come up with a better way to phrase this. It is just supposed to mean that forming the intersection at the level of sets clearly cannot tell you about the higher homotopy type.

Let’s see, maybe you can help me with an idea for how to say this at a chatty level such that it is still useful: I simply want to highlight at that point in a non-technical way that when you have a cospan of higher groupoids and look at the pullback of just the underlying sets of 0-cells, then qualitatively there are two things that go wrong: not only is the resulting set not invariantly meaningful without looking at the higher cells, too, but it is also “too small” in that its elements are equalities between pairs of points in the tip of the cospan, instead of equivalences there.

But can you say anything, at this level of precision, about why the homotopy-motivated answer is physically “correct” (or what that even means)?

The way this works is a kind of reverse-engeneering from available data: one is looking for a sensible mathematical structure such that several truncations or limits of it match certain insights that had been obtained before.

To briefly start with a historical analogy: how do we know that our mathematical model of the electromagnetic field is physically correct? We collect the required properties in various areas where it appears. First, in the classical limit it exerts forces whose force vectors arrange into a closed differential 2-form. So the electromagnetic field mathematically must be something involving a closed 2-form. Next, 70 years later it is discovered that it also must be a rule that consistently assigns values in the circle group to curves in spacetime. After a little fiddling one finds that there is a mathematical structure naturally unifying these two aspects which is the thing that in the above notation has BU(1) conn\mathbf{B}U(1)_{conn} as its moduli stack. So this is a “physically correct” mathematical structure. Finally, one sees that it is also “more physically correct” than the parts that it unifies, because it turns out to deal with further relevant physical phenonema (flux quantization etc.).

For the supergravity C-field there were similarly partial constraints known: first, it was known that it involves a closed differential 3-form. Then that it must be a rule to assign values in U(1)U(1) cosistently to 3-volumes in space. By comparison with the previous case that seemed to indicate that it is the thing classified by B 3U(1) conn\mathbf{B}^3 U(1)_{conn}. But then it turned out that there were more datapoints: a certain piece of the “quantum corrected action functional” for the C-field only made sense as a function on just gauge equivalence classes if that “flux quantization condition” holds. And finally it was known that when restricted to a boundary of spacetime the whole structure had to naturally transmute into a certain other structure.

It’s a bit like with the proverbial Elephant that Johnstone appeals to, only that this Elephant is not topos theory but, hm, M-theory or the like: there are facets that are known and one checks how the next puzzle piece would fit in.

So concerning the C-field the task was: can you write down a natural mathematical structure that looks essentially like B 3U(1) conn\mathbf{B}^3 U(1)_{conn}, but with a little twist built in such that some constraint equation holds and such that relative cohomology with coefficients in this beast (meaning: restriction to boundaries) has certain properties.

Earlier there has been the observation that one can manufacture by hand a certain discrete 1-groupoid approximation to what I am calling CField(X)\mathbf{CField}(X) that has most of these desired properties, except that, being a discrete 1-groupoid, it still must have been some truncation and restriction of the full moduli \infty-stack.

So then the construction that we consider, the one that homotopy type theory produces from feeding the available datapoints into it, does produce somehting that is a smooth moduli \infty-stack, such that restricted to all these known special cases and limits it reproduces what it has to reproduce, and in this sense is “physically correct”. And moreover it is “more physically correct” than the previous constructions, which did not give full moduli 3-stacks, because of yet one more datapoint: for quantization of gauge theories we do need these higher stacks, or at least their infinitesimal approximation (known as “BRST complexes”).

Posted by: Urs Schreiber on May 10, 2012 10:15 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

So a pretty simple way to illuminate

when you have a cospan of higher groupoids and look at the pullback of just the underlying sets of 0-cells, then qualitatively there are two things that go wrong,

would be by looking at the pullback of one mapping of a point into a circle along another. Done wrongly you find either a point or the empty set. Done properly you’ll have something equivalent to BB \mathbb{Z}.

Posted by: David Corfield on May 10, 2012 5:12 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

So a pretty simple way to illuminate

Yes, that’s about the simplest non-trivial example.

Done properly you’ll have something equivalent to B\mathbf{B}\mathbb{Z}.

You mean the circle is B\mathbf{B}\mathbb{Z}, the homotopy pullback *× B*\ast \times_{\mathbf{B}\mathbb{Z}} \ast is ΩB\Omega \mathbf{B} \mathbb{Z} \simeq \mathbb{Z}!

Posted by: Urs Schreiber on May 10, 2012 5:18 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

That is, we replace both maps pt -> S^1 by surjective submersions R -exp-> S^1, and then the fiber product is R x Z. I think I’m getting it!

Posted by: Allen Knutson on May 10, 2012 6:28 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Just a remark on this here:

we replace both maps ptS 1pt \to S^1 by surjective submersions

This does come out right in this case, but it is a bit misleading to attribute it to the submersiveness of the map, isn’t it? There is really no smooth structure of relevance here, we are talking about the circle as an object of GrpdTop\infty Grpd \simeq Top. (I think. If we are talking about the smooth circle as S 1SmthMfdYonedaSmoothGrpdS^1 \in SmthMfd \stackrel{Yoneda}{\to} Smooth \infty Grpd then its categorical loop space is the point!)

What matters is that we replace one of the two point inclusions by a fibration in the relevant model category structure, so either by a Serre fibration if we choose to present B\mathbf{B}\mathbb{Z} by the topological circle S 1S^1, or by a Kan fibration if we choose to represent it by the nerve of the groupoid with a single object and \mathbb{Z} as its morphisms.

Details on how and why this computation works are at nLab: homotopy pullback - Concrete constructions - General. Lots of examples are also spelled out at nLab:homotopy limit.

Posted by: Urs Schreiber on May 10, 2012 7:00 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Urs wrote

You mean…

Whoops, of course.

Posted by: David Corfield on May 11, 2012 9:43 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

It is just supposed to mean that forming the intersection at the level of sets clearly cannot tell you about the higher homotopy type.

Hmm, but you want to say that somehow without the words “higher homotopy type”? Seems tricky… you could just say “contains too few data.”

Thanks for the explanation of the physical background!

Posted by: Mike Shulman on May 10, 2012 5:21 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

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)Id(x,y) or Paths(x,y)Paths(x,y) or (x⇝y).

Yes, I was thinking about that, too, when this idea here was ripening. It certainly has its appeals.

It is closely related to whether or not one uses the “\infty“-prefix in higher category theory. While emphasis may demand it, eventually it is more natural to just drop it and instead invent a prefix for when we explicitly do not mean the higher case.

But with HoTT being an internal language it seems more natural, even, not to change the symbols here.

Posted by: Urs Schreiber on May 10, 2012 10:44 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Here is another, maybe amusing, example of the use of homotopy-logic, and another reason, maybe, for the “notational conservatism” discussed above.

For some nn \in \mathbb{N}, consider the type B nU(1):\mathbf{B}^n U(1) : Smooth∞Grpd (where I am adoping the habit of naming the object classifier TypeType after the ambient \infty-topos) which classifies smooth circle nn-bundles / bundle (n-1)-gerbes.

Then the type B nU(1) conn\mathbf{B}^n U(1)_{conn} which classifies circle nn-bundles with connection aka ordinary differential cocycles of degree (n+1) has (details are here) the following homotopy-logical expression

B nU(1) conn{PB nU(1),FΩ cl n+1|curv(P)=F}. \mathbf{B}^n U(1)_{conn} \simeq \left\{ P \in \mathbf{B}^n U(1), F \in \Omega^{n+1}_{cl} | curv(P) = F \right\} \,.

In homotopy-words: a circle nn-bundle with connection is a circle nn-bundle and an identification of its curvature with a closed (n+1)(n+1)-form.

And that’s now an accurate theorem characterizing the moduli nn-stack for differential cohomology. This has a certain charme to it.

We can also massage this to read in a maybe even more enjoyable form. For that, first a preliminary: We previously had here (somewhere, I forget in which thread) discussion where I said I am enjoying to strictly regard the notation

  • {x:X|P(x)}\{ x : X | P(x) \}

and

  • x:X.P(x)\exists_{x : X} . P(x)

as synonymous in homotopy type theory, instead of reading the latter as being the bracket type/(-1)-truncation of the former (links for eventual bystanders).

I understand that this is not what Coq or some other system does, but I will happily ignore this and take the standpoint that this is Coq’s problem and not mine. Because I find it is a very nice unification that constructively and with higher homotopy types around, I may perfectly identify these two expressions. This seems to be a nice feature that I don’t feel like “correcting” by talking about support, bracket types and (-1)-truncation. I can talk about all that still when I really really need to form a (-1)-truncation. But when would that be?

Okay, so if I allow myself this, then I can write the moduli nn-stack for ordinary differential cohomology in degree (n+1)(n+1) equivalently as

B nU(1) conn{PB nU(1),| FΩ cl n+1.curv(P)=F}. \mathbf{B}^n U(1)_{conn} \simeq \left\{ P \in \mathbf{B}^n U(1), | \exists_{F \in \Omega^{n+1}_{cl}} . curv(P) = F \right\} \,.

This homotopy-logical theorem now reads in words: a circle nn-bundle with connection is a circle nn-bundle such that its curvature is a closed (n+1)(n+1)-form.

Not sure if this is very useful, but it is kind of fun!

One can play this game with each item in the “table of twisted cohomologies”. For instance the evident formal expression for the simple sentence

For αH 3(X,)\alpha \in H^3(X, \mathbb{Z}), an α\alpha-twisted KK-cocycle is a projective unitary bundle and an identification of its Dixmier-Douady class with α.\alpha.

is now (or compiles to, under homotopy type theory) a rigorous characterization of the stack whose connected components are twisted K 0K^0.

Posted by: Urs Schreiber on May 10, 2012 4:01 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Hmm, I see that now you want to also take the propositions as types point of view on the existential quantifier. Many type theorists of course do this all the time, as does Agda. (Coq’s “Prop” is sort of like a bracket type, but not entirely consistently so.)

I’m not yet convinced by the argument to use PAT terminology. Using == to mean isomorphism is not a problem because there is no other internally meaningful notion of “equality” between inhabitants of higher types. And many mathematicians have long recognized this by “sloppily” using the symbol == to denote isomorphism informally already.

But outside of the small circle of constructive type theorists who subscribe to PAT, mathematicians universally distinguish between “the collection of xx such that P(x)P(x)” and “the collection of xx together with pP(x)p\in P(x)”, and both are meaningful and useful things to consider in homotopy type theory. If we use “such that” to mean “together with”, then we are left without a good phrase which means “such that”; we have to resort to some clumsy thing like putting brackets around our sentence.

“Such that” types are everywhere in mathematics, so if homotopy type theory is to be a foundation for all of mathematics (not just a few narrow fields), then it needs a good language for them. But as an example of where the ability to actually say “such that” may be useful for the specific sorts of things you are interested in, consider for a type XX the type

{A:Type|A is equivalent to X} \{ A : Type \; | \; A \;\text{ is equivalent to }\; X \}

which you could write more formally as

A:Type[AX] \sum_{A: Type} [A\simeq X]

The “together with” version of this type is (assuming univalence) contractible. But the “such that” version is the classifying space of bundles with fiber AA.

Posted by: Mike Shulman on May 10, 2012 5:20 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

I see, good. Okay, you have convinced me!

But one question: in you last sentence, aren’t you mixing up the “such that”-version and the “together with”-version?

We have BAut(X)\mathbf{B} Aut(X) is the “collections of AAs together with an equivalence to XX”.

Posted by: Urs Schreiber on May 10, 2012 5:32 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

We have BAut(X)\mathbf{B}Aut(X) is the “collections of AAs together with an equivalence to XX.”

No, that’s the contractible one. The type

A:TypeEquiv(A,X)\sum_{A:Type} Equiv(A,X)

is equivalent, by univalence, to

A:Type(A=X)\sum_{A:Type} (A=X)

which is contractible; it’s the mapping path space of A:1TypeA : 1\to Type. It’s only when you add the bracket-type that it becomes BAut(X)\mathbf{B}Aut(X).

Posted by: Mike Shulman on May 10, 2012 8:58 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

it’s the mapping path space

Ah! Thanks, now I see where I went wrong.

So in the categorical semantics, we have the pullback

A(A=X) * X (BAut(X)) I BAut(X) Type BAut(X) \array{ \sum_{A} (A = X) &\to& * \\ \downarrow && \downarrow^{\mathrlap{}} & \searrow^{\mathrlap{X}} \\ (\mathbf{B}Aut(X))^I &\to& \mathbf{B}Aut(X) &\to & Type \\ \downarrow \\ \mathbf{B}Aut(X) }

And then the bracket type version is the (-2)-truncation of the total left vertical composite! Right? Hence BAut(X)\mathbf{B}Aut(X).

Posted by: Urs Schreiber on May 10, 2012 10:59 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Great stuff! I’ll write something more substantial later, but as a quick sanity check Id [C,B 3U(1)]Id_{[C, B^3 U(1)]} in part 3 of the analysis of CFieldCField should be Id [X,B 3U(1)]Id_{[X, B^3 U(1)]}?

And where you write

In the correct answer there is yet one more field on XX,

you mean that rather than think of CField(X)CField(X) as just a subset of the product of three fields, we should see it as a new field in itself?

Posted by: David Corfield on May 10, 2012 9:55 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

but as a quick sanity check

Yes, that was a typo. I have fixed it now. Thanks for spotting it!

we should see it as a new field in itself?

Yes. I realize that this is a point that maybe the above text should spend a tad more time on.

So the thing is that the extra homotopy in the homotopy pullback of fields is visible itself as a field!

Here a few more details. I’ll do this for the case that the thing called G 4G_4 vanishes, which is the relevant boundary case (and this and more is all explained in the article).

So we have the field of gravity, ϕ gr\phi_{gr}, and it induces another field called 12p 1(ϕ gr)\frac{1}{2}p_1(\phi_{gr}). This has a field strength, which is a closed 4-form, to be denoted F ωF ω\langle F_\omega \wedge F_\omega\rangle.

And then there is an E 8E_8 gauge field, which induces another field called a(ϕ ga)a(\phi_{ga}), also with its field strength 4-form, now called F AF A\langle F_A \wedge F_A\rangle.

The homotopy pullback that we are talking about makes these two 4-forms become equivalent as 4-forms, by an explicit equivalence. An equivalence of closed 4-forms is a 3-form, call it HH, such that its de Rham differential dHd H is the difference of the two 4-forms

dH=F ωF ωF AF A. d H = \langle F_\omega \wedge F_\omega \rangle - \langle F_A \wedge F_A\rangle \,.

So HH here is the equivalence between the two “pre-existing” fields, but this is now interpreted itself as a field: the field strength of the (twisted) “B-field”.

Posted by: Urs Schreiber on May 10, 2012 10:30 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

So the B-field is in [X,B 2U(1)][X, \mathbf{B}^2 U(1)]? Has this been induced from somewhere like 12p 1(ϕ gr)\frac{1}{2}p_1(\phi_{gr}) was induced from ϕ gr\phi_{gr}?

Posted by: David Corfield on May 11, 2012 12:35 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

So the B-field is in [X,B 2U(1)][X, \mathbf{B}^2 U(1)]?

That’s going in the right direction. More precisely it’s like this:

Like the C-field, the B-field experiences various “twists” in general, depending on which type of string theory we look at (type II or heterotic) and depending on which other fields are present, because they all influence each other.

But, yes, in the plain vanilla version the B-field is a connection on a circle 2-bundle = bundle gerbe and as such is a term

ϕ B[X,B 2U(1) conn]. \phi_B \in [X, \mathbf{B}^2 U(1)_{conn}] \,.

(I should decide whether I want to write (XA)(X \to A) or [X,A][X,A] for function types here. While I am still undecided, keep in mind that both notations stand for precisely the same thing.)

Here the subscript “ conn{}_{conn}” indicates the differential refinement, the connection. There is a forgetful morphism

u:B 2U(1) connB 2U(1) u : \mathbf{B}^2 U(1)_{conn} \to \mathbf{B}^2 U(1)

which forgets the connection and just remembers the underlying 2-bundle / bundle gerbe or physically: roughly, the underlying “instanton sector”

u(ϕ B)[X,B 2U(1)]. u(\phi_B) \in [X, \mathbf{B}^2 U(1)] \,.

You ask:

Has this been induced from somewhere like 12p 1(ϕ gr)\frac{1}{2}p_1(\phi_{gr}) was induces from ϕ gr\phi_{gr}.

Something like this does happen in backgrounds for the type II superstring, yes.

Where in the heterotic string the twist that governs the anomaly cancellation (as it were) is the second Chern class

c 2:BSUB 3U(1) \mathbf{c}_2 : \mathbf{B} SU \to \mathbf{B}^3 U(1)

or rather its differential refinement

c^ 2:BSU connB 3U(1) conn \hat \mathbf{c}_2 : \mathbf{B} SU_{conn} \to \mathbf{B}^3 U(1)_{conn}

for the type II string the corresponding twist is given by the Dixmier-Douady class

dd:BPUB 2U(1). \mathbf{dd} : \mathbf{B} PU \to \mathbf{B}^2 U(1) \,.

In words and physically this means: a gauge field for the stable projective unitary group (namely on a D-brane) “induces” a B-field. Yes.

And in this case there is also a similar “constraint equation” which says that this induced field must equal the difference of two other induced fields.

Posted by: Urs Schreiber on May 11, 2012 4:03 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Here’s a problem that doesn’t directly have anything to do with gauge theory, but does involve some (possibly not so) exact complexes and in my vague understanding, nn-stuff shows up whenever complexes appear. Would this formalism have an application here?

Consider the following commutative square of linear differential operators

(1)Γ SC(F) c Γ SC(G) f g Γ SC(F˜ *) d Γ SC(G˜ *) \begin{matrix} \Gamma_{SC}(F) & \overset{c}{\longrightarrow} & \Gamma_{SC}(G) \\ \downarrow\mathrlap{\scriptsize{f}} & & \downarrow\mathrlap{\scriptsize{g}} \\ \Gamma_{SC}(\tilde{F}^*) & \underset{d}{\longrightarrow} & \Gamma_{SC}(\tilde{G}^*) \end{matrix}

The notation is as follows. FMF\to M and GMG\to M are vector bundles, dimM=n\dim M = n. F˜ *F * MΩ nM\tilde{F}^* \cong F^*\otimes_M \Omega^n M are densitized dual bundles, so that point-wise contraction and integration gives a natural pairing between sections of FF and F *F^*. Similarly for G *G^*. Γ SC(F)\Gamma_{SC}(F) and Γ SC(G)\Gamma_{SC}(G) denote the spaces of smooth sections with spatially compact support (contained in the domain of influence of a compact set). The vertical maps are hyperbolic (one can define two sided inverses with advanced and retarded supports, Green functions ±\mathcal{F}_\pm and 𝒢 ±\mathcal{G}_\pm). The horizontal maps are “elliptic” in the sense that they could be extended to “elliptic” complexes

(2)c 1Γ SC(F)cΓ SC(G)c 1 \cdots \overset{c_{-1}}{\longrightarrow} \Gamma_{SC}(F) \overset{c}{\longrightarrow} \Gamma_{SC}(G) \overset{c_1}{\longrightarrow} \cdots

and similar for dd, with finite dimensional cohomology.

When the constraints cc are ignored and ff is globally hyperbolic on MM, the kernel, image and cokernel of ff are nicely characterized by the following exact sequence:

(3)0Γ 0(F)fΓ 0(F˜ *) + Γ SC(F)fΓ SC(F˜ *)0, 0 \to \Gamma_0(F) \overset{f}{\to} \Gamma_0(\tilde{F}^*) \overset{\mathcal{F}_+ - \mathcal{F}_-}{\longrightarrow} \Gamma_{SC}(F) \overset{f}{\to} \Gamma_{SC}(\tilde{F}^*) \to 0 ,

where Γ 0(F)\Gamma_0(F) consists of sections with compact support.

Now, taking cc into account, the challenge is to characterize the spaces kerfkerc\ker f\cap \ker c, im(fc)\im(f\oplus c) and coker(fc)\coker(f\oplus c). Is there some neat higher categorical/homotopy-type way of doing that using the elliptic complexes that extend cc and dd?

Posted by: Igor Khavkine on May 11, 2012 2:32 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Hi Igor,

I see what you are getting at. Something at least closely related can be said:

Using homotopy type theory gives a very conside and neat way of speaking about the BV-BRST formalism in a homotopy-true way.

(Note to bystanders: this and other links I provide for the sake of other readers, not for Igor. Igor is a co-author of that page.)

More precisely, homotopy type theory gives a natural automatic way to speak about derived critical loci.

So consider some configuration space of fields, which for definiteness and for comparison with the other discussion here I take to be of the form

Conf=(XA), Conf = (X \to A) \,,

i.e. to be a “function type” (in HoTT language) of maps from spacetime XX to some moduli type of field configurations. For instance if AA is a Riemannian manifold, then this might be the space of field configurations of a standard sigma-model. Or if A=BG connA = \mathbf{B}G_{conn} is a moduli stack of connections, then this would be the configuration stack of a gauge theory.

So then an action functional

S:(XA)𝔸 1 S : (X \to A) \to \mathbb{A}^1

is now a term of function type (XA)𝔸 1(X \to A) \to \mathbb{A}^1. If we assume a suitable differential geometric context, then this induces a term of function type

dS:(XA)T *(XA), d S : (X \to A) \to T^* (X \to A) \,,

its differential.

The corresponding covariant phase space P BVP_{BV} in its incarnation as a derived critical locus / BV-complex is the homotopy fiber of this dSd S over 0, assuming that we interpret all of this in a “derived” \infty-topos.

Hence formulating the discussion at derived critical locus in the language of homotopy type theory, yields the following evident expression as a theorem:

P BV={ϕ:XA|(dS ϕ=0)}. P_{BV} = \left\{ \phi : X \to A \;\; | (d S_\phi = 0) \right\} \,.

Or, as Mike insists, equivalently

P BV= ϕ:XA(dS ϕ=0). P_{BV} = \sum_{\phi : X \to A} (d S_{\phi} = 0) \,.

This is the kind of trick that homotopy type theory achieves for us: this expression looks precisely like the naive definition of the ordinary covariant phase space, which is simply the “subset of points” of configuration space on which the Euler-Lagrange equation dS=0d S = 0 holds.

But homotopy type theory automatically “compiles” this to the homotopy-correct statement and makes it be the derived covariant phase space / the derived critical locus, hence the full BV-complex.

This is actually a very good example for the theme of the above post. Thanks for bringing this up.

Posted by: Urs Schreiber on May 11, 2012 3:31 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

I wrote:

Or, as Mike insists, equivalently P BV= ϕ:XA(dS ϕ=0)P_{BV}= \sum_{\phi : X \to A} (d S_\phi = 0)

In fact this notation is maybe noteworthy in this context: it manifestly exhibits the BV-complex / derived covariant phase space as a homotopy-theoretic path integral .

Posted by: Urs Schreiber on May 11, 2012 3:37 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

as Mike insists

The main thing I have a problem with is using “\exists” to mean \sum. The notation {...|...}\{ ... | ... \} I don’t have as strong feelings about. Traditionally in mathematics it’s used only when the thing on the right is a proposition, but if we put something that isn’t a proposition there I don’t think there is any ambiguity. That is, I don’t think the traditional notation includes an implicit bracket around the thing on the right; rather, in ordinary set theory the notation would be considered ill-formed if the thing on the right were not a proposition.

Coq uses {...&...}\{ ... \& ... \} when the thing on the right is not in PropProp; we could adopt that too. Either of these notations does have the advantage over \sum that often the thing on the left is as or more important as the thing on the right, and in a \sum notation that one gets stuck into a subscript.

Posted by: Mike Shulman on May 11, 2012 5:12 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Actually, I was deliberately obscure about the origin of the above construction to see if it would be independently recognized as a kind of pattern that you guys might be familiar with. A concrete example might clarify what I’m talking about.

Consider a 1-form A μA_\mu on a Lorentzian manifold that satisfies Euler-Lagrange equations of the Proca action functional. An equivalent way of writing these equations is the pair A μm 2A μ+(curvatureterm)=0\square A_\mu - m^2 A_\mu + (\mathrm{curvature term})=0, μA μ=0\nabla^\mu A_\mu = 0. The first is a massive wave equation (the ff operator in the abstract setting above), while the second is a constraint (the cc operator) (it would be called a “second class constraint” in the standard Hamiltonian classification). The other two operators, gg and dd, are can be found by “commuting” ff and cc. Their existence ensures that the the constraint μA μ\nabla^\mu A_\mu is consisten with the massive wave equation.

This system has no gauge invariance, so the ghost part of the BV formalism is trivial here. You can even forget about the fact that these equations came from an action functional. The challenge is just to characterize the space of solutions of the massive wave equation that also satisfy the constraints. In this case it’s not particularly difficult, but neither is solving the Maxwell equations modulo gauge transformations. In these situations, the constraints and the gauge transformations are rather simple. The complications appear for gauge systems when the gauge transformations become more complicated and have to be described by a non-trivial complex of differential operators, which gives rise to the whole hierarchy of ghosts of ghosts. Similarly, when the constraints cc are not all independent, their degeneracies would be described by the ellptic complexes that extend the operators cc and dd in my previous post.

I see a certain parallel here between gauge transformations and constraints. Both may be complicated enough to have to be resolved by a complex of differential operators. Though for gauge transformations, the complex extends to the left, while for constraints the complex extends to the right. I wonder if this fancy machinery that already applies to the gauge setting can apply to setting of constraints as well.

Posted by: Igor Khavkine on May 11, 2012 6:08 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

I wonder if this fancy machinery that already applies to the gauge setting can apply to setting of constraints as well.

To the extent that you cosider resolving your constraint surface by BV methods: yes. What I said above applies already to the case that there are no gauge symmetries.

Maybe to be more explicit: I don’t see how appealing to homotopy type theory can help with actually solving some equations. But if you do appeal to BV at all (gauge symmetries or not) there is the fact that the kind of up-to-homotopy construction that BV secretly is has a nice native formulation in homotopy type theory.

This is probably not what you are hoping for here, but it’s still kind of noteworthy.

Posted by: Urs Schreiber on May 11, 2012 6:49 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Right. I see what you are saying. But it is worth noting that the standard BV formalism (or its generalization to non-variational systems à la Lyakhovich et al) does not pay special attention to such “second class” constraints. That is a little unsatisfying. So, the lesson seems to be that if there is any application of higher categorical or homotopical methods here, it is yet to be found.

Posted by: Igor Khavkine on May 11, 2012 10:22 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Urs wrote:

How will homotopy type theory change our lives?

To me the most exciting thing was always the idea that topology is ‘logic turned into space’, as perhaps the name ‘topology’ was hinting all along. And this sort of realization seems bound to be important in physics, where we have these weird things called ‘space’ and ‘spacetime’ and ‘phase space’ that we’re trying to understand more deeply than we do now.

But a lot of mathematicians and physicists want to see concrete answers to questions of the form ‘how does X help me do Y?’ So it’s good to compile a list of examples.

Posted by: John Baez on May 13, 2012 3:22 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

topology is ‘logic turned into space’

That is crucially different from logic turned into homotopy types, though!

Posted by: Urs Schreiber on May 14, 2012 10:50 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

So is the idea of this post that many interesting constructions in specific (,1)(\infty, 1)-toposes can be thought of as general homotopy logic operations? Might there be cases where an interesting construction relies too specifically on the particularity of its (,1)(\infty, 1)-topos setting, so one wouldn’t count it as logical?

Won’t the examples you ask for just come from looking at what higher homotopy means in different (,1)(\infty, 1)-toposes? I guess your example looks especially striking as it’s not just any old pullback in SmoothGrpdSmooth \infty Grpd, but has a physical interpretation, where the higher homotopy is physically meaningful.

Posted by: David Corfield on May 13, 2012 3:44 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

So is the idea of this post that many interesting constructions in specific (∞,1)-toposes can be thought of as general homotopy logic operations?

No, this is the basic idea that already drives the existing interest: that homotopy type theory is presumeably the internal language of elementary (,1)(\infty,1)-toposes.

What I am after here is seeing examples of how this is useful beyond just interest in establishing this relation itself. Examples of where looking at constructions in homotopy theory, which we are interested in as homotopy theory, are illuminated by re-phrasing them in homotopy logic.

You may imagine me talking to students of homotopy theory who don’t care about symbolic logic, be it homotopy type theory or not, who see no reason to be interested in learning about homotopy type theory, maybe whose advisor advises them not to waste time with this fad, as there is nothing to be learned for homotopy theorists. The question is: what can one tell them apart from “right, nothing to be seen here, move on”?

The example I tried to give in this thread is supposedly one where a subtle problem in application of homotopy theory has a crstal clear solution once formulated systematically in homotopy type theory. It’s not quite an example where you can make progress only with homotopy type theory, after all we found the solution just from homotopy theoretic reasoning, too, but I notice that from the point of view of homotopy type theory it becomes even more elegant. So that’s satisfactory, for me at least. But I am quite suspecting that this is only the tip of the iceberg.

Posted by: Urs Schreiber on May 14, 2012 11:05 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Maybe your example is difficult to judge for a student of homotopy theory in that they won’t know enough about higher differential geometry to see whether you could have arrived at your construction most easily through: physical considerations; differential geometric/topological considerations; quasi-categorical considerations; or homotopy logical considerations.

Perhaps an example in TopTop would help. But I wonder whether this might be pushing against the flow of ideas. Couldn’t we see the dramatic changes as more to do with a flood of ideas coming out of homotopy theory to the rest of maths, by isolating concepts such as (,1)(\infty, 1)-toposes which surprisingly apply to areas such as differential and algebraic geometry. Or is that something has been added in the development of the internal language of homotopy type theory which will allow the debt to be somewhat repaid?

Posted by: David Corfield on May 14, 2012 11:57 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Maybe your example is difficult to judge for a student of homotopy theory

Yes, that example about the C-field is to motivate me :-)

For those students I hope to eventually prepare the page HoTT methods for homotopy theorists, which however is still at best in a nascent state. (But right now I need to be looking into something completely different, so this page has to wait a moment.)

There are hopefully two layers to this: one concerning lots of little tricks (hah!) as on that page (eventually), which are useful in everyday computation in homotopy theory and which haven’t found attention before the point of view of HoTT introduced them, the other concerning deeper research-level questions.

Couldn’t we see the dramatic changes as more to do with a flood of ideas coming out of homotopy theory to the rest of maths, by isolating concepts such as (∞,1)-toposes which surprisingly apply to areas such as differential and algebraic geometry.

I guess so, but what role is homotopy type theory to play in this?

For instance, Mike is proposing (hopefully I am stating it correctly) that homotopy type theory indicates that in elementary (,1)(\infty,1)-topos theory it is not the usual notion of (,1)(\infty,1)-colimits that are fundamental, as one would have expected, but that of \infty-initial \infty-algebras over presentable \infty-monads (as in our parallel discussion here). Both concepts will of course reflect on each others, but some things will be more natural with respect to the initial agebras, apart from this having a direct formalization in homotopy type theory.

So one way to answer my question here is: what would be interesting items in a list of examples for applications in traditional homotopy theory that are more elegantly expressed in terms of initial algebras of presentable \infty-monads, as opposed to in terms of just plain \infty-colimits?

Posted by: Urs Schreiber on May 14, 2012 12:55 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

I don’t think I would try to use this example to convince a homotopy theorist that homotopy type theory is useful. The direct homotopy-theoretic solution — take the homotopy pullback rather than the strict pullback — seems pretty obvious and doesn’t need any type-theoretic machinery.

in elementary (∞,1)-topos theory it is not the usual notion of (∞,1)-colimits that are fundamental, as one would have expected, but that of ∞-initial ∞-algebras over presentable ∞-monads

Yes, I think that’s roughly accurate. I think it sounds a little better (because seemingly more general) to talk about free algebras rather than initial algebras, though they are essentially the same. It’s not entirely clear to what extent the notion of “presentable \infty-monad” can be defined without already having usual (,1)(\infty,1)-colimits, though. (One could of course regard HITs themselves as a “definition” of presentable \infty-monads.)

what would be interesting items in a list of examples for applications in traditional homotopy theory that are more elegantly expressed in terms of initial algebras of presentable ∞-monads, as opposed to in terms of just plain ∞-colimits?

I’ve said this before, but I think that localization is near the top of that list. Classical algebraic topologists are constantly localizing Gpd\infty Gpd with respect to various things, like prime numbers, but the construction of such localizations is frequently very messy. In nice cases one can induct up the Postnikov tower, but in general one usually resorts to a small object argument. The fact that localization has a very clean description as a higher inductive type (even if that description “compiles out” in classical models to a small object argument) seems to me very suggestive. However, I don’t yet know of actual applications of this idea to something that a classical algebraic topologist would care about.

Posted by: Mike Shulman on May 14, 2012 6:59 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

I think that localization is near the top of that list.

Right, I have looked at that post every now and then, but still need to find some way to connect to it. What happens when I read that post is that I do follow how the code there formalizes localization, and I do apreciate the remarkable claim that you have given a Coq-checked proof that this gives indeed a reflection, but then I am maybe left wondering what I learn from this now as long as I don’t try to do some serious Coq programming myself (which seems unlikely anytime soon).

Let’s see. Maybe this here would help me: what is the induction principle and what is the recursion principle induced by this higher inductive type? I suppose the recursion principle is the universal property of precomposition with the the unit, hence with to_local?

What’s the induction principle? Is that something that is usefully made explicit? So we’d have first of all an XX-dependent type with a map to a (localizeX)(localize X)-dependent local type. And then compatible dependent terms of both. Hm, is that good for something?

(I should admit that don’t really have the leisure to think about this right now, so I am just rambling…)

Posted by: Urs Schreiber on May 14, 2012 11:58 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

I wrote:

So we’d have first of all an X-dependent type

Ah, no, that’s wrong. The endofunctor in degree 0 is sort of constant on XX.

Anyway, I have to go offline now. Would be happy to continue discussing this later, though.

Posted by: Urs Schreiber on May 15, 2012 12:26 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

That’s a good question. Unfortunately, the only general induction principle I know is not much more useful than the recursion principle. It basically says that if you have a type P(z)P(z) dependent on z:localize(X)z : localize(X), such that z:localize(X)P(z)\sum_{z: localize(X)} P(z) is local, then you have a section. I mentioned this sort of induction principle in the more general context of reflective subfibrations here.

A more useful induction principle would change the hypothesis to ask only that each type P(z)P(z) is local. Unfortunately this one isn’t valid for all localizations, only those that give rise to a stable factorization system. That does include all nullifications, i.e. localizations at maps of the form S1S\to 1. For instance, nn-truncation is nullification at the (n+1)(n+1)-sphere.

Posted by: Mike Shulman on May 15, 2012 7:42 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

In the comparison to the dot-com bubble, Urs writes

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

Obviously, one ought not push the comparison too far, or else we’d be looking to match the current moment to a point on the Nasdaq graph, presumably before that big spike at 2000.

But I was wondering, where can one hear speculations about the possible future impact of homotopy type theory other than at our places (nLab, Café), the Homotopy Type Theory site, and the Univalent Foundations site?

Presumably, there is also what is written in the informal parts of papers on (,1)(\infty, 1)-toposes by e.g., Lurie, Toën, Joyal, etc. Are you hearing a lot more than is written anywhere? Anything as daring as some of these 1999/2000 predictions for 2010?:

A fourth-grader on his way home from school will be able to punch a button on his bicycle that will “activate the microwave oven to heat his snack so it’ll be ready when he walks in the kitchen.” As he rides he’ll have one eye on a computer monitor on which he’s getting a head start on homework.– Charlotte News and Observer

or

Kids’ dolls, trucks and other toys will use artificial intelligence to talk and “evolve” with your child as he grows, a process you’ll be able to track dramatically with holographic photos. “Land line phones will be a thing of the past” and “there will probably be a single international currency.” – The Melbourne Herald Sun

Posted by: David Corfield on May 14, 2012 10:48 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

I remember chatting to an algebraic geometer at Kent a couple of years ago and trying to find out what level of category theory fed into his work. He knew of toposes but they didn’t feature in his research. He also had some idea of what derived algebraic geometry sought to achieve, but again with no felt need to find out more.

If we were to liken the situation today to some point in the foundational changes of the 1880-1930 period, is it that

Then: by, say, 1900, some of the avant garde had the idea that much (or all) of mathematics can be thought to be about sets or classes, and some also that there’s an (internal) formal language in which all mathematical reasoning can be cast.

Now: some of the avant garde have the idea that much (or all) of mathematics can be though to be about (,1)(\infty, 1)-toposes, and some also that there’s an (internal) formal language.

E.g., an avant garde expression of the future role of homotopy theory from David Ben-Zvi:

It is not that homotopy theory was to be a part of group theory, but as Quillen started to show the converse is true – currently a big swath of algebraic geometry can be seen as a special easy case of homotopy theory, but with great insight to be gained from the broader perspective. In fact it is apparent that algebraic geometers largely ignored homotopy theory only at great cost and that is beginning to change.

Homotopy theory is an incredibly rich beautiful subject with many overarching themes, large scale patterns, deep phenomena related to the most beautiful parts of number theory and geometry etc. It certainly has suffered from very bad salesmanship for a long time but Hopkins, Madsen, Lurie and others are changing that hopefully.

Even if this vision wins out, it doesn’t mean homotopy type theory will feature explicitly. Most people got by in the past with an informal grasp of mathematics as being about structured sets and a passing knowledge of predicate logic. These ideas weren’t mentioned to me in four years as an undergraduate at Cambridge in the 1980s, so presumably it was supposed that one could work perfectly effectively with no training in set theory or logic. Of course, all this doesn’t stop them being wonderful conceptual discoveries.

Posted by: David Corfield on May 15, 2012 9:44 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

I think the big difference to traditional (material) set theory is that this was never meant to be actually used explicitly in practice, but only served as a proof of principle. This is already different for structural set theory like ETCS, which is actually useful in practice. And it already goes a long way towards type theory, which to some extent takes the same basic idea and just formalizes it further, doesn’t it?

Posted by: Urs Schreiber on May 15, 2012 10:38 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Like Molière’s Monsieur Jourdain

Good Heavens! For more than forty years I have been speaking prose without knowing it,

it may be that people could be said to have been reasoning unknowingly in a structural set theoretic way for many years. But I’m wary of bringing that debate up again after the FOM experience.

Clearly a major change occurred between 1880 and 1930, for one thing in terms of a kind of homogenization of mathematics, so that it became much less surprising that different branches could speak to one another.

It is as if you took a man out of a milieu in which he lived not because it fitted him but from ingrained habits and prejudices, and then allowed him, after thus setting him free, to form associations in better accordance with his true inner nature. (Weyl)

I hope the homotopization of mathematics is as eventful, and that homotopy type theory plays an important role.

Posted by: David Corfield on May 15, 2012 12:51 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Hi David,

while I agree with what you say or indicate, I feel that somehow the issue that motivated me here is not entirely reflected in these comments of yours. Maybe I am wrong, but for the sake of clarity, let me try to emphasize a point which it feels you don’t quite address yet.

For instance you end with:

I hope the homotopization of mathematics is as eventful, […]

But I would say: the homotopization of mathematics has already been happily and eventfully been proceeding all along. That’s what the “nn” in the title of this blog here is meaning to pay tribute to, for instance.

What is new is that this homotopization has reached also the very foundations. The question that I meant to be highlighting in this discussion here is:

how does the homotopization of various areas that we are all already involved in profit from the fact that also the foundations are being homotopical now?

Do you see what I mean?

Another way might be to put it like this:

we (for some value of “we”) have long agreed that the language that the world is written in is higher category theory. What is new now is that suddenly we realize that this higher category theory has an equivalent reformulation which, while equivalent, looks more fundamental, even, to some extent.

The natural question (for me) is: what do we gain in practice by adopting that new viewpoint, that equivalent reformulation?

Posted by: Urs Schreiber on May 15, 2012 5:44 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

The natural question (for me) is: what do we gain in practice by adopting that new viewpoint, that equivalent reformulation?

It’s a very interesting question. You’ll have a much better sense of a good answer than I. What I’m naturally led to think about is what it was imagined formal mathematical languages of the past could achieve, and what they actually achieved.

Let’s sketch a list.

Security: the idea of a gapless proof, where no appeal to intuition need be given. E.g., no more discoveries of cases such as where Euclid presumes without stating that certain circles will intersect.

Proof theory: the idea that proofs themselves could be subjected to mathematical analysis.

Mechanization: certain inferences steps would become more or less automatic. Machines could be designed to do maths.

Carving concepts correctly: Frege imagined his Begriffsschrift could do this. He said that the earlier forms of logic just allowed you to join or intersect properties, but his allowed the formation of fruitful new concepts.

I haven’t heard anything much about the first two with respect to categorical type theory. I know there are category theoretic treaments of proof theory, e.g., M. E. Szabo, Algebra of Proofs, Studies in Logic and the Foundations of Mathematics, Vol. 88, North-Holland, 1978, but that’s category theory as proof theoretic tool, not proof theory about category theoretic proofs.

Concerning mechanization, I believe Voevodsky himself has suggested that mathematics could be automated with the adoption of homotopy type theory. I think I remain to be convinced.

It has always been the fourth, carving concepts correctly, that has intrigued me about category theory, though this is sometimes given the air of being fairly automatic. E.g., you here “turning the crank” to work out what a stabilzer of a sub-2-group must be. How to characterize such crank-turning? Can it be seen as operating a type theory?

I must admit to being a little disappointed over the years that general category theory hasn’t made greater inroads into mainstream maths by crank-turning in concrete realizations. At the Café when it was found that optimal transport was all about profunctors in an enriched category, I thought we would quickly reveal whether the optimal tranpsort people had chosen the optimal concepts.

There must be a heap of examples where X is working on a concept ignorant that Y has shown it to be a concrete realization of a category theoretic construction. Y doesn’t know what’s needed to make something of the observation, and X never finds out.

Choosing randomly a piece of recent general category theory, Mike’s work with Steve Lack on Enhanced 2-categories and limits for lax morphisms, is that dripping with possibilities of surprising concrete realizations?

Posted by: David Corfield on May 16, 2012 9:40 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Concerning mechanization,

I really cannot judge this. But I can point out that the mechanization of mathematics using type theory is proceeding independently of its homotopization. There is the project ForMath: Formalization of Mathematics led by Coquand. I have not much feel for this, but you might find it interesting to look around a bit on their list of publications, especially concerning the Slides-section towards the bottom of the page.

I recently went around and asked people who might know what would happen to these kinds of programs once the Coq code used there does or will make the homotopization explicit. After all, the point is that not too much is necessary to do so. Once it is shown that univalence is computationally good, it can be done in principle. What will happen then? What is the missing red entry on Mike’s slide number 4?

How to characterize such crank-turning? Can it be seen as operating a type theory?

Yes, that “crank turning” referred precisely to internalization. By the way, meanwhile Mike has proven that our two definitions of stabilizer infinity-group are equivalent, and he did so in homotopy type theory.

There must be a heap of examples where X is working on a concept ignorant that Y has shown it to be a concrete realization of a category theoretic construction.

Yeah, I like to collect such examples in my area of interest.

Posted by: Urs Schreiber on May 16, 2012 12:58 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Security: the idea of a gapless proof, where no appeal to intuition need be given.

Mechanization: certain inferences steps would become more or less automatic. Machines could be designed to do maths.

Type theory is actually even better at security than it is at mechanization, through the use of machines. It turns out to be easier to program a computer to verify that a proof is correct, than it is to program a computer to produce a proof automatically. Coq and Agda and other proof assistants which we use in type theory are doing exactly that, so we do have security guaranteed.

I feel like people talk about this quite a lot, although I guess maybe I haven’t emphasized it very much around here. But non-homotopical type theory is already being used in this way: for instance, the four-color theorem has been completely computer-verified, and work is in progress for various other complicated mathematical theorems whose correctness people are worried about. Voevodsky isn’t innovating here at all; it’s a well-established fact.

Proof assistants do also have a certain degree of automation, which can make “simple” steps be proven automatically. A computer’s definition of “simple” is not necessarily that of a human, though, so sometimes you end up having to spell out manually things that seem obvious, but other times the computer can just do something like magic and you aren’t entirely sure how it happened. However, this sort of automation is only going to get better. I wouldn’t go so far as to say that all of mathematics can be automated (and I haven’t personally heard Voevodsky claim that, though I wouldn’t be surprised if he has), but I think in 100 years, the process of doing mathematics will look radically different than it does today.

I would also have said that type theory is very closely related to proof theory. I’m not a proof theorist, but the terms that appear in type theory are exactly a “representation of proofs” which are used in proving proof-theoretic theorems like cut-elimination.

Posted by: Mike Shulman on May 16, 2012 4:48 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

I remember someone, was it John Power, telling me that it was no surprise that European computer science had gone down a path of assuring security through type-checking in typed languages, hence open to category theory, while the American approach primarily sought speed (or something like that).

Maybe there’ll be a proof theory for homotopy type theory, with relative consistency proofs, etc.

As for Voevodsky’s beliefs, he talks here of

a new era which will be characterized by the widespread use of automated tools for proof construction and verication.

I guess that’s not too radical. Call me old-fashioned, but I find what’s happening more interesting in terms of the production of new conceptual understandings.

Posted by: David Corfield on May 16, 2012 5:16 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Maybe there’ll be a proof theory for homotopy type theory

Since homotopy type theory is just intensional type theory with maybe a few extra axioms and rules, I would say that it already has a proof theory.

Posted by: Mike Shulman on May 17, 2012 1:09 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

But I would say: the homotopization of mathematics has already been happily and eventfully been proceeding all along. That’s what the “nn” in the title of this blog here is meaning to pay tribute to, for instance.

But that’s only partial, right? Beyond the great city of homotopization, there still lies the distant dream of categorification.

Posted by: David Corfield on May 16, 2012 9:48 AM | Permalink | Reply to this

Re: What is homotopy type theory good for?

Beyond the great city of homotopization, there still lies the distant dream of categorification.

I don’t find this distinction helpful. These are just two words for aspects of the same thing. Homotopization is (,1)(\infty,1)-categorification, and categorification is directed homotopization.

Instead of prolonging the schism, I’d rather see the mistake of making the distinction in the first place been buried and forgotten.

Posted by: Urs Schreiber on May 16, 2012 12:25 PM | Permalink | Reply to this

Re: What is homotopy type theory good for?

I’m curious what “bad salesmanship” of homotopy theory David has in mind. I’ve certainly heard that charge leveled against category theory (with some justification, as far as I can tell), but never before against homotopy theory.

Posted by: Mike Shulman on May 15, 2012 6:31 PM | Permalink | Reply to this

Post a New Comment