English

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 (R,LM)(R,LM), where RR is a monad on sets and LMLM is a left module over RR, a C-system (contextual category) CC(R,LM)CC(R,LM) and describe a class of sub-quotients of CC(R,LM)CC(R,LM) in terms of objects directly constructed from RR and LMLM. 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.

Keywords

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}
}
R2 v1 2026-06-22T05:02:41.052Z