Base change in homotopy type theory

Question

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?

Answer 1

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.)

As for question 2, it's true that in HoTT we usually make use of higher-order operations. This is not so different from doing mathematics in a 1-topos, although working with non-0-truncated types does mean that some things that used to be formulable using "mere relations" no longer are. So geometric logic, and its preservation by geometric morphisms, is perhaps a bit less useful than in 1-topos theory. On the other hand, one can also consider a larger sort of "geometric type theory" involving un-truncated operations such as pushouts that are nevertheless still preserved by inverse image functors.

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".