2016/02/01 by Vladimir Voevodsky, Voevodsky, Vladimir
Mathematics · #18C50 #18D99 #Algebraic structures and combinatorial models #Category Theory (math.CT) #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO) #Rings, Modules, and Algebras
paper · pdf · doi:10.48550/arxiv.1602.00352
openalex publication_date 2016/02/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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→ 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.