Summary: Induction-induction is a principle for defining data types in Martin-Löf Type Theory. An inductive-inductive definition consists of a set \(A\), together with an \(A\)-indexed family \(B : A \rightarrow \mathrm{Set}\), where both \(A\) and \(B\) are inductively defined in such a way that the constructors for \(A\) can refer to \(B\) and vice versa. In addition, the constructors for \(B\) can refer to the constructors for \(A\). We extend the usual initial algebra semantics for ordinary inductive data types to the inductive-inductive setting by considering dialgebras instead of ordinary algebras. This gives a new and compact formalisation of inductive-inductive definitions, which we prove is equivalent to the usual formulation with elimination rules.
For the entire collection see [Zbl 1221.68011].