@inproceedings{0343ab5f655243829ad4e2da96c98b39,
title = "A categorical semantics for inductive-inductive definitions",
abstract = "Induction-induction is a principle for defining data types in Martin-L{\"o}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.",
keywords = "data type, dialgebras, elimination rules, formalisation, initial algebras, type theory",
author = "Thorsten Altenkirch and Peter Morris and {Nordvall Forsberg}, Fredrik and Anton Setzer",
year = "2011",
month = aug,
day = "19",
doi = "10.1007/978-3-642-22944-2_6",
language = "English",
isbn = "9783642229435",
series = "Lecture Notes in Computer Science",
publisher = "Springer Berlin Heidelberg",
pages = "70--84",
editor = "Andrea Corradini and Bartek Klin and Corina C{\^i}rstea",
booktitle = "Algebra and Coalgebra in Computer Science",
note = "4th Conference on Algebra and Coalgebra in Computer Science, CALCO 2011 ; Conference date: 30-08-2011 Through 02-09-2011",
}