Homotopy type theory as a language for diagrams of $\infty$-logoses
Abstract
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.
Fields of Study & Subjects
Computability
Logic
AI Algorithms
programming
and type systems
Reasoning
and Knowledge
Publication details
- Journal / source
- Logical Methods in Computer Science
- Publisher
- Centre pour la Communication Scientifique Directe (CCSD)
- Volume
- Volume 22, Issue 1
- Publication date
- 12 March 2026
- Language
- EN