Homotopy type theory as internal languages of diagrams of $\infty$-logoses

We show that certain diagrams of $\infty$-logoses are reconstructed in internal languages of their oplax limits via lex, accessible modalities, which enables us to use plain homotopy type theory to reason about not only a single $\infty$-logos but also a diagram of $\infty$-logoses. This also provides a higher dimensional version of Sterling's synthetic Tait computability -- a type theory for higher dimensional logical relations. To prove the main result, we establish a precise correspondence between the lex, accessible localizations of an $\infty$-logos and the lex, accessible modalities in the internal language of the $\infty$-logos. To do this, we also partly develop the Kripke-Joyal semantics of homotopy type theory in $\infty$-logoses.