一句话：在单值类型论中比较三种依赖类型论的范畴模型，并给出 Coq 形式化。
论文研究依赖类型理论的范畴语义，比较三类代数结构：categories with families、分裂类型范畴以及预层可表示映射。作者在单值类型论而非集合论基础中展开工作，构造这些结构类型之间的映射，并证明在单值公理下部分比较构成等价。文章还分析这些结构沿弱、强范畴等价的迁移，尤其说明它们如何从普通范畴下降到其 Rezk 完备化；为此引入相对宇宙并研究其沿适当结构的迁移。全部内容已在 UniMath 库上用 Coq 形式化，部分结果依赖单值公理。
In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in univalent type theory, where the comparisons between them can be given more elementarily than in set-theoretic foundations. Specifically, we construct maps between the various types of structures, and show that assuming the Univalence axiom, some of the comparisons are equivalences. We then analyze how these structures transfer along (weak and strong) equivalences of categories, and, in particular, show how they descend from a category (not assumed univalent/saturated) to its Rezk completion. To this end, we introduce relative universes, generalizing the preceding notions, and study the transfer of such relative universes along suitable structure. We work throughout in (intensional) dependent type theory; some results, but not all, assume the univalence axiom. All the material of this paper has been formalized in Coq, over the UniMath library.Comment: v2: revised and extended version for publication in LMCS
@article{paperbot378,
title = {Categorical structures for type theory in univalent foundations},
author = {Benedikt Ahrens and Peter LeFanu Lumsdaine and Vladimir Voevodsky},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 3},
year = {2018},
doi = {10.23638/lmcs-14(3:18)2018}
}