Pith. sign in

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

1 Pith paper cite this work. Polarity classification is still indexing.

1 Pith paper citing it
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.

fields

math.CT 1

years

2024 1

verdicts

CONDITIONAL 1

representative citing papers

citing papers explorer

Showing 1 of 1 citing paper.