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 15 of 15
In the HoTT book, there's all these great slick proofs of classical results from homotopy theory in Chapter 8, but then there's this tricky stuff about constructive definitions of the real numbers in Chapter 11. And they don't have much to do with each other. But historically, these subjects have been closely related: not only does the definition of the fundamental group involve the unit interval in the real line; knowing the fundamental group of the circle allows us to prove the Brouwer fixed point theorem (and thence the Jordan curve theorem), for example. I could some algebraic topologists might claim that the subject matter of Chapter 8, while interesting, simply is not their subject matter.
Has any work been done on constructing classical homotopy theory (which is about homotopy 0-types equipped with subframes of their power frames) in HoTT and then showing that this is an internal model of HoTT itself, allowing the results of Chapter 8 to be reflected in results about analysis?
Presumably there will be parts of classical homotopy theory which are due to the specificity of the ()-category they’re working in.
Is something relevant here the way Eckmann-Hilton duality fails in Top, because of a lack of arrow-reversing duality in the latter
…a pullback of a cofibration by a fibration is a cofibration, but a pushforward of a fibration by a cofibration is not a fibration.
Presumably there will be parts of classical homotopy theory which are due to the specificity of the ()-category they’re working in.
Certainly strict homotopy will not show up in HoTT. But there is a lot of classical homotopy theory (for example, the result ) that is also true in HoTT's native homotopy theory, but we still don't know (or at least I don't) how to conclude the classical theorem (about functions between the set of real numbers and related sets) from the native one. (For simplicity, let us work in HoTT + EM, to obviate any considerations about the correct constructive notion of continuous map.)
If you’re willing to work in HoTT+AC, then all of classical homotopy theory can be developed internally and shown to be a model of HoTT, in exactly the same way that classical homotopy theory inside ZFC can be shown to be a model of HoTT. No one has written this out explicitly, but if you believe that ETCS(perhaps +R) is as good a foundation for mathematics as ZFC, then you should believe this, because chapter 10 shows that the hsets in HoTT satisfy ETCS. I should point out, though, that even in ZFC, it’s not topological spaces that model HoTT directly, but rather simplicial sets.
On the other hand, the existence of any constructive model of HoTT is a topic of current research. Simplicial sets don’t seem to work without at least LEM; I don’t know whether they work with LEM but without AC. Thierry and Marc have recently claimed that cubical sets do work constructively, at least if you give up judgmental computation for identity types. If this is right, then you could perform their proof inside the hsets of HoTT to construct an internal model of HoTT. (I do think some work would be required to conclude that HoTT still looks mostly familiar even without judgmental Id-computation.)
Relating simplicial or cubical sets to topological spaces constructively is another question. It seems clear that any space will still have a singular simplicial or cubical set. Will it be sufficiently fibrant?
@jim: I have some experience with both (including helping to write the book). What do you want to know? (Although maybe this would be better as a separate thread.)
Thanks, Mike! It's interesting that people even want to use AC, since such elementary results as seem pretty constructive (requiring at most the fan theorem). Still, I can imagine that general results would need more.
If we wished to prove the Brouwer fixed point theorem in HoTT + AC using the homotopy-theoretic argument, would it be shorter to do a proof purely in the ETCS fragment, or to use the slick homotopy-theoretic results from HoTT together with the reflection of this in simplicial h-sets? I'm guessing the former.
I suppose that the bottom line is that there's still a lot of work to do.
I expect it’s probably less that people want to use AC as that algebraic topologists are classical mathematicians and it doesn’t even occur to them to try to avoid it.
There may be another level of confusion going on, by the way: my #5 was about building a model of HoTT inside of HoTT, but another thing you could do is stay with only one model of HoTT and ask how spaces (i.e. hsets with subframes of their power frames) give rise to “fundamental types” in that same model of HoTT. Your second paragraph seems to me to suggest that approach, which we don’t even exactly know how to do yet — the fundamental type should be a HIT of some sort, but there’d have to be some way to package up its a-priori infinitely many constructors.
In any case, however, I think you’re right that there’s going to be some amount of work in connecting topological spheres to homotopical ones. It’s not even obvious to me that, say, the fundamental type of the topological -sphere, for , is (constructively) the HIT -sphere.
stay with only one model of HoTT and ask how spaces (i.e. hsets with subframes of their power frames) give rise to “fundamental types” in that same model of HoTT
This would be ideal. The constructors would be simplices (in the concrete classical-analytic sense: pointwise continuous functions from a power of the h-set of real numbers).
I guess if all you want is to prove the Brouwer fixed point theorem, then you only need the fundamental 1-type, and that won’t be hard to define. But I still don’t see an immediate way to identify the fundamental 1-type of the topological circle with the HIT circle.
It seems to me that such an identification ought to be doable, at the level of homotopy equivalence between types, or something is wrong. They both ought to be equivalent to the one-object groupoid whose automorphism group is .
Yes, certainly; I spoke confusingly. I meant, I don’t yet see a way to identify them without first proving that each of them is equivalent to that. In other words, I don’t see how to use the calculation of of the HIT circle to tell us something that we didn’t already know about the topological one.
A slightly off-topic but related remark and question:
I heard from the recent meeting in Oxford that some of the non-logician big shots attending showed irritation upon being exposed to enthusiastic advertizement of the existence of a computation of of the circle in HoTT.
In Barcelona I experienced what is maybe the converse of this: HoTT theorists jumping at me for calling some classical fact “simple”, emphasising that in HoTT it takes a hundred lines of Coq code and hence is not at all simple.
I know some big names in homotopy theory who look down on the whole HoTT program based on this impression that it’s just simple facts being rederived in a seemingly inappropriate way.
In these conversations, I am trying to argue for HoTT. I am trying to point out that computing the homotopy group of the circle is not meant to be a big deal in itself (even if the concrete code that accomplishes is a genuine accomplishment which these critics wouldn’t be able to reproduce without considerable effort), but rather a proof-of-principle that is meant to open the door to a source of genuinely new insights in homotopy theory.
I noticed that the announcement of the Peter Lumsdaine et al. proof of Blakers-Massey theorem goes in this direction.
But my question is: did anyone try to write an exposition “Why should pure homotopy theorists care about HoTT?” Is there a section in the book dedicated to this, maybe? (I had once started that nLab page HoTT methods for homotopy theorists but it doesn’t quite get to this point yet.)
I think a good explanation of why pure homotopy theorists should get excited about the existence of a constructive proof of would have considerable sociological value. I was pleased to see homotopy theorist Jack Morava attend the HoTT meeting in Bacelona, but he is clearly an exception in his broadness of appreciation of ideas. It would be great fun if the next HoTT conferences had more and more pure homotopy theorists attending. but I think that will take some more convincing. Of course that will eventually happen by itself as the field proceeds. But maybe an advertizement right now might help a lot.
If we wanted to look at a case we already now much more about, why not compare
Could we say that convincing a homotopy theorist of the benefits of HoTT, will be like convincing (3) that (1) is important? Might they not think that to they extent they want any general theory, and this may not be great, they can receive it from (2)?
Similarly, won’t a homotopy theorist look first to Higher Topos Theory and Higher Algebra before The HoTT Book, if they look anywhere at all? I guess one should distinguish between a homotopy theorist who just cares about the homotopy of spaces, and one interested in seeing homotopic constructions applied more generally.
Perhaps the first task is to persuade people that (2) profits from (1), so that any credit due to (2) is shared with (1).
I think the answer to your question, Urs, is “no, not yet”. Personally, I haven’t tried to write such a thing partly because I’m not sure that we have a very good case yet. I feel that it would consist mostly of “the fact that we can do A suggests that maybe someday we’ll be able to do B, and that might be useful to you”. And maybe the people able to appreciate such an argument aren’t the ones we have a problem reaching out to anyway.
1 to 15 of 15