一句话：在依赖类型论中为弱 ω-范畴操作定义自然性构造，用于生成并验证高维路径项。
本文关注如何在依赖类型论中构造弱 ω-范畴的高维操作项，并解决其自然性与组合结构难以显式生成的问题。作者将自然性构造定义为一种元操作，其几何直觉是与有向区间作局部张量积，逻辑上可视为 Reynolds 参数性的 globular 类比。该构造作为“强力工具”用于定义 ω-范畴中圆柱与圆锥的组合操作，并能生成结构复杂的高维项。作者在证明助手中实现该机制，由类型检查器保证生成项类型正确；结果可导出到同伦类型论，从而显式计算复杂路径类型的居民。
We define a naturality construction for the operations of weak ω-categories, as a meta-operation in a dependent type theory. Our construction has a geometrical motivation as a local tensor product with a directed interval, and behaves logically as a globular analogue of Reynolds parametricity. Our construction operates as a "power tool" to support construction of terms with geometrical structure, and we use it to define composition operations for cylinders and cones in ω-categories. The machinery can generate terms of high complexity, and we have implemented our construction in a proof assistant, which verifies that the generated terms have the correct type. All our results can be exported to homotopy type theory, allowing the explicit computation of complex path type inhabitants.
DOI 原文 ·
@inproceedings{paperbot8671,
title = {Naturality for higher-dimensional path types},
author = {Thibaut Benjamin and Ioannis Markakis and Wilfred Offord and Chiara Sarti and Jamie Vicary},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00028}
}