Homotopy type theory as a language for diagrams of $\mathrm{\infty }$-logoses

We show that certain diagrams of $\mathrm{\infty }$-logoses are reconstructed in homotopy type theory extended with some lex, accessible modalities, which enables us to use plain homotopy type theory to reason about not only a single $\mathrm{\infty }$-logos but also a diagram of $\mathrm{\infty }$-logoses. This also provides a higher dimensional version of Sterling’s synthetic Tait computability – a type theory for higher dimensional logical relations.