论文标题
同质类型理论作为$ \ infty $ logoses图表的语言
Homotopy type theory as a language for diagrams of $\infty$-logoses
论文作者
论文摘要
我们表明，$ \ infty $ logoses的某些图是以同置类型的理论重建的，该理论以某些LEX，可访问的方式扩展，这使我们能够使用普通同型类型的理论来推理不仅是单个$ \ suftty $ logos，而且还要理解$ \ hyptty $ logoges的图。这也提供了Sterling的合成Tait可计算性的更高维版本 - 一种用于更高维度逻辑关系的类型理论。
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.
