BLC 2010

Formalising inductive-inductive definitions
Fredrik Forsberg
Induction principles are powerful and important principles of definition, especially so in dependent type theory and constructive mathematics. Induction-induction is an induction principle which generalises indexed inductive definitions. It gives the possibility to simultaneously introduce a set A together with an A-indexed set B, i.e. for every a : A, B(a) is a set. Both A and B(a) are inductively defined, and the constructors for A can also refer to B and vice versa. Instances of induction-induction have implicitly been used by several researchers (Dybjer, Danielsson, Chapman) to model type theory inside type theory, and inductive-inductive definitions are available in the proof assistant/programming language Agda, but without justification of the principle. In this talk, we will discuss how to formalise inductive-inductive definitions. We will also sketch how inductive-inductive definitions can be reduced to ordinary indexed inductive definitions, which shows that they have the same proof theoretical strength.