%0 Journal Article %1 voevodsky2014csystem-monad %A Voevodsky, Vladimir %D 2014 %K C-system HoTT module monad %T C-system of a module over a monad on sets %U http://arxiv.org/abs/1407.3394 %X 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.

@article{voevodsky2014csystem-monad, abstract = {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.}, added-at = {2014-11-17T13:19:45.000+0100}, author = {Voevodsky, Vladimir}, biburl = {https://www.bibsonomy.org/bibtex/2dce8cb57e943f2ee44ed5a30aec1fde9/t.uemura}, description = {C-system of a module over a monad on sets}, interhash = {975e7183af2e87dc239e72a93fd375fb}, intrahash = {dce8cb57e943f2ee44ed5a30aec1fde9}, keywords = {C-system HoTT module monad}, note = {cite \href{http://arxiv.org/abs/1407.3394}{arxiv:1407.3394}}, timestamp = {2014-11-18T09:33:45.000+0100}, title = {C-system of a module over a monad on sets}, url = {http://arxiv.org/abs/1407.3394}, year = 2014 }