## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

1. I added the reference

2. Rasekh speaks of a future goal

Blakers-Massey: One of the classical results of algebraic topology is the Blakers-Massey theorem. We already know it holds in a higher topos [Re05]. Thus the next natural question is to show it also holds in an EHT, using the fact that the proof mainly relies on the descent condition

But we know this about the Blakers-Massey theorem already, no? It says thre about the HoTT proof that

This translates to an internal language proof of Blakers-Massey valid in all (∞,1)-toposes (including elementary (∞,1)-toposes). Unwinding of the fully formal HoTT proof to ordinary mathematical language is, for the special case of the Freudenthal suspension theorem, in (Rezk 14).

3. We may as well carry on discussion of this topic here, rather than the parallel thread, since the nLab software sends updates to elementary (infinity,1)-topos here.

With the definition settling down :), perhaps this is a good moment to revisit Joyal-Kripke semantics for HoTT. It was raised back here as something needing some loving attention with regard to n-types cover.

• CommentRowNumber4.
• CommentAuthorMike Shulman
• CommentTime5 days ago

I’m still trying to finish up the semester, haven’t had a chance to really read Rasekh’s paper yet. Re #2, I guess the point is that Rezk’s manual unwinding should apply essentially verbatim in the elementary case, presuming that it only uses descent rather than any Grothendiecky stuff? (Otherwise, the claim would depend on the conjecture that HoTT is an internal language for (elementary) $(\infty,1)$-toposes.)

• CommentRowNumber5.
• CommentAuthornimarasekh
• CommentTime4 days ago
I might be able to explain where the Blakers-Massey came from. There is a good chance that I am over-complicating things and everything has already been done, but here is my perspective: There is already a proof in HoTT. That proof was translated to spaces by Charles Rezk. He also proves that it holds for a higher topos (using model categories). Ideally this means that the proof will also hold for an elementary higher topos, however, I don't know if that directly follows. In particular the arguments by Rezk are focused on spaces. As Mike pointed out the underlying idea should be that everything just depends on descent and other topos theoretic properties, but I personally think this is worth analyzing.

There is also a second motivation I had in mind, which might be less clear from the HoTT perspective. I am hoping to convince more "traditional" algebraic topologists to consider topos theory/higher cats/HoTT. That is also why I called the section algebraic topology. It's interesting how results that are obvious to the HoTT community are surprising to many algebraic topologists. From that perspective having concrete proofs in the language of higher categories seems to be a benefit.
4. Thanks for joining in the conversation, Nima. Of course, do feel free to add to the entry elementary (infinity,1)-topos.

results that are obvious to the HoTT community are surprising to many algebraic topologists.

I’d be interested to hear of anything specific that can be said along these lines. Will HoTT insights be expressible as understandable maxims, or will they remain difficult to comprehend.

• CommentRowNumber7.
• CommentAuthorMike Shulman
• CommentTime4 days ago

There are two proofs by Rezk cited at Blakers-Massey theorem. The first, in Toposes and homotopy toposes, does indeed use model categories. But the second is the one that’s a translation of the HoTT proof and thus uses only elementary topos-theoretic properties, no model categories in sight. The latter writeup does talk about “spaces”, but he says at the beginning

I expect that things go through in an arbitrary ∞-topos.

I think one can just read his note essentially verbatim with “space” translated to “object”. I suppose maybe it would have been better if he’d written it in that language to start with and not trusted the reader to do the translation in their head?

• CommentRowNumber8.
• CommentAuthornimarasekh
• CommentTime2 days ago

OK, I am new to the forum and so my comments are more ambiguous than I expected. I will try to clarify.

I’d be interested to hear of anything specific that can be said along these lines. Will HoTT insights be expressible as understandable maxims, or will they remain difficult to comprehend.

When I was talking about the surprise among algebraic topologists I had the following in mind. There are many results that are well-known for spaces, such as truncations, factorizations, Blakers-Massey, … . Many of those results can be generalized, but very often the proof has to be changed. That’s exactly what resulted in the new proof of Blakers-Massey or truncations. In algebraic topology a standard way to construct truncations is the small object argument. That obviously doesn’t work in every setting, which is exactly why a new proof was necessary. As a result of this general fact algebraic topologists can react surprised that certain results about spaces can hold in other settings and I would like to change that.

There are two proofs by Rezk cited at Blakers-Massey theorem. The first, in Toposes and homotopy toposes, does indeed use model categories. But the second is the one that’s a translation of the HoTT proof and thus uses only elementary topos-theoretic properties, no model categories in sight. The latter writeup does talk about “spaces”, but he says at the beginning.

Yes, I had exactly those two proofs in mind in my previous post. I think you are right and the proof can be adjusted to a topos. The one thing that worries me are fiber-wise statements (like Lemma 1.4). By my understanding of the word fiber this only holds for spaces.

• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTime1 day ago

Ah, I didn’t realize Rezk was lazy in his translation that way. Statements like that, of course, should be interpreted in the HoTT sense of “fiberwise”, as a dependent product internal to the topos. You’re right that there would be some additional work to be done in writing that in true $\infty$-categorical language. On the other hand, maybe that work was already done by ABFJ? Their generalized Blakers-Massey theorem is explicitly “valid in an arbitrary higher topos” (as well as “with respect to an arbitrary modality”) and it looks like their proof is written in $\infty$-categorical language.

• CommentRowNumber10.
• CommentAuthornimarasekh
• CommentTime17 hours ago

I think ABFJ might be a more promising path forward. At least one issue is that some of their results on modalities rely on presentability conditions (for example Proposition 3.1.8 and Proposition 3.3.8). In particular it seems to be needed for the parts where you have to show that we get a factorization system. So, those parts need to be adjusted somehow.

• CommentRowNumber11.
• CommentAuthorMike Shulman
• CommentTime17 hours ago

Right, you do need to be in something like a locally presentable setting in order to generate modalities by an arbitrary set of maps. But the classical Blakers-Massey is, I believe, the special case of their theorem applied to the truncation modalities, and those should exist in the elementary case. Indeed, the fact that truncations can be constructed from finite colimits and an NNO is a big part of what motivated me to suggest that we were ready for a tentative definition of elementary $(\infty,1)$-topos. However, as far as I know, that proof hasn’t been written out in categorical language yet.

But that problem is already mentioned as (III) in your “Algebraic topology” section, so if that’s the only obstacle to applying ABFJ in the elementary case then it doesn’t seem like your problem (II) is really open any more. (Also, I think even in (III) you should say explicitly that the theorem has already been proven in HoTT, and all that remains to do is translate it into categorical language.)