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
& Hillman Centers 6501
of Programming Seminars