C-system of a module over a monad on sets
Logic
2014-09-30 v3
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 , where is a monad on sets and is a left module over , a C-system (contextual category) and describe a class of sub-quotients of in terms of objects directly constructed from and . 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.
Cite
@article{arxiv.1407.3394,
title = {C-system of a module over a monad on sets},
author = {Vladimir Voevodsky},
journal= {arXiv preprint arXiv:1407.3394},
year = {2014}
}