Fredrik Nordvall-Forsberg
Postdoc in the Mathematically Structured Programming group at Strathclyde University, UK
Towards a Presentation of General Higher Inductive Types
Abstract:
Lumsdaine and Shulman's concept of Higher Inductive Types (HITs) is one of the major new features of Homotopy Type Theory (HoTT). 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. However, while we know of particular examples of HITs, we do not yet have a general schema for well-behaved such definitions.
In this talk, I will give an introduction to HITs, and then report on work in progress together with Thorsten Altenkirch and his students on defining a schema for a very general class of HITs internally to HoTT. This schema covers all the examples of HITs that I know of, and is more general than the schemas proposed by e.g. Shulman or Barras.
Bio: Fredrik Nordvall-Forsberg is a postdoc in the Mathematically Structured Programming group at Strathclyde University, UK. He received his PhD from Swansea University, UK in 2013. His interests include (Homotopy) Type Theory, constructive mathematics and categorical methods in Computer Science. Currently, he is visiting CMU on the CORCON poject.