Fredrik Nordvall Forsberg: Applications and theory of Higher inductive types
Applications and theory of Higher inductive types
Homotopy Type Theory is a foundational system and programming language that connects ideas from type theory and homotopy theory: we think of types as spaces, terms as points in a space, and of Martin-Löf's identity type as the path space of a given space. This led Lumsdaine and Shulman to consider a generalisation of inductive types, where not only points are freely generated, but also paths, paths between paths, and so on. Inductive types with such higher-dimensional generators are called Higher Inductive Types (HITs). HITs generalise ordinary inductive types, as well as quotient types, but also geometrical objects such as intervals, spheres or tori can be represented using HITs, leading the way to synthetic homotopy theory.
In this talk, I will give a gentle introduction to HITs. I will survey some of their applications, such as doing homotopy theory inside Homotopy Type Theory. I will then talk about the surprisingly relatively undeveloped theory underlying HITs. While we know many particular examples of HITs, we do not yet have a general schema for well-behaved definitions. Moreover, even for simple, "well-understood" HITs, we do not have proof-theoretical results such as normalisation or confluence. Trying to rectify this is joint work with Thorsten Altenkirch, Paolo Capriotti and Gabe Dijkstra.
