V. Voevodsky. (2014)cite http://arxiv.org/abs/1407.3394arxiv:1407.3394.
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.
%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
}