University of Cambridge > > Logic & Semantics for Dummies > Categorical models of dependent type theory

Categorical models of dependent type theory

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Nathanael Arkor.

Just as simple type theories can be interpreted in cartesian categories, so too can dependent type theories be interpreted in categories with sufficient limits. I will start by recalling the relationship between algebraic theories, cartesian categories, and simple type theories, before introducing generalisations of each to dependent type theories. There are several categorical formalisms of dependent types in vogue: I will focus on contextual categories, C-systems, categories with attributes, and finitely complete categories; time permitting, I will also outline the relationship to fibrational models, such as comprehension categories.

This talk is part of the Logic & Semantics for Dummies series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity