BLC 2010

Extensions of inductive definition: indexed inductive, inductive-recursive and inductive-inductive definitions
Anton Setzer
We investigate the concept of inductive definitions in the context of Martin-Lof Type Theory. We will see that already there some generalisations take place, namely that later arguments can depend on previous ones. Then we develop the concepts of indexed inductive definitions where we will meet two different kinds of indexed inductive definitions, restricted ones and generalised ones. The intensional equality type is the key example of a generalised one. Then we look at inductive recursive definitions. We then develop the new concept of inductive inductive definitions (joint work with Frederik Forsberg), which is sometimes mixed up with inductive-recursive definitions, and which can be used to formalise the syntax of type theory inside type theory. Finally we look at fixed point constructions which don't admit the notion of a least fixed point, such as the Mahlo universe and the Pi-3-reflecting universe.