A first-order logic is interpreted in a model where sentences of the logic can be said to be true or false. There may be more than one model, and we can identify morphisms between models.
Do we have a universal model, that is one in which all other models are quotients of this one?
If not, are there nice conditions under which there is?
For example, for geometric theories, we have the classifying topos:
So the classifying topos for the geometric theory $T$ is a Grothendieck topos $S[T]$ equipped with a “universal model $U$ of $T$”. This means that for any Grothendieck topos $E$ together with a model $X$ of $T$ in $E$, there exists a unique (up to isomorphism) geometric morphism $f:E \rightarrow S[T]$ such that $f^*$ maps the $T$-model $U$ to the model $X$.