C-system of a module over a monad on sets 1

By Vladimir Voevodsky. 2014

10 citations recorded by the source corpus.

AbstractThis is the second paper in a series started in [13] which aims to provide mathematicaldescriptions of objects and constructions related to the rst few steps of the semantical theoryof dependent type systems.We construct for any pair ( M;LM ), where M is a monad on sets and LM is a left moduleover M , a C-system (\contextual category") CC ( M;LM ) and describe, using the results of [13]a class of sub-quotients of CC ( M;LM ) in terms of objects directly constructed from M and LM . In the special case of the monads of expressions associated with nominal signatures thisconstruction gives the C-systems of general dependent type theories when they are speci ed bycollections of judgements of the four standard kinds. 1 Introduction The rst few steps in all approaches to the semantics of dependent type theories remain ffitlyunderstood. The constructions which have been worked out in detail in the case of a few particulartype systems by dedicated authors are being extended to the wide variety of type systems underconsideration today by analogy. This is not acceptable in mathematics. Instead we should be ableto obtain the required results for new type systems by

Citations in the corpus