Swan 问题

Andrew Swan 在 [Swan 2018] 中猜想, 对于立方类型论, 如下三个性质只有两个能同时成立:

•	典范性、正规性, 对应了类型规则的可判定性.
•	宇宙满足泛等公理, 也是同伦类型论中大量证明的基石.
•	J 公理满足严格的计算规则, 即正则性.

立方类型论中的道路类型和直接使用 $\mathrm{refl}$ 作为构造规则的相等类型是等价的, 而后者显然满足严格的计算规则, 所以这个需求在一定程度上被满足. 因此, 立方类型论的设计选择了前两个性质.

1参考资料

•	Andrew Swan (2018). “Separating Path and Identity Types in Presheaf Models of Univalent Type Theory”. arXiv: 1808.00920.