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 have given the definition of (infinity,1)-pretopos an entry, from appendix A of Jacob Lurie’s “Spectral Algebraic Geometry”.
Since this is defined via a variant of the Giraud-Rezk-Lurie axioms with some of the infinitary structure made finitary, and since there is a large supply of non-Grothendieck examples (the sub--categories of coherent objects in any Grothendieck -topos are -pretoposes), it would be interesting if -pretoposes were examples of elementary (infinity,1)-toposes, for some definition of the latter.
Are they?
No; the difference is analogous to that between a 1-pretopos and an elementary 1-topos.
An elementary topos is a pretopos with power objects, is that right?
What kind of universes does an -pretopos have, if any?
An elementary topos is a pretopos with power objects, is that right?
Recognizing that you ask whether that is right, not whether it appears on the nLab, let me remark here that in Section 1 of pretopos one currently reads more or less precisely that:
“A topos is a pretopos that has power objects.”
Yes, an elementary topos is a pretopos with power objects, or equivalently a locally cartesian closed pretopos with a subobject classifier. A pretopos doesn’t necessarily have any universes.
Okay, thanks.
Is there a direct way to conclude from the Giraud-Rezk-Lurie axioms the existence of universes, and hence to see what fails for -pretoposes?
And could you remind me what candidate examples of non-Grothendieck elementary -toposes you know of, or expect? Or in fact remind of of anything there is to say regarding examples at the moment?
(The Lab entry on elementary -toposes would also deserve to have a comment on this issue added.)
Can we please avoid saying “-pretopos” for “-pretopos”? This usage is even more execrable than -topos for -topos, since “-pretopos” is already in common use in 1-topos theory to mean an infinitary 1-pretopos (i.e. a 1-pretopos that is infinitary-extensive).
Universes for Grothendieck -toposes usually come from adjoint-functor-theorem local-presentability-type arguments, while an -pretopos is not locally presentable.
There’s not much known about examples of elementary -toposes at the moment. The MRC group made some good progress towards a gluing construction, which would presumably produce non-Grothendieck examples if the gluing functor is inaccessible, though I don’t know whether we know of any inaccessible lex functors between -topoi. (In the 1-categorical case, their existence requires large cardinal hypotheses.) I would expect filterquotients to exist without too much trouble, and realizability toposes to exist with a good deal of trouble (a number of HoTT people are already working on the latter, from various different perspectives). I’m not sure whether to expect other non-Grothendieck 1-toposes to categorify, such as uniformly continuous actions by a topological group, or small-set-valued presheaves on a large groupoid.
Thanks, Mike.
I added a very brief comment on the Lab page here saying that presently no non-Grothendieck examples are known.
There should be an -functor from homotopy type theories to -categories as in arXiv:1610.00037 and elementary -toposes should be defined to be the essential image of that. But I suppose again nobody knows how to make this work with universes?
[…]
There should be an -functor from homotopy type theories to -categories as in arXiv:1610.00037 and elementary -toposes should be defined to be the essential image of that.
I don’t think that’s a good way to say it. Firstly, elementary -toposes are only going to correspond to one particular kind of homotopy type theory (in my proposal, they should correspond to HoTT with univalent universes, propositional resizing, and non-recursive HITs); other kinds of homotopy type theory correspond to other kinds of higher categories. Secondly, even in the particular case of this correspondence it is not clear how exact it should be, e.g. type theory generally comes with a specified tower of countably many universes, whereas categorically I think it is more natural to assume only the mere existence of as many universes as needed. Finally, I think defining the category theory as the “essential image” of the type theory is backwards: we should instead choose the type theory so as to correspond to the categories we are interested in, although experience with type theory can inform our choice of definitions for category theory. In particular, if the coherence problem relating type theory to -category theory turns out to be unresolvable, then it is type theory that will have to change, not -category theory.
Sure, just some type theories. I keep forgetting what exactly the agreement is what “Homotopy Type Theory” refers to. In any case, the definition via such a functor would have the advantage that it would construct actual examples from syntax.
How about the would-be example of -finite homotopy types, if we disregard the existence of homotopy colimits altogether? Does the -category of -finite homotopy types still have a universe?
For me, “homotopy type theory” is not the name of a specific type theory but of the whole subject.
I would doubt that -finite homotopy types have a universe, but I don’t know.
Okay, thanks.
When you try to motivate elementary -toposes to people who are not motivated by type theory as such, what is your perspective?
I don’t know that I’ve ever tried to do that. It would probably depend on who they were. Are they category theorists or homotopy theorists?
They are into -topos theory. They read “Spectral algebraic geometry”, see the remarks on first order logic there [1] and are wondering if the concept of elementary -toposes has something to offer. They look at the -finite homotopy types in the Ambidexterity article, and are wondering if their -topos theory, stripped down a bit, would allow them to handle this better. Generally, they have the vague feeling that given their expertise in -topos theory, that they would benefit from understanding elementary -toposes, and maybe conversely that the theory of elementary -toposes would benefit from them, but they don’t get a foot on the ground and don’t really know what’s going on.
[1]: “On the other hand, the theory of bounded infinity-pretopoi has the virtue that it admits a completely finitary description (in other words, it can be axiomatized without referring to infinite limits and colimits), and seems to provide a good language for extending concepts of first-order logic to the infinity-categorical setting. We offer some evidence for this last assertion in §A.9 by proving an infinity-categorical generalization of the “conceptual completeness” theorem of Makkai-Reyes (see [143]).”
That doesn’t sound as if they need any motivation.
If none of this actually gives rise to examples of elementary -toposes, then the conclusion drawn will be that there is no apparent motivation for the axioms, and that something like -pretoposes is the way to go for them.
If you had posed the parallel issue for ordinary elementary toposes after they were first proposed, what would have been likely suggestions for the benefits of the concept? Was the focus largely logical? I remember hearing of the effective topos as a first non-Grothendieck example.
From MO, we know there’s interest in developing the categorical logic for -pretoposes. Motivation for wanting an elementary -topos is thin here. [7 upvotes for Mike’s definition there.]
It seems likely to me that -pretoposes is the way to go for them. I think elementary toposes are generally of more interest to people coming from a logical/foundational perspective. Most non-Grothendieck elementary toposes are rather exotic; realizability toposes are perhaps an exception (although in some sense even there I regard it as an “accident” that they are toposes rather than just pretoposes — some closely related things are only pretoposes), but they are probably not of much interest to folks coming from geometry and homotopy theory. I think the main interest in elementary toposes as such is that they have an “elementary” (first-order, finitary) definition (which is a bit questionable in the -case anyway) and we can “do mathematics relative to any one of them” (which has about the same content as saying we can interpret type theory inside one).
Moreover, in the -case, I think the particular choice of axioms for an elementary -topos, even if my proposal turns out to be the “right” one (insofar as that has meaning), is likely to be much less “central” in the world of elementary higher topos theory — by which I mean “elementary (higher topos theory)”. For one thing, inductive constructions like HITs seem more important homotopically than 1-categorically, and in general those are not available in my definition. For another thing, the impredicative subobject classifier is both less useful and less necessary homotopically; some reasons were discussed here.
I would hope that we would not separate the type theorists and -topos theorists here, because the beauty of the subject is that this distinction ought to be artificial.
What I would like to better understand now is:
1) What are interesting examples of locally Cartesian closed -categories with object classifiers (besides Grothendieck -toposes)?
2) Which classes of -colimits do these examples happen to have?
Or in other words, I’d like to know which axioms (except for the basic //-type formers and type universes) need to be taken away from those of elementary -toposes such that we hit known examples besides Grothendieck -toposes.
Of course there is a unity to the subject, but even within a unified subject there is plenty of variety in what individual mathematicians are interested in, their background and motivations. I don’t think this is an “artificial” distinction; on the contrary, the beauty of having a unified subject is that there are many different entry points, which emphasize different parts of the subject, and nevertheless they are all interconnected.
By the way, in case it wasn’t clear, by “much less central” I meant “less central than it is in 1-topos theory”, not “less central than it is in type theory”.
Offhand I don’t think I know any examples of -categories with object classifiers that aren’t Grothendieck -toposes (or derived from them in some trivial way).
Thanks, Mike. It’s good to know what you say the state of this question is. Maybe that’s a good question for MathOverflow.
1 to 23 of 23