Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 18 of 18
I am working on the following post for the Café. This still needs plenty of polishing. But I will take a little break and thought I might already give a preview here.
[edit: now posted here]
Due to the size restrictions on comments here, I am posting this in several parts
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 everbody 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 had 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.
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 is it 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 interprets 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 “-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.
The situation studied in that article concerns a hypothetical physical system in which on spacetime 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 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.)
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?
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 “”, 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 of configurations of the gauge field. And a set, to be denoted, , of configurations of (part of) the -field. So we’d write
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):
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
This is just some equation in the set (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
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 are not just three fields on . But four!
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, 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
becomes the statement that is a term of type . 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
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 ), 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
over the product type
of (and that’s the key) the dependent identity type .
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 automagically comes out as the homotopy pullback of along , the homotopy-universal way of completing the following diagram:
of smooth -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 at homotopy pullback.)
In our example, the claim is that this homotopy type is the correct “type of -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, takes automatically care of otherwise subtle phenomena.
Looking good! But doing some proof reading for boring typos.
Re #1
“I think is fair to say” I think IT’s fair to say
“rich of subtle mathematical effects” rich IN subtle
“The E8-modlu 3-stack” moduli
Re #2
“concerns a hypthetical physical system” hypOthetical
“Since all of the are gauge fields” theM
“to elements of these sets” ’to’ sounds odd.
Hi David,
excellent! While I am still revising, already the first bug reports come in. That’s efficient! :-)
Thanks for catching those typos, am correcting them now.
I will mainly still work on the very last paragraphs. Currently I think the punchline is not yet communicated properly yet. When I arrived at that point after all the introduction, I was running out of steam…
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, I’d say. For instance that the geometric procedure of giving a contracting homotopy of an -stack is equivalent to the homtopy-logical procedure of proving (see at contractible type for details) might be taken as an example.
Or consider the notion of free loop space objects (“derived loop spaces”) of an -stack . Often these are heuristically motivated as formalizing the idea that a point in them is given by “making two points in equal in two different ways” (such as to yield a loop). In terms of homotopy type theory, this heuristics becomes a theorem:
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.
On p. 5 of that article, there’s something wrong with the expression of the mapping . At the very least a stray bracket, and I think an extra hat and ’conn’s.
Woops, you are right. I’ll fix this now in my local copy. Hm, that’s an annoying typo. Thanks for catching it!
I look forward to hearing responses to the question in your conclusion. You’d think all the DAG-people would have examples.
True, for instance the derived loop space is in the literature often motivated as formalizing the idea of “making two points equal in two ways” (giving a loop). If you adopt homotopy type theory, then this heuristics becomes a theorem, expressing the derived loop space of some as
Maybe I should add that to the above.
Quite beautiful! It makes me very happy to see this nice application.
One thing which might be nice to add: is there anything more you can say, at this level of precision, about in what sense the homotopical object is the “correct” space of solutions?
A minor nitpick. In the sentence
In the correct answer the collection of field satisfying the quantization constraint contains not three elements. But four!
you probably don’t want to say that “, not !”. I know what you are trying to say, but I’m a but stuck how to express it nicely. What about
In the correct answer, the number of fields involved in the constrained collection of fields is not three, but four!
But I feel it could be done better.
Thanks, David. You are absolutely right. I have changed it simply to “not three fields on . But Four.”
Maybe I should expand on that in a footnote…
Since David Corfield addressed the same point on the Café, I wrote a bit more in reply to it here.
Since, somewhat inadvertedly, 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?
A minor nitpick
The word ”inadvertedly” (resembling ”inadvertently”) perhaps legally does not exist (oxforddictionaries.com).
But, ok: ”Die Bedeutung eines Wortes ist sein Gebrauch in der Sprache.” (the meaning of a word is its use in the language) :-)
Ah, right. Thanks, you got me there. I’ve fixed it.
1 to 18 of 18