类型族乘积与 C-系统上的 (Pi,lambda)-结构
范畴论
2017-06-13 v1
摘要
本文继续研究 C-系统上最重要的结构，这些结构在句法 C-系统的情况下对应于 -推理规则系统。其中一种结构由 J. Cartmell 引入，后来由 T. Streicher 以类型族乘积的名义进行了研究。我们引入了 (Pi,lambda)-结构的概念，并为给定的 C-系统构造了 (Pi,lambda)-结构集合与 Cartmell-Streicher 结构集合之间的双射。在后续论文中，我们将展示如何构造并在某些情况下完全分类对应于宇宙范畴的 C-系统上的 (Pi,\lambda)-结构。本文第一节对一般 C-系统的许多性质提供了仔细的证明。本文的方法是全然构造性的，即既不使用排中律公理，也不使用选择公理。
引用
@article{arxiv.1706.03605,
title = {Products of families of types and (Pi,lambda)-structures on C-systems},
author = {Vladimir Voevodsky},
journal= {arXiv preprint arXiv:1706.03605},
year = {2017}
}
备注
The first part of the paper adds to the general theory of C-systems and may be used as an advanced introduction into C-systems. The paper is the first of the three papers into which the preprint "Products of families of types in the C-systems defined by a universe category" evolved during publication. The paper is published in Theory and Applications of Categories