Subsystems and regular quotients of C-systems
Subsystems and regular quotients of C-systems
复制标题
C 系统的子系统和正则商
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
V. Voevodsky
中科院分区：
文献类型：
--
作者：
V. Voevodsky
C-系统是由J.Cartmell以“语境范畴”的名义提出的。在本文中，我们研究了C-系统的子对象和商对象。在子对象的情况下，我们考虑所有子对象，而在商对象的情况下，只考虑正则商，其特别地具有对应的投影态射在对象上和在态射上都是满射的性质。这些结果一方面为B-系统理论提供了基础，另一方面也为相依型理论的“结构规则”的形式提供了代数解释的基础。本文是基于同一作者的《关于类型系统的注解》材料的几篇短文之一。
C-systems were introduced by J. Cartmell under the name "contextual categories". In this note we study sub-objects and quotient-objects of C-systems. In the case of the sub-objects we consider all sub-objects while in the case of the quotient-objects only regular quotients which in particular have the property that the corresponding projection morphism is surjective both on objects and on morphisms. These results provide on the one hand the basis for the theory of B-systems and on the other the basis for an algebraic explanation of the form of the "structural rules" of dependent type theories. This text is one of several short papers based on the material of the "Notes on Type Systems" by the same author.