C-system of a module over a monad on sets

2014/07/12 by Voevodsky, Vladimir
#03B15 #03B22 #03F50 #03G25 #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.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.

Related

• C-system of a module over a Jf-relative monad
• Subsystems and regular quotients of C-systems
• The Interpretation Lifting Theorem for C-Systems
• Martin-Lof identity types in the C-systems defined by a universe category
• Products of families of types and (Pi,lambda)-structures on C-systems