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.

Principles
of Programming Seminars