BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic &amp\; Semantics for Dummies
SUMMARY:Categorical models of dependent type theory - Nath
 anael Arkor (University of Cambridge)
DTSTART;TZID=Europe/London:20210226T110000
DTEND;TZID=Europe/London:20210226T120000
UID:TALK157318AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/157318
DESCRIPTION:Just as simple type theories can be interpreted in
  cartesian categories\, so too can dependent type 
 theories be interpreted in categories with suffici
 ent limits. I will start by recalling the relation
 ship between algebraic theories\, cartesian catego
 ries\, and simple type theories\, before introduci
 ng generalisations of each to dependent type theor
 ies. There are several categorical formalisms of d
 ependent types in vogue: I will focus on contextua
 l categories\, C-systems\, categories with attribu
 tes\, and finitely complete categories\; time perm
 itting\, I will also outline the relationship to f
 ibrational models\, such as comprehension categori
 es.
LOCATION:https://meet.google.com/jxy-edcv-wgx
CONTACT:Nathanael Arkor
END:VEVENT
END:VCALENDAR