Inductive-inductive definitions

Fredrik Nordvall Forsberg


We present inductive-inductive definitions, a principle for introducing new sets in Martin-Loef type theory which generalise indexed inductive data types. The principle allows one to simultaneously introduce a set A together with an A-indexed set B, where A and B(a) for a : A are mutually inductively defined. Instances of this principle have been used to formalise type theory inside type theory, but without justification why this is consistent or constructively valid.

In this talk, we will introduce the notion of inductive-inductive definitions and then give a closed axiomatisation. We prove consistency by constructing a set theoretic model.
Thursday 11th February 2010, 14:00
Far-134 (Video Conferencing Room)
Department of Computer Science