Categorical models of dependent type theory

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

• Nathanael Arkor (University of Cambridge)
• Friday 26 February 2021, 11:00-12:00
• https://meet.google.com/jxy-edcv-wgx.

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.

This talk is included in these lists:

• Logic & Semantics for Dummies
• https://meet.google.com/jxy-edcv-wgx
• tcw57’s list
• yk373's list

Note that ex-directory lists are not shown.