Indexed induction-recursion

Abstract

We give two finite axiomatizations of indexed inductive-recursive definitions in intuitionistic type theory. They extend our previous finite axiomatizations of inductive-recursive definitions of sets to indexed families of sets and encompass virtually all definitions of sets which have been used in intuitionistic type theory. The more restricted of the two axiomatization arises naturally by considering indexed inductive-recursive definitions as initial algebras in slice categories, whereas the other admits a more general and convenient form of an introduction rule. The class of indexed inductive-recursive definitions properly contains the class of indexed inductive definitions (so called “inductive families”). Such definitions are ubiquitous when using intuitionistic type theory for formalizing mathematics and program correctness. A side effect of the present paper is to get compact finite axiomatizations of indexed inductive definitions in intuitionistic type theory as special cases. Proper indexed inductive-recursive definitions (those which do not correspond to indexed inductive definitions) are useful in intuitionistic metamathematics, and as an example we formalize Tait-style computability predicates for dependent types. We also show that Palmgren’s prooftheoretically strong construction of higher-order universes is an example of a proper indexed inductive-recursive definition. A third interesting example is provided by Bove and Capretta’s definition of termination predicates for functions defined by nested recursion. Our axiomatizations form a powerful foundation for generic programming with dependent types by introducing a type of codes for indexed inductive-recursive definitions and making it possible to define generic functions by recursion on this type.