BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Higher Categorical Structures\, Type-Theoretically - Nicolai Kraus
 \, University of Nottingham
DTSTART:20170512T130000Z
DTEND:20170512T140000Z
UID:TALK72605@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:Category theory internally in homotopy type theory is intricat
 e as categorical laws can only be stated 'up to homotopy'\, requiring cohe
 rence (similar to how the associator in a bicategory requires the pentagon
 ).  To avoid this\, one can consider definitions with truncated types such
  as the univalent categories by Ahrens-Kapulkin-Shulman\, which however fa
 il to capture some important examples.  A more general structure are (n\,1
 )-categories\, ideally with n = infinity\, and a possible definition is gi
 ven by Capriotti's complete semi-Segal types.  I will show how simplified 
 (complete) semi-Segal types are indeed equivalent to univalent categories.
 \nVery much related is the question what an appropriate notion of a type-v
 alued diagram is (joint work with Sattler).  Using the type universe as a 
 semi-Segal type\, I will present several constructions of homotopy coheren
 t diagrams (some of them infinite) and show\, as an application\, how one 
 can construct all the degeneracies that a priori are missing in a complete
  semi-Segal type.  With a further construction\, we get a (finite) definit
 ion of simplicial types (up to a finite level).
LOCATION:FW26
END:VEVENT
END:VCALENDAR