作为 ∞-logos 图表语言的同伦类型论
范畴论
2026-03-18 v6 计算机科学中的逻辑
逻辑
摘要
我们表明，某些 ∞-logos 的图表可在扩展了若干 lex、可访问模态的同伦类型论中重建，这使我们能够使用plain同伦类型论不仅对单个 ∞-logos 进行推理，也对 ∞-logos 的图表进行推理。这也提供了 Sterling 的综合 Tait 可计算性——一种用于高维逻辑关系的类型论——的高维版本。
引用
@article{arxiv.2212.02444,
title = {Homotopy type theory as a language for diagrams of $\infty$-logoses},
author = {Taichi Uemura},
journal= {arXiv preprint arXiv:2212.02444},
year = {2026}
}