Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 2 of 2
I see there a preprint just out
We present a generalization of cartesian closed categories (CCCs) for dependent types, called dependent cartesian closed categories (DCCCs), which also provides a reformulation of categories with families (CwFs), an abstract semantics for Martin-Löf type theory (MLTT) which is very close to the syntax. Thus, DCCCs accomplish mathematical elegance as well as a direct interpretation of the syntax. Moreover, they capture the categorical counterpart of the generalization of the simply-typed lambda-calculus (STLC) to MLTT in syntax, and give a systematic perspective on the relation between categorical semantics for these type theories. Furthermore, we construct a term model from the syntax, establishing the completeness of our interpretation of MLTT in DCCCs.
So he reviews Martin-Loef Type Theory (MLTT) an Categories with Families (CwF) and how the former can be interpreted in the latter. Then he introduces Dependent Categories with nice features (DCCC), which I think have a relatively straight forward definition and how those induce relevant CwF. It’s too bad he doesn’t seem to discuss “MLTT in DCCC” directly, you need to read up the whole bridge over CwFs to understand what’s happening.
1 to 2 of 2