Indexed induction–recursion

An indexed inductive definition (IID) is a simultaneous inductive definition of an indexed family of sets. An inductive–recursive definition (IRD) is a simultaneous inductive definition of a set and a recursive definition of a function on that set. An indexed inductive–recursive definition (IIRD) is a combination of both.We present a closed theory which allows us to introduce all IIRD in a natural way without much encoding. By specialising it we also get a closed theory of IID. Our theory of IIRD includes essentially all definitions of sets which occur in Martin–Löf type theory. We show in particular that Martin–Löf’s computability predicates for dependent types and Palmgren’s higher order universes are special kinds of IIRD and thereby clarify why they are constructively acceptable notions.We give two axiomatisations. The first formalises a principle for introducing meaningful IIRD by using the data-construct in the original version of the proof assistant Agda for Martin–Löf type theory. The second one admits a more general form of introduction rule, including the introduction rule for the intensional identity relation, which is not covered by the first axiomatisation. If we add an extensional identity relation to our logical framework, we show that the theories of restricted and general IIRD are equivalent by interpreting them in each other.Finally, we show the consistency of our theories by constructing a model in classical set theory extended by a Mahlo cardinal.