A categorical semantics for inductive-inductive definitions

Thorsten Altenkirch, Peter Morris, Fredrik Nordvall Forsberg, Anton Setzer

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

15 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationAlgebra and Coalgebra in Computer Science
Subtitle of host publication4th International Conference, CALCO 2011, Winchester, UK, August 30 – September 2, 2011. Proceedings
EditorsAndrea Corradini, Bartek Klin, Corina Cîrstea
Place of PublicationBerlin
Number of pages15
Publication statusPublished - 19 Aug 2011
Event4th Conference on Algebra and Coalgebra in Computer Science, CALCO 2011 - University of Winchester, Winchester, United Kingdom
Duration: 30 Aug 20112 Sept 2011

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


Conference4th Conference on Algebra and Coalgebra in Computer Science, CALCO 2011
Country/TerritoryUnited Kingdom


  • data type
  • dialgebras
  • elimination rules
  • formalisation
  • initial algebras
  • type theory


Dive into the research topics of 'A categorical semantics for inductive-inductive definitions'. Together they form a unique fingerprint.

Cite this