C-system of a module over a \(Jf\)-relative monad (Q2689172)

This paper aims to study the B-systems arising from presheaf extensions of a C-system. These B-systems significant on the construction of sub-quotients of C-systems. Specifically, to construct the regular sub-quotients of \(C(\boldsymbol{RR},\boldsymbol{LM})\) that corresponds to the type system generated by the given system of inference rules. In order to be able to describe regular sub-quotients of a C-system, one needs to know its \textit{pre-B-system} [\url{arXiv:1416.5389}]. The principal result of the paper is a detailed description of the pre-B-system of the form \(\left(B(CC[F]),\widetilde{B}(CC[F])\right)\) for an important class of coefficient C-systems \(CC\). The synopsis of the paper goes as follows. \begin{itemize} \item[\S 2] gives an overview of relative monads and left modules over relative monads. The author first recall the notion of relative monad on a functor \(J:C\rightarrow D\) that was introduced in [\textit{T. Altenkirch} et al., Lect. Notes Comput. Sci. 6014, 297--311 (2010; Zbl 1284.18010), Definition 1, p.299] and considered in more detail in [\textit{T. Altenkirch} et al., Log. Methods Comput. Sci. 11, No. 1, Paper No. 3, 40 p. (2015; Zbl 1448.18007)]. He then focuses his attention on relative monads over the functor \(Jf\). \item[\S 3] furcates into two subsection. \S 3.1 reintroduces some of the objects and constructions defined in [\textit{V. Voevodsky}, Contemp. Math. 658, 127--137 (2016; Zbl 1452.03040)] by using the partial ordering which is defined on the set of objects of any C-system as \[ X\leq Y\text{ iff }l(X)\leq l(Y)\text{ and }X=ft^{l(Y)-l(X)}(Y) \] \S 3.2 constructs for any C-system \(CC\) and a presheaf \(F\) on the category underlying \(CC\) a new C-system \(CC[F]\), called the \(F\)-extension of \(CC\) and reminiscent of affine spaces over schemes in algebraic geomety. \item[\S 4] multifurcates into three subsections. \S 4.1 is occupied by simple computations in \(K(\boldsymbol{RR})\) for \(Jf\)-relative monads \(\boldsymbol{RR}\). \S 4.2 considers the C-system \(C(\boldsymbol{RR})\) corresponding to the Lawvere theory \(RML(\boldsymbol{RR})\) defined by a \(Jf\)-relative monad \(\boldsymbol{RR}\), the underlying category of this C-system being \(K(\boldsymbol{RR})^{\mathrm{op}}\). The main result is the description of the B-sets of \(C(\boldsymbol{RR})\) and of the actions of the B-system operations on these sets. \S 4.3 applies the construction of \S 3.2 to \(C(\boldsymbol{RR})\) in taking into account that the functors \[ \boldsymbol{LM}:C(\boldsymbol{RR})^{\mathrm{op}}\rightarrow Sets \] are the same as the functors \[ K(\boldsymbol{RR})\rightarrow Sets \] that are in turn the same as the relative (left) modules over \(Jf\). The B-sets \(B(C(\boldsymbol{RR},\boldsymbol{LM}))\) and \(\widetilde{B}(C(\boldsymbol{RR},\boldsymbol{LM}))\) are computed, and the action of the B-system operations on these sets is determined. \end{itemize}