C-system of a module over a monad on sets

Original · EN

This is the second paper in a series that aims to provide mathematical descriptions of objects and constructions related to the first few steps of the semantical theory of dependent type systems. We construct for any pair (R,LM), where R is a monad on sets and LM is a left module over R, a C-system (contextual category) CC(R,LM) and describe a class of sub-quotients of CC(R,LM) in terms of objects directly constructed from R and LM. In the special case of the monads of expressions associated with nominal signatures this construction gives the C-systems of general dependent type theories when they are specified by collections of judgements of the four standard kinds.