Abstract

The slides for this talk are at http://www.cs.swan.ac.uk/~csetzer/slides/index.html.

Inductive-recursive definitions were developed by P. Dybjer as a concepts which formalises the principle for introducing sets in Martin-Loef Type Theory. Indexed inductive-recursive definitions extend this principle by the possibility, to introduce simultaneously several sets inductive-recursively.

All sets definable in the core of Martin-Loef type theory, which is accepted by most researchers in this area, are instances of indexed inductive-recursive definitions. It contains as well many extensions, for instance Erik Palmgren’s superuniverses and higher universes. Many data types which are used in programming and theorem proving are instances of indexed inductive-recursive definitions, e.g. the accessible part of an ordering, Martin-Loef’s computability predicate, which was used in his normalisation proof for one version of Martin-Loef type theory, and Bove and Carpretta’s formalisation of partial functions in type theory.

In this lecture we will introduce the notions of inductive-recursive definitions and indexed inductive-recursive definitions. We will show how to introduce inductive-recursive defintions using finitely many rules. We look at the relationship between inductive-recursive definitions and initial algebras. We will then investigate new extensions of type theory, which look at first sight like inductive-recursive definitions, but are of different nature.