@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",

}