BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Lab Lunch
SUMMARY:Internal higher-categorical models of dependent ty
pe theory - Nicolai Kraus (University of Birmingha
m)
DTSTART:20191024T110000Z
DTEND:20191024T120000Z
UID:TALK3962AT
URL:/talk/index/3962
DESCRIPTION:Using dependent type theory to formalise models of
dependent type theory is an active topic of study
. Formalising the initial such model goes under th
e name of "type theory eating itself" or "type the
ory in type theory". I will explain why this is di
fficult in the absence of the principle of unique
identity proofs (UIP)\, and how higher categorical
models connect two long-standing open problems of
homotopy type theory.
LOCATION:CS 217
CONTACT:Todd Waugh Ambridge
END:VEVENT
END:VCALENDAR