BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:Higher Universal Algebra in Type Theory - Eric Fin
ster\, INRIA\, Paris
DTSTART:20190122T150000Z
DTEND:20190122T160000Z
UID:TALK3480AT
URL:/talk/index/3480
DESCRIPTION:I will describe recent progress on understanding h
igher algebraic structures in dependent type theor
y. In particular\, I show how one can define a co
herent version of polynomial monad\, whose special
cases include definitions of $(\\infty\,1)$-categ
ory and $\\infty$-groupoid. I will also explain h
ow these techniques yield a definition of simplici
al type\, discuss progress on formalization and fo
rmulate a number of conjectures aimed testing the
definition's suitability.
LOCATION:Computer Science\, 245
CONTACT:Jamie Vicary
END:VEVENT
END:VCALENDAR