C-system of a module over a $Jf$-relative monad

TL;DR

This paper constructs a C-system from a relative monad and a module over it, providing explicit computations of the system's operations, which aids in formalizing models of dependent type theories.

Contribution

It introduces a detailed construction of C-systems from relative monads and modules, expanding on previous work with explicit calculations and broader applicability.

Findings

Explicit construction of C-systems from relative monads and modules

Detailed computation of B-system operations on C-systems

Foundation for rigorous models of dependent type theories

Abstract

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.