Homotopy type theory as a language for diagrams of $\infty$-logoses
This work addresses a theoretical challenge in higher-dimensional category theory and type theory, offering a new tool for researchers in these fields, though it appears incremental as it builds on existing frameworks like Sterling's synthetic Tait computability.
The paper tackles the problem of reasoning about diagrams of ∞-logoses by reconstructing them in homotopy type theory with lex, accessible modalities, enabling the use of plain homotopy type theory for such diagrams and providing a higher-dimensional version of synthetic Tait computability.
We show that certain diagrams of $\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 $\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.