Zusammenfassung
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.
Nutzer