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.

Linked paper: arXiv:1004.3802 [math.CT]

9more comments