### 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 language | English |
---|---|

Title of host publication | Algebra and Coalgebra in Computer Science |

Subtitle of host publication | 4th International Conference, CALCO 2011, Winchester, UK, August 30 – September 2, 2011. Proceedings |

Editors | Andrea Corradini, Bartek Klin, Corina Cîrstea |

Place of Publication | Berlin |

Pages | 70-84 |

Number of pages | 15 |

DOIs | |

Publication status | Published - 19 Aug 2011 |

Event | 4th Conference on Algebra and Coalgebra in Computer Science, CALCO 2011 - University of Winchester, Winchester, United Kingdom Duration: 30 Aug 2011 → 2 Sep 2011 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Berlin Heidelberg |

Volume | 6859 |

ISSN (Print) | 0302-9743 |

### Conference

Conference | 4th Conference on Algebra and Coalgebra in Computer Science, CALCO 2011 |
---|---|

Country | United Kingdom |

City | Winchester |

Period | 30/08/11 → 2/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