宇宙范畴定义的C-系统中的Martin-Lof恒等类型
范畴论
2015-05-26 v1
摘要
本文继续了一系列开发依赖类型理论的语法和语义新方法的论文。在此我们研究由宇宙范畴产生的C-系统上，内涵性Martin-Lof类型理论中的恒等类型规则的释义。在论文第一部分，我们发展了从宇宙范畴上的某些结构产生这些规则的释义的构造，而在第二部分我们研究了这些构造关于宇宙范畴函子的函子性。论文第一部分的结果在单纯集上类型理论的单值模型的构造中起着关键作用。
引用
@article{arxiv.1505.06446,
title = {Martin-Lof identity types in the C-systems defined by a universe category},
author = {Vladimir Voevodsky},
journal= {arXiv preprint arXiv:1505.06446},
year = {2015}
}