# Is ${\bf Set}$ the terminal autological topos

An autological topos is a type of topos defined by Mike Shulman in his paper on stack semantics; specifically, they are toposes satisfying an additional topos theoretic axiom schema expressed in their internal stack semantics which gives their internal logics the full strength of $$ZF$$ set theory. In his own words:

On the other hand, the stack-semantics version of [the] separation [axiom] seems to be a new topos-theoretic property. We call a topos with this property autological. Autology is also closely connected to the stack semantics: a topos is autological if and only if its stack semantics is representable, in the same sense that the usual Kripke-Joyal semantics is always representable. (This motivates the name: a topos is autological if the logic of its stack semantics can be completely “internalized” by representing subobjects.) Autology is also quite common and well-behaved; for instance, we will show in §9 that all complete topoi are autological, and in in [Shub] we will study its preservation by other topos-theoretic constructions (including realizability).

Since Grothendieck toposes are complete, all Grothendieck toposes are autological.* Let $$\mathfrak{Groth}$$ denote the category of Grothendieck toposes and geometric morphisms, and $$\mathfrak{aut}$$ the category of autological toposes and geometric morphisms.

$${\bf Set}$$ is terminal in $$\mathfrak{Groth}$$ which is a subcategory of $$\mathfrak{aut}$$ by the above, but is $${\bf Set}$$ terminal in $$\mathfrak{aut}$$?

This would seem like a more satisfying characterization since autological categories are precisely the categories with the internal logical strength of $$ZF$$, so the category of sets in $$ZF$$ should be universal in some sense among these categories.

EDIT: As Qiaochu Yuan suggests in the comments, we may want morphisms other than geometric morphisms in $$\mathfrak{aut}$$ in order to correctly characterize $${\bf Set}$$ as universally modeling $$ZF$$ internally.

As a bonus question:

How does this relate to the fact that $${\bf Set}$$ is the initial $$ZF$$-algebra? Is it some sort of dual statement?

*This is proven in IZF set theory in Mike's paper.

**This question occurred to me while trying to answer this question.

• How does one see that $\mathbf{Set}$ is terminal in $\mathfrak{Groth}$? – Jordan Mitchell Barrett Dec 16 '20 at 8:43
• @JordanMitchellBarrett Here is a link to a MSE question with some hints: math.stackexchange.com/questions/3052046/…. If you have more questions, I think this would make a great question on MSE. – Alec Rhea Dec 16 '20 at 8:47
• oh, that's nice. I'm a topos theory noob so I'll read up on that result. – Jordan Mitchell Barrett Dec 16 '20 at 8:54
• For the purposes of trying to characterize $\text{Set}$ as a model of ZF I don't think it's at all clear that geometric morphisms are the appropriate notion of morphism (as opposed to e.g. logical morphisms or something else entirely). – Qiaochu Yuan Dec 16 '20 at 8:58
• @JordanMitchellBarrett: But just so you know, the statement that $\textbf{Set}$ is the terminal Grothendieck topos is not some deep insight about the category of sets, because the notion of a Grothendieck topos refers to $\textbf{Set}$. In fact, there is a relativization: For any (elementary) topos $\mathcal{E}$, $\mathcal{E}$ is terminal in the category of "Grothendieck toposes over $\mathcal{E}$" (more formally known as "elementary toposes which are bounded over $\mathcal{E}$). – Ingo Blechschmidt Dec 16 '20 at 13:39

The answer to the original question is no. Indeed, there are autological toposes that do not admit any geometric morphism to $$\rm Set$$, such as realizability toposes and filterquotients. (As pointed out by მამუკა ჯიბლაძე in the comments, this is also true of the topos of finite sets and that of sets below some inaccessible cardinal, which are also autological, but unlike the former realizability toposes and filterquotients contain NNOs, and unlike the latter they require no hypotheses beyond ZFC.)
Switching to logical functors doesn't help matters. There are already Grothendieck toposes that don't admit any logical functor from $$\rm Set$$ (indeed, any topos admitting a logical functor from $$\rm Set$$ must be Boolean, since a logical functor preserves the isomorphism $$1+1\cong\Omega$$), while I believe the trivial topos is terminal among any kind of topos with logical functors.
In general, I don't think one can expect to uniquely characterize $$\rm Set$$ using any elementary property such as autology (even combined with initiality or terminality). I don't know a watertight argument against this myself, but maybe some set theorist can come up with one. Note that the initial ZF-algebra, like the terminal Grothendieck topos, has a non-elementary property of set-indexed completeness.