The joy of QIITs

Thorsten Altenkirch, University of Nottingham. Part of the logic seminar series.

'Quotient inductive inductive types (QIITS) are set-truncated mutually defined higher inductive types. I am going to discuss two applications of QIITs:

1. define an internal syntax of Type Theory without reference to untyped preterm;

2. define a version of the partiality monad that doesn\'t require countable choice.

On the one hand I think that these applications are interesting because they represent applications of HoTT which have nothing to do with homotopy theory; on the other hand they are clearly not very higher order (in the sense of truncation levels) but can be defined in the set-truncated fragment of HoTT. Hence my question: what are interesting applications of higher types which are not directed related to synthetic homotopy theory?

This talk is based on joint work with Paolo Capriotti, Nils Anders Danielsson, Gabe Dijkstra, Ambrus Kaposi and Nicolai Kraus.

Thorsten Altenkirch, University of Nottingham