# Definition of "classifying topos"

Is there a geometric theory $$T$$ and a Grothendieck topos $$\mathcal E$$ such that (2) holds but (1) doesn't:

1. $$\mathcal E$$ 2-represents the 2-functor $$\mathbf{GrothTop}\to\mathbf{Cat}$$ which sends a Grothendieck topos $$\mathcal E$$ to the category of models of $$T$$ in $$\mathcal E$$.

2. $$\mathcal E$$ represents the 1-functor $$\mathrm h\mathbf{GrothTop}\to\mathrm h\mathbf{Cat}\to \mathbf{Set}$$ which can be obtained by truncating the above functor to the 1-categorical level and composing with the functor sending a category $$\mathcal C$$ to the set $$\mathrm{Ob}(\mathcal C)/\mathord{\cong}$$ of all objects of $$\mathcal C$$ up to isomorphism.

Conversely, (1) implies (2), right?

A topos $$\mathcal{E}$$ is completely determined by the functor $$\mathbf{Geom}(-,\mathcal{E}) : \mathbf{GrothTop}^\mathrm{op} \to \mathbf{Cat}$$ (this is some kind of 2-Yoneda Lemma). But we can also look at the 1-category $$\mathrm{h}\mathbf{GrothTop}$$ in which we identify geometric morphisms that are isomorphic. Then the (1-categorical) Yoneda Lemma says that $$\mathcal{E}$$ is completely determined by the functor $$\mathbf{Geom}(-,\mathcal{E})/\!\cong\,\, : \mathrm{h}\mathbf{GrothTop}^\mathrm{op} \to \mathbf{Class}$$ to the category of classes (we have to work with classes rather than sets because there can be a proper class of geometric morphisms up to isomorphism between two toposes).
In particular, suppose that $$\mathbf{Geom}(-,\mathcal{E})/\!\cong\,\,$$ agrees with the functor that sends each Grothendieck topos $$\mathcal{F}$$ to the collection of $$T$$-models in $$\mathcal{F}$$ up to isomorphism, for some geometric theory $$T$$. Then $$\mathcal{E}$$ is the classifying topos of $$T$$. To prove this, we need to use the fact that the classifying topos of a geometric theory always exists (thanks to @Mike Shulman for pointing this out).
• However, (2) only implies (1) in this way, for a particular topos $\mathcal{E}$ and theory $T$, once you already know that there exists some other topos that satisfies (1) for $T$, since the argument proceeds by proving that $\mathcal{E}$ is equivalent to that other topos. So, in particular, when constructing classifying toposes in the first place, we still have an obligation to prove the a-priori-stronger statement (1). Commented Dec 24, 2021 at 2:42