Removed the adjective “some” in front of “finite $(\infty,1)$-limits”, since a terminal object and pullbacks suffice to construct all finite $(\infty,1)$-limits.

]]>Thanks, Mike. It’s good to know what you say the state of this question is. Maybe that’s a good question for MathOverflow.

]]>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 $(\infty,1)$-categories with object classifiers that aren’t Grothendieck $(\infty,1)$-toposes (or derived from them in some trivial way).

]]>I would hope that we would not separate the type theorists and $(\infty,1)$-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 $\infty$-categories with object classifiers (besides Grothendieck $\infty$-toposes)?

2) Which classes of $\infty$-colimits do these examples happen to have?

Or in other words, I’d like to know which axioms (except for the basic $\prod$/$\sum$/$id$-type formers and type universes) need to be taken away from those of elementary $\infty$-toposes such that we hit known examples besides Grothendieck $\infty$-toposes.

]]>It seems likely to me that $(\infty,1)$-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 $\infty$-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 $\infty$-case, I think the particular choice of axioms for an elementary $(\infty,1)$-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.

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 $(\infty, 1)$-pretoposes. Motivation for wanting an elementary $(\infty, 1)$-topos is thin here. [7 upvotes for Mike’s definition there.]

]]>If none of this actually gives rise to examples of elementary $(\infty,1)$-toposes, then the conclusion drawn will be that there is no apparent motivation for the axioms, and that something like $(\infty,1)$-pretoposes is the way to go for them.

]]>That doesn’t sound as if they need any motivation.

]]>They are into $(\infty,1)$-topos theory. They read “Spectral algebraic geometry”, see the remarks on first order logic there [1] and are wondering if the concept of elementary $(\infty,1)$-toposes has something to offer. They look at the $\pi$-finite homotopy types in the Ambidexterity article, and are wondering if their $(\infty,1)$-topos theory, stripped down a bit, would allow them to handle this better. Generally, they have the vague feeling that given their expertise in $(\infty,1)$-topos theory, that they would benefit from understanding elementary $(\infty,1)$-toposes, and maybe conversely that the theory of elementary $(\infty,1)$-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]).”

]]>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?

]]>Okay, thanks.

When you try to motivate elementary $(\infty,1)$-toposes to people who are not motivated by type theory as such, what is your perspective?

]]>For me, “homotopy type theory” is not the name of a specific type theory but of the whole subject.

I would doubt that $\pi$-finite homotopy types have a universe, but I don’t know.

]]>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 $\pi$-finite homotopy types, if we disregard the existence of homotopy colimits altogether? Does the $\infty$-category of $\pi$-finite homotopy types still have a universe?

]]>There should be an $\infty$-functor from homotopy type theories to $\infty$-categories as in arXiv:1610.00037 and elementary $\infty$-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 $\infty$-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 $(\infty,1)$-category theory turns out to be unresolvable, then it is type theory that will have to change, not $(\infty,1)$-category theory.

]]>[…]

]]>Thanks, Mike.

I added a very brief comment on the $n$Lab page here saying that presently no non-Grothendieck examples are known.

There should be an $\infty$-functor from homotopy type theories to $\infty$-categories as in arXiv:1610.00037 and elementary $\infty$-toposes should be defined to be the essential image of that. But I suppose again nobody knows how to make this work with universes?

]]>Can we please avoid saying “$\infty$-pretopos” for “$(\infty,1)$-pretopos”? This usage is even more execrable than $\infty$-topos for $(\infty,1)$-topos, since “$\infty$-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 $(\infty,1)$-toposes usually come from adjoint-functor-theorem local-presentability-type arguments, while an $(\infty,1)$-pretopos is not locally presentable.

There’s not much known about examples of elementary $(\infty,1)$-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 $(\infty,1)$-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.

]]>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 $\infty$-pretoposes?

And could you remind me what candidate examples of non-Grothendieck elementary $\infty$-toposes you know of, or expect? Or in fact remind of of anything there is to say regarding examples at the moment?

(The $n$Lab entry on elementary $\infty$-toposes would also deserve to have a comment on this issue added.)

]]>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.

]]>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.”

]]>An elementary topos is a pretopos with power objects, is that right?

What kind of universes does an $\infty$-pretopos have, if any?

]]>No; the difference is analogous to that between a 1-pretopos and an elementary 1-topos.

]]>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-$\infty$-categories of coherent objects in any Grothendieck $\infty$-topos are $\infty$-pretoposes), it would be interesting if $\infty$-pretoposes were examples of elementary (infinity,1)-toposes, for some definition of the latter.

Are they?

]]>