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.
Two new references
Nima Rasekh, Yoneda Lemma for Elementary Higher Toposes, (arXiv:1809.01736)
Nima Rasekh, Every Elementary Higher Topos has a Natural Number Object, (arXiv:1809.01734)
What can be said already of the relation between what can be proved in HoTT and what holds in all elementary (∞,1)-toposes, and of processes to translate between such proofs?
I guess every elementary higher topos should thus admit all W-types? Or at least all finitary ones (those associated to polynomial functors given by formal power series).
What can be said already of the relation between what can be proved in HoTT and what holds in all elementary (∞,1)-toposes, and of processes to translate between such proofs?
At the moment, nothing general and precise. Being able to deduce automatically that HoTT theorems hold in elementary (∞,1)-toposes would require at least (with current technology) knowing how to present any elementary (∞,1)-topos by a suitable kind of fibration category, which is something that we almost know how to do with Grothendieck (∞,1)-toposes (the universes are still too weak in general), but in the elementary case we haven’t much of a clue. There is also the disputed initiality principle. In the other direction, one would need to show that the homotopy (∞,1)-category of the fibration category built out of HoTT syntax is an elementary (∞,1)-topos, which also has not been done; I think the best result we have is Chris Kapulkin’s theorem that it is locally cartesian closed. So at the moment we’re at the stage of only being able to translate proofs “by hand”, which unfortunately isn’t feasible for very long and involved ones like the impredicative construction of an NNO that I formalized in HoTT.
In addition, although I don’t understand Rasekh’s construction of an NNO yet, I do see that he uses non-elementary means, e.g. an infinite limit of categories of diagrams. It’s not immediately clear how to translate such an argument into HoTT manually, although if we believe that the homotopy (∞,1)-category of HoTT is an elementary (∞,1)-topos then there must be a way.
I watched Mike’s very nice talk yesterday – Towards elementary infinity-toposes.
I have a question. So you explain why we can have a subobject classifier straight away, but need to go about things more subtly with object classifiers, since monomorphisms are either equal or not. This shows they can be treated differently, but should they be?
I recall from discussions several years ago, you thinking it better to keep a logical level separate from the type theory. I thought the realisation that the $(-1)$-level is just one level and of no greater significance than any other was to be taken as a sign that ’logic’ is just an integral part of the whole, the result of a truncation. Shouldn’t the definition of elementary infinity-toposes keep to this egalitarian treatment?
I think I should read up on propositional resizing - a page which needs to be created.
If one were to imagine an $\infty$-Elephant, I guess the 6 section structure continues to make sense: as categories; 2-categorical aspects; as spaces; as theories; homotopy and cohomology; as mathematical universes. In fact, maybe some, like the fifth, work out much better.
But that’s the general phenomenon: $\infty$-Category theory has all the structures familiar from plain category theory, plus a bunch of improvements.
From way back in 2007, when I first saw André Joyal speak at the Fields institute here, I (seem to) remember that this is how he introduced the topic of what we now call $\infty$-category theory. He started his talk (paraphrasing from memory) with saying: “In this talk I want to convince you that $\infty$-category theory exists, and behaves much like ordinary category theory.” Of course he said “quasi-categories” instead of “$\infty$-categories”.
Yes, Andre had the same message at 3WFTOP.
I wasn’t presenting this as a surprise that much remains as before, but rather a chance to think on Johnstone’s choice of sixfold account, and how things might be organised from the $\infty$ perspective. I could imagine some shuffling about at the very least.
I see. Regarding the Elephant, I was always thinking that the reason why volume 3 keeps (or kept?) being delayed is that the topic of that volume (cohomology) works really well only once passing from toposes to $\infty$-toposes.
I definitely agree with #40: Part E of the 1-Elephant was outdated before it was written. (-: Although I am still hoping to read Part F one day.
This shows they can be treated differently, but should they be?
They certainly need not be (funny how “need not” and “should not” have such different semantics in English). I wrote about this back here. But it’s a question of terminology: in the 1-category case, an “elementary topos” has an impredicative subobject classifier, so I think it’s best to stick to that usage in the $\infty$ case, with alternative terms like “predicative ($\infty$-)topos” for the predicative case. That way we can say sensible-sounding things like “the category of 0-truncated objects in an elementary $\infty$-topos is an elementary 1-topos”.
Thanks! I don’t even remember that thread. I see it ends
I was already suspicious of the suboject classifier in toposes; type theory is much more elegant without an equivalent of this (Prop, the type of propositions)…Now that these inelegances are out of the way, I am much more interested in topos theory.
Earlier, however, you’d linked elegance with predicativity, and effective computation with its opposite. But perhaps elegance is in the eye of the beholder.
I assume you mean I linked elegance with impredicativity. Yes, elegance is certainly one of the things that’s in the eye of the beholder. However, I do see Itai’s point (he being the one you are quoting about the elegance of type theory). Roughly, the problem is that propositional resizing is an axiom, rather than something expressible as a rule. On the other hand you can formulate a type theory with a specified “type of propositions” $Prop$ that’s impredicative in the sense of admitting quantifications over types in arbitrary universes (for instance, Coq does this), but then you don’t know (unless you assert it as another axiom) that every type with the property of “being a proposition” (i.e. $isprop(A) \equiv \prod_{x,y:A} Id(x,y)$) is equivalent to something in $Prop$. In the traditional perspective on 1-topos theory, this rears its head as the fact that higher-order logic cannot prove the axiom of unique choice, even though it holds in all toposes (because HOL has other models, like strong-subobject logic in quasitoposes, where AUC fails).
Maybe the point is that we’re applying the same adjective to different things: impredicative proofs are more elegant, but predicative formal systems are more elegant.
Yes, impredicativity.
Interesting stuff.
In your talk Mike, you responded to a comment I couldn’t hear by saying something like “that paper has a mistake” and that you were in contact with the author. What paper was that? I notice you didn’t mention Rasekh’s work on NNOs, so I was wondering if it was this.
Yes, it’s that one.
OK, thanks. I was going to ask him if from NNOs one gets all W-types in an elementary $\infty$-topos, but I guess you’re the person to ask now :-)
I haven’t worked it out, but I expect so, in the same way one does in an elementary 1-topos.
Back on #42-43: On the other hand, one might argue that the most elegant formal system is the maximally impredicative one with $Type:Type$…
Concerning #49: What are some good references about Type:Type? I understand that Girards paradox gives us a non-normalising well type term, but can one be a bit clever and avoid these kinds of terms? I have seen for example in the UniMath library that Type:Type is okay as long as one treads carefully. What exactly is meant by this?
Perhaps this post – Universe Polymorphism and Typical Ambiguity – for a start.
I have seen for example in the UniMath library that Type:Type is okay as long as one treads carefully. What exactly is meant by this?
You’d have to ask the UniMath authors. The only thing I can think of that they might have meant by “tread carefully” is “only write down things that could be formalized using a hierarchy of universes instead”, i.e. don’t actually make any use of Type:Type. Universe polymorphism and typical ambiguity, as implemented in modern Coq, are ways that you can sometimes forget about this and just write “Type” whenever you want a universe, and the computer can make sure for you that universe hierarchy levels can be consistently assigned. (In practice, some manual universe level management seems often to be required whenever you’re working seriously with multiple universes, though this could just be a limitation of current tools.)
People do sometimes like to use Type:Type when implementing new type theories, just because it’s simpler and doesn’t get in the way of understanding whatever new features you want to focus on. And if you’re regarding type theory as a programming language for actually writing real-world programs, then non-normalizing terms need not be worrisome, since real-world programming language usually include general recursion (and hence plenty of non-terminating programs) anyway. (And in fact, from Type:Type you can construct a looping combinator and thereby obtain general recursion.) To take an example I happened to be reading recently, this paper writes
…we analyze and implement a partial type checking algorithm for the inconsistent theory Type:Type … The motivation for this work is to implement type checkers for dependently typed programming languages which support general recursion… We use Type:Type as a test case for a language with dependent types avoiding the syntactic complexity of a full programming language.
The problem only comes in when you also want to use type theory to prove things, because a non-normalizing term of type $\emptyset$ would be a proof of a contradiction. (I have some further thoughts about that, but they haven’t coalesced enough to talk about yet.)
1 to 53 of 53