Abstract

The first example of a simultaneous inductive-recursive definition in intuitionistic type theory is Martin-Lof's universe a la Tarski. A set U$_0$ of codes for small sets is generated inductively at the same time as a function T$_0$, which maps a code to the corresponding small set, is defined by recursion on the way the elements of U$_0$ are generated. In this paper we argue that there is an underlying general notion of simultaneous inductive-recursive definition which is implicit in Martin-Lof's intuitionistic type theory. We extend previously given schematic formulations of inductive definitions in type theory to encompass a general notion of simultaneous induction-recursion. This enables us to give a unified treatment of several interesting constructions including various universe constructions by Palmgren, Griffor, Rathjen, and Setzer and a constructive version of Aczel's Frege structures. Consistency of a restricted version of the extension is shown by constructing a realisability model in the style of Allen.