This is a vague question, and I apologize in advance for it. I do not need a definite answer, I am happy to just get some general ideas.
An elementary topos can model higher order logic over a dependent type theory (the first type theory in the last chapter of Bart Jacob's book), and that is already sufficient for a lot of mathematics. I have also seen that the stack semantic (paper by Mike Shulman) adds clauses to the Kripke-Joyal Semantic of a topos, which allow to interpret unbounded quantification over types (∀X:Type, ∃X:Type).
I have recently witnessed someone (Ingo Blechschmidt) start an informal argument in the internal language of a sheaf topos (the Zariski topos) like this: Internal to the Zariski topos we can form the category of finitely presented $\mathbb A$-algebras, and the category of internal presheaves on them. I have been told that the right way to make the internal language expressive enough to allow such talk is to extend the internal language, so that it can talk about locally internal categories in $Zar$ (certain Grothendieck fibrations above $Zar$), or even about all fibrations above $Zar$. The type theory which Ingo sketched looked a lot like the logic of a 2-category which you can find in Mike Shulman's part of the nLab.
Here is my confusion: If someone told me that they would like to form for example the category of groups internal to the Zariski topos
Group = ΣG:Type, Σm:G×G→G, Σe:1→G, ...
then I would have guessed that they need to add universes to their semantic, and I would have suspected that they need some set-theoretic Grothendieck-universes from the outside to make that happen (I don't know much about universes in type theory). The extension of the model from the Zariski topos (sheaves on $Ring_{fp}^{op}$) to Zariski-stacks (2-sheaves on $Ring_{fp}^{op}$), that is from a 1- to a 2-categorical world, seemingly goes in an orthogonal direction. (Altough it is also a size increase, since the 2-category $Cat_\kappa$ in which the 2-sheaves take values must be larger than the 1-category $Set_\kappa$, here $\kappa$ is a fixed cardinal). On the other hand, the extension to stacks makes sense, since intuitively the stack $R\mapsto \mathrm{Mod}_R$ should be the interpretation of Vect and the self indexing should be the interpetation of Type.
Questions: Can I also construct the Zariski topos internal to the Zariski topos by adding support for universes to my semantic? Would the resulting theory and its external semantic be essentially different? What is its relation to the (let me call it) language of fibrations over $Zar$?
(I am asking on this side, since I have been told that proofassistant.stackexchange was supposed to be also about categorical logic and the semantic of type theories.)
