Inductive-inductive definitions

The principle of inductive-inductive definitions is a principle for defining data types in Martin-Löf Type Theory. It allows the definition of a set A, simultaneously defined with a family B ∶ A → Set indexed over A. Such forms of definitions have been used by several authors in order to for example define the syntax of Type Theory in Type Theory itself. This thesis gives a theoretical justification for their use. We start by giving a finite axiomatisation of a type theory with inductive-inductive definitions in the style of Dybjer and Setzer’s axiomatisation of inductive-recursive definitions. We then give a categorical characterisation of inductive-inductive definitions as initial objects in a certain category. This is presented using a general framework for elimination rules based on the concept of a Category with Families. To show consistency of inductive-inductive definitions, a set-theoretical model is constructed. Furthermore, we give a translation of our theory with a simplified form of the elimination rule into the already existing theory of indexed inductive definitions. This translation does notseem possible for the general elimination rule. Extensions to the theory are investigated, such as a combined theory of inductive-inductive-recursive definitions, more general forms of indexing and arbitrarily high (finite) towers of inductive-inductive definitions.Even so, not all uses of inductive-inductive definitions in the literature (in particular the syntax of Type Theory) are covered by the theories presented. Finally, two larger, novel case studies of the use of inductive-inductive definitions are presented: Conway’s Surreal numbers and a formalisation of positive inductive-recursive definitions.