Abstract
Induction-induction is a principle for defining data types in Martin Lof Type Theory. An inductive-inductive definition consists of a set A, together with an A-Type Family , 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.
Outline
1. Introduction
1.1. Examples of Inductive-Inductive Definitions
2 Preliminaries
2.1. Inductive-Inductive Definitions as Dialgebras
Def 2.1. Category of Families () Def 2.2. Category of dialgebras () Def 2.3. Inductive-Inductive Definitions Def 2.4. Contexts and Type Example 2.5. Sorted lists