$Jf$ -相对单子上模的C-系
C-system of a module over a $Jf$-relative monad
摘要：
令$F$是具有对象集$\bf N$和态射的范畴，态射是对应基数的标准有限集之间的函数。设$Jf:F\rightarrow Sets$是从这个范畴到集合的集范畴的明显函子。本文对$Jf$上的相对单子$\bf RR$和$\bf RR$上的左模$\bf LM$构造了一个C-系统$C({\bf RR},{\bf LM})$，并显式地计算了B-系统运算在其B-集上的作用.在下面的文件中，它是用来提供一个严格的数学方法来建设的C-系统的长期模型的一个广泛的依赖类型的理论。这篇论文是arXiv：1407.3394进化的结果。然而，这篇论文要详细得多，包含了很多arXiv：1407.3394中没有包含的材料。它也不包括arXiv：1407.3394中涵盖的一些材料。
英文摘要：
Let $F$ be the category with the set of objects $\bf N$ and morphisms being the functions between the standard finite sets of the corresponding cardinalities. Let $Jf:F\rightarrow Sets$ be the obvious functor from this category to the category of sets. In this paper we construct, for any relative monad $\bf RR$ on $Jf$ and a left module $\bf LM$ over $\bf RR$, a C-system $C({\bf RR},{\bf LM})$ and explicitly compute the action of the B-system operations on its B-sets. In the following paper it is used to provide a rigorous mathematical approach to the construction of the C-systems underlying the term models of a wide class of dependent type theories. This paper is a result of evolution of arXiv:1407.3394. However this paper is much more detailed and contains a lot of material that is not contained in arXiv:1407.3394. It also does not cover some material that is covered in arXiv:1407.3394.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
