A categorical semantics for inductive-inductive definitions

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 → 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