BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Schemas and semantics for Higher Inductive Types - Peter LeFanu Lu
 msdaine (Stockholm University)
DTSTART:20170711T150000Z
DTEND:20170711T160000Z
UID:TALK73234@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:Higher inductive types are now an established tool of homotopy
  type theory\, but many important questions about them are still badly-und
 erstood\, including:can we set out a scheme defining &ldquo\;general HITs&
 rdquo\;\, analogously to how CIC defines &ldquo\;general inductive types&r
 dquo\;?can we find a small specific collection of HITs from which one can&
 nbsp\;construct &ldquo\;all HITs&rdquo\;\, analogously to how the type-for
 mers of MLTT suffice for&nbsp\;inductive types?how can we model HITs (spec
 ific or general)&nbsp\;in interesting&nbsp\;homotopical settings?I will su
 rvey these questions and present what I know of progress on them (in parti
 cular\, the cell monads semantics of Lumsdaine/Shulman&nbsp\;https://arxiv
 .org/abs/1705.07088)\; I will also open the floor for interested audience 
 members to briefly present other current work on these topics.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR