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:Category Theory Seminar
SUMMARY:Two-Level Type Theory - Nicolai Kraus (University
of Nottingham)
DTSTART;TZID=Europe/London:20171107T141500
DTEND;TZID=Europe/London:20171107T151500
UID:TALK94090AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/94090
DESCRIPTION:I give an introduction to *two-level type theory*\
, a system that can combine two Martin-Lof style t
ype theories. We can take one of them to be homot
opy type theory (HoTT)\, and the other to be a ver
sion of MLTT with unique identity proofs. This yi
elds an extension of HoTT where a "type of strict
equalities" is available\, and from the point of v
iew of HoTT\, this strict equality can be compared
to judgmental/definitional equality\; essentially
\, we get a variant of HoTT where it is possible t
o reason internally about judgmental equality.\n
This system can be understood as a variant of Voev
odsky's *homotopy type system* (HTS). Both HTS an
d two-level type theory address the issue that cer
tain higher-categorical structures cannot be suita
bly encoded in standard HoTT (cf. semisimplicial t
ypes).\n Two-level type theory has been suggested
by Altenkirch-Capriotti-K (arXiv:1604.03799 / CSL
'16)\, developed further by Annenkov-Capriotti-K (
arXiv:1705.03307)\, and a conservativity result ha
s been shown by Capriotti (arXiv:1702.04912 / PhD
thesis).
LOCATION:MR5\, Centre for Mathematical Sciences
CONTACT:Tamara von Glehn
END:VEVENT
END:VCALENDAR