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

AI 速览

一句话：为依赖类型论给出一类保持单价性（univalence）的简单内模型构造。

依赖类型论中单价性公理的模型构造是类型论语义的核心问题之一。Coquand 提出一种简单的内模型构造（inner model construction），用于依赖类型论，并证明该构造保持单价性成立。所谓内模型，意味着在依赖类型论自身内部建立对理论的解释，而非仅在外部元语言中通过预层或单纯集合等结构刻画语义，从而可将部分外部语义论证转化为内部可形式化的构造。其关键结果是该内模型保持 univalence，即单价性在该解释下仍然成立。摘要未给出具体形式化细节或评估方式，工作属于类型论语義与模型构造方向。

问题

如何在依赖类型论中构造一个内模型，并使其保持单价性公理成立。

方法

提出一种简单的内模型构造（inner model construction），用于依赖类型论，并论证该构造保持 univalence。

评估

摘要未说明具体评估或机器化验证；作者以该内模型保持单价性作为主要理论结果。

链接与引用

DOI 原文 ·

@inproceedings{paperbot4322,
  title = {Inner Models of Univalence},
  author = {Thierry Coquand},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209112}
}