# Base change in homotopy type theory

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?

The answer to question 1 is yes. To see this, I think it's better to consider a "geometric sequent" to be of the form $$(x:X), \phi(x) \vdash \psi(x)$$ since this avoids all mention of $\forall$ and $\Rightarrow$. Now we can see that the point is just that the "geometric" logical operations $\exists$, $\wedge$, $\vee$ (and more generally its infinitary version $\bigvee$), $\top$, and $\bot$ all correspond to categorical operations that are preserved by inverse image functors — finite limits and arbitrary colimits — while the meta-logical operation $\vdash$ just means the existence of a morphism, which is certainly preserved by any functor.
The same argument works essentially unaltered in the homotopy/∞ case, if we replace "formulas" by what HoTT calls hprops or "mere propositions", and the logical operations by their $(-1)$-truncated versions, since these are all interpreted by $(\infty,1)$-categorical constructions built out of finite limits and arbitrary colimits. (Although a version of HoTT allowing infinitary operations such as $\bigvee$ is not yet well-studied.)
One particular application of geometric logic for 1-toposes is of course the theory of classifying topoi. The theory of classifying $(\infty,1)$-topoi is not yet as well-developed, but indications are promising. Closely related material has been developed, in different language, by Jacob Lurie under the name of geometry (see also the nlab page). Recently Andre Joyal and some collaborators have been working on showing that the $(\infty,1)$-topos of parametrized spectra is a classifying topos for "stable objects"; the latter notion involves loop-spaces of suspensions, and thus belongs to "geometric type theory" but not the more restrictive (-1)-truncated "geometric logic".