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

9 Citations (Scopus)

Abstract

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
Pages70-84
Number of pages15
DOIs
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 Sep 2011

Publication series

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

Conference

Conference4th Conference on Algebra and Coalgebra in Computer Science, CALCO 2011
CountryUnited Kingdom
CityWinchester
Period30/08/112/09/11

Keywords

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

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

  • Cite this

    Altenkirch, T., Morris, P., Nordvall Forsberg, F., & Setzer, A. (2011). A categorical semantics for inductive-inductive definitions. In A. Corradini, B. Klin, & C. Cîrstea (Eds.), Algebra and Coalgebra in Computer Science: 4th International Conference, CALCO 2011, Winchester, UK, August 30 – September 2, 2011. Proceedings (pp. 70-84). (Lecture Notes in Computer Science; Vol. 6859).. https://doi.org/10.1007/978-3-642-22944-2_6