skip to content

Schemas and semantics for Higher Inductive Types

Presented by: 
Peter LeFanu Lumsdaine Stockholm University
Tuesday 11th July 2017 - 16:00 to 17:00
INI Seminar Room 1
Higher inductive types are now an established tool of homotopy type theory, but many important questions about them are still badly-understood, including:
  • can we set out a scheme defining “general HITs”, analogously to how CIC defines “general inductive types”?
  • can we find a small specific collection of HITs from which one can construct “all HITs”, analogously to how the type-formers of MLTT suffice for inductive types?
  • how can we model HITs (specific or general) in interesting homotopical settings?
I will survey these questions and present what I know of progress on them (in particular, the cell monads semantics of Lumsdaine/Shulman; I will also open the floor for interested audience members to briefly present other current work on these topics.
The video for this talk should appear here if JavaScript is enabled.
If it doesn't, something may have gone wrong with our embedded player.
We'll get it fixed as soon as possible.
Presentation Material: 
University of Cambridge Research Councils UK
    Clay Mathematics Institute London Mathematical Society NM Rothschild and Sons