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 it combination of both. We present a closed theory which allows Lis 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-Lof type theory. We show in particular that Martin-Lof'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-Lof 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. (c) 2005 Elsevier Inc. All rights reserved.
inductive definitions inductive-recursive definitions martin-lof type theory dependent type theory inductive families initial algebras normalisation proofs generic programming