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

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Categorical models of dependent type theory

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Webex BAS Seminar Room 1; https://bas-ac-uk.zoom.us/j/94373277038 SG1/2, Alison Richard Building, Cambridge, CB3 9DT

Other talks

Group Work Title to be confirmed Unveiling the curtain with ukubuyisa or go lata: complicated roles of museums and nation states in the cultural repatriation discourse and practice in southern Africa Organiser's Welcome Emergency Medicine and Metabolic Medicine Polar Oceans Seminar Talk
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity