arXivDaily arXiv每日学术速递 周一至周五更新
arXiv周末暂无论文更新,休息一下吧,周末愉快~~
arXiv 2212.02444math.CTcs.LOmath.LO
收藏

同伦类型论作为图示的∞-逻辑格的语言

Homotopy type theory as a language for diagrams of $\infty$-logoses

Stockholms universitet(斯德哥尔摩大学)

Taichi Uemura

AI总结:

论文展示通过扩展同伦类型论加入某些lex可及模态量,可将∞-逻辑格的图示重构,从而用普通同伦类型论处理单个或多个∞-逻辑格。

摘要:

我们展示某些∞-逻辑格的图示可在扩展了某些lex、可及模态量的同伦类型论中被重构,这使我们能够使用普通的同伦类型论来推理单个∞-逻辑格或∞-逻辑格的图示。这还提供了一个更高维度的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.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑