Recall that with the internal language of 1-toposes, we have the nice, basic, and useful result that geometric sequents are stable under base change along geometric morphisms: If $\varphi$ and $\psi$ are geometric formulas (formulas not containing $\forall$ and $\Rightarrow$), and if $\mathcal{E} \models \forall x:X. (\varphi(x) \Rightarrow \psi(x))$, then also $\mathcal{F} \models \forall x:f^*X. (f^*\varphi(x) \Rightarrow f^*\psi(x))$, where $f : \mathcal{F} \to \mathcal{E}$ is a geometric morphism.

This is useful for lots of things, for instance for comparing validity on a space with validity at all points and for using classical reasoning in proving geometric sequents.

I have two naive questions relating the $(\infty,1)$-categorical generalization of this.

**Question 1.** Is there a similar preservation statement for the internal language of $(\infty,1)$-toposes, at least in those cases where it's known that homotopy type theory serves as the internal language? (Note that, in light of propositions as types, one should probably formulate the preservation statement in slightly different terms.)

**Question 2.** If yes, is it useful? Or are, with the prevalent use Pi types and universes (which are probably not preserved by the inverse image parts of arbitrary geometric morphisms), few formulas of the required form?