我的阅读状态 （保存写回仓库，全设备同步；首次保存需输入访问令牌）

AI 速览

一句话：在 n-截断类型论中研究部分 univalence，并解释其与 UIP 不相容的根源。

论文关注 univalence 与 uniqueness of identity proofs (UIP) 的已知冲突：UIP 要求所有类型都是 h-set，而 univalence 会使有限 h-set 在其不是 h-proposition 时产生非平凡自同构，因此二者不能同时成立。作者在 n-truncated type theory 的设定下研究 partial univalence，即对 univalence 加以截断层级限制，以考察其与 UIP 能否相容。摘要给出的核心观察是，冲突并非仅来自一般类型，而是源于有限 h-set 的自同构结构；当有限 h-set 超出 h-proposition 层级时，非平凡自同构必然出现。摘要未展开具体构造、形式化证明或模型评估。

问题

univalence 与 UIP 不相容；UIP 将所有类型视为 h-set，而 univalence 会导致非 h-proposition 的有限 h-set 出现非平凡自同构。

方法

在 n-truncated type theory 中研究 partial univalence，通过对 univalence 施加截断限制来考察二者关系；具体方法摘要未详述。

评估

摘要未说明评估方式；从题名与摘要看，属于类型论的理论/形式化研究。

链接与引用

DOI 原文 · PDF（开放获取） ·

@inproceedings{paperbot5502,
  title = {Partial Univalence in n-truncated Type Theory},
  author = {Christian Sattler and Andrea Vezzosi},
  booktitle = {LICS},
  year = {2020},
  doi = {10.1145/3373718.3394759}
}