Fredrik Nordvall-Forsberg
Postdoc in the Mathematically Structured Programming group at Strathclyde University, UK

Towards a Presentation of General Higher Inductive Types

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.

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.

Monday, September 22, 2014
3:00 PM
Gates & Hillman Centers 6501

Principles of Programming Seminars