一句话：用带 lex 可及模态的 HoTT 重建 ∞-logos 图，并给出高维 synthetic Tait computability。
论文研究如何用同伦类型论（HoTT）刻画的不只是单个 ∞-logos，还包括 ∞-logos 构成的图。作者在 HoTT 上加入一族 lex、accessible 模态，并证明某些 ∞-logos 图可在该类型论中重建，从而可用普通 HoTT 推理这些图表及其中的逻辑结构。该工作还给出 Sterling 的 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Uemura26,
title = {Homotopy type theory as a language for diagrams of $\infty$-logoses},
author = {Taichi Uemura},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 1},
year = {2026},
doi = {10.46298/lmcs-22(1:25)2026}
}