Fredrik Nordvall-Forsberg: Inductive-inductive definitions in Intuitionistic Type Theory

Martin-Löf's dependent type theory can be seen both as a foundational framework for constructive mathematics, and as a functional programming language with a very rich type system. Of course, we want this language to have a rich notion of data structure as well. I will describe one class of such data types, where a type A is formed inductively, simultaneously with a second type B : A → Type which depend on it. Since both types are formed inductively, we call such definitions inductive-inductive definitions. Examples of inductive-inductive definitions — e. g. sorted lists, Conway's Surreal numbers and the syntax of dependent type theory — will be given, and their meta-theory discussed.