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 and Semantics Seminar (Computer Laboratory)
SUMMARY:Higher Categorical Structures\, Type-Theoretically
- Nicolai Kraus\, University of Nottingham
DTSTART;TZID=Europe/London:20170512T140000
DTEND;TZID=Europe/London:20170512T150000
UID:TALK72605AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/72605
DESCRIPTION:Category theory internally in homotopy type theory
is intricate as categorical laws can only be stat
ed 'up to homotopy'\, requiring coherence (similar
to how the associator in a bicategory requires th
e pentagon). To avoid this\, one can consider def
initions with truncated types such as the univalen
t categories by Ahrens-Kapulkin-Shulman\, which ho
wever fail to capture some important examples. A
more general structure are (n\,1)-categories\, ide
ally with n = infinity\, and a possible definition
is given by Capriotti's complete semi-Segal types
. I will show how simplified (complete) semi-Sega
l types are indeed equivalent to univalent categor
ies.\nVery much related is the question what an ap
propriate notion of a type-valued diagram is (join
t work with Sattler). Using the type universe as
a semi-Segal type\, I will present several constru
ctions of homotopy coherent diagrams (some of them
infinite) and show\, as an application\, how one
can construct all the degeneracies that a priori a
re missing in a complete semi-Segal type. With a
further construction\, we get a (finite) definitio
n of simplicial types (up to a finite level).
LOCATION:FW26
CONTACT:Dominic Mulligan
END:VEVENT
END:VCALENDAR