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.