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.

翻译：我们证明，通过lex、可达模态，某些$\infty$-逻辑图可以在其oplax极限的内语言中被重构，这使得我们能够使用纯同伦类型论不仅推理单个$\infty$-逻辑，还能推理$\infty$-逻辑图。这也提供了Sterling综合Tait可计算性的高维版本——一种用于高维逻辑关系的类型论。为证明主要结果，我们建立了$\infty$-逻辑的lex、可达局部化与其内语言中lex、可达模态之间的精确对应。为此，我们还部分发展了$\infty$-逻辑中同伦类型论的Kripke-Joyal语义。