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.
I added the reference
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).
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.
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.)
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.
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?
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.
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.
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.
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.)
I agree I should mention the HoTT work on NNO and truncations in the problem section. Thank you for reminding me.
On the ABFJ I am still uncertain. It’s seems promising (and it should be true that descent is enough) but I still need to check in detail to make sure presentability hasn’t snuck into any of the later results.
That’s fair, but even before the checking has been done, their work (and Rezk’s) should still be mentioned in any discussion of this possibly-still-open problem.
Do we have a precise (classical) connection between Shulman/Rasekh and the work by Joyal, who uses model structures? Constructively, we would first need to develop a theory of $\infty$-categories, probably following Riehl/Shulman, perhaps along the lines of directed type theory and the work by Licata and Weaver slides.
Which work by Joyal are you referring to?
This one, the one linked to at that elementary+(infinity%2C1)-topos using tribes.
Hmm. Well, I haven’t worked out the details, but I expect that one of his presents one of ours, whereas it’s an open question whether every one of ours could be presented by one of his. Some of his axioms (like fibrancy of $\mathbb{N}$) are very strict, so strict that I don’t even know whether every Grothendieck $(\infty,1)$-topos has a model satisfying them. Other than that issue, it looks like the main difference is that he assumes one fixed universe as part of the structure rather than the mere existence of as many universes as necessary, plus the effectiveness of groupoid objects (which is not “elementary” in the sense of “finite”).
He seems to restrict to Grothendieck toposes over Reedy categories, I don’t know why he wants $N$ to be fibrant.
It would be good to record this in any case, currently, the page read like the two notions are equivalent.
Mike as a follow up to our previous discussion, do you have (or are aware of) a write up of a proof for how to build an NNO in an EHT? I’ve seen you mention this based on the fact that it holds in HoTT, but was wondering if there is an actual higher categorical argument out there.
I don’t think anyone has compiled the HoTT proof out into a topos-theoretic one. It’s kind of involved.
My guess would be that he wants N to be fibrant for the same reason the 2LTT people do, so that he can do things like define a fibrant type of semisimplicial types by induction over it.
Yeah, that is what I was worried about. I think one important step in translating many of the results into an EHT is to have a concrete proof that we can construct an NNO. Well then let me rephrase my question. Do you know of a HoTT proof that would be more amenable to a translation to higher categorical language?
I think constructing an NNO out of the rest of the structure is more of a curiosity than an impediment to using the definition of EHT. Just like the question of whether we can construct colimits: the important thing is that colimits and the NNO are there; if we can remove them from the definition without changing the fact that they’re there, that’s nice, but it doesn’t make much of a difference in practice.
I thought we need an NNO to make the definition of an EHT work. Specifically the constructions by Egbert Rijke need colimits over countably infinite set. So we either have to assume it (which would be a non-finite assumption and so not elementary?) or we have to prove it.
In particular in your blog post you suggest that one reason why we should not assume NNOs in a topos is exactly because we can prove it’s existence and then use that to recover the results of Rijke in the setting of an EHT.
I think in that sense it is different from finite colimits. It am perfectly willing to assuming we have finite colimits (but it would be cool to know you can recover them), but I think it is important that we can build NNO to avoid assuming it.
Based on your post are you suggesting we should just add the existence of an NNO to the definition of an EHT?
An NNO is perfectly finite and elementary. I don’t think it is any different from finite colimits. The only difference between them is that in the 1-categorical case an NNO is not usually included in the definition and doesn’t follow from it — but probably more theorems about elementary 1-toposes than not add the assumption of an NNO, and there aren’t many interesting examples that lack one; so arguably it could just as well have been included.
I think in a paper proving (say) the Blakers-Massey theorem in an EHT it would be perfectly in order to state the definition including an NNO and then say “it is expected that the existence of an NNO can be proven from the other axioms; this has been shown in homotopy type theory, which is conjecturally the internal language of EHTs, but the general internal language theorem has not yet been proven and the construction of an NNO has not yet been manually compiled out into categorical language.”
OT: about toposes without NNO… I guess sheaves of finite sets on a finite site, but are there finite versions of realisability topses? Lurie’s recent course on categorical logic ended up with $\infty$-pretoposes of finite homotopy types, which aren’t $\infty$-toposes, so that’s kind of an indication of the boundary between EHT and higher pretoposes as far as possessing NNO/W-types goes.
1 to 28 of 28