BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Categorical models of dependent type theory - Nathanael Arkor (Uni
 versity of Cambridge)
DTSTART:20210226T110000Z
DTEND:20210226T120000Z
UID:TALK157318@talks.cam.ac.uk
CONTACT:Nathanael Arkor
DESCRIPTION:Just as simple type theories can be interpreted in cartesian c
 ategories\, so too can dependent type theories be interpreted in categorie
 s with sufficient limits. I will start by recalling the relationship betwe
 en algebraic theories\, cartesian categories\, and simple type theories\, 
 before introducing generalisations of each to dependent type theories. The
 re 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 t
 he relationship to fibrational models\, such as comprehension categories.
LOCATION:https://meet.google.com/jxy-edcv-wgx
END:VEVENT
END:VCALENDAR