[[!redirects Inductive Inductive Type]] ## Idea ## Induction-induction is a principle for mutually defining data types $A : Set$ and $B: A \to Set$. Both $A$ and $B$ are defined inductively, and the constructors for $A$ can refer to $B$ and vice versa. In addition, the constructor for $B$ can refer to the constructor for $A$. Induction-induction occurs in a natural way when formalising dependent type theory in type theory. ## Results ## Inductive-inductive types are related to [[inductive-recursive type|inductive-recursive types]]. Importantly, inductive-inductive types can be reduced to indexed inductive types. The consistency of the framework used for the elimination (the theorem prover Agda) is not so clear, as it allows the definition of a universe containing a code for itself. There is an axiomatisation of the new principle in such a way that the resulting type theory is consistent, as proved by constructing a set-theoretic model; see [ForsbergSetzer](#IID). ## Higher inductive inductive types ## These are described in the book. ## References ## Fredrik Nordvall Forsberg and Anton Setzer, _A finite axiomatisation of inductive-inductive definitions_ [PDF](http://cs.swan.ac.uk/~csfnf/papers/indind_finite.pdf) {#IID} Fredrik Nordvall Forsberg and Anton Setzer, _Inductive-Inductive Definitions_, Computer Science Logic, Lecture Notes in Computer Science Volume 6247, 2010, pp 454-468 [Paper](http://link.springer.com/chapter/10.1007%2F978-3-642-15205-4_35). Fredrik Nordvall Forsberg, _Inductive-inductive definitions_, PhD thesis Swansea University, 2013. [PDF](http://cs.swan.ac.uk/~csfnf/thesis/thesis.pdf)