License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2019.6
URN: urn:nbn:de:0030-drops-130707
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13070/
Go to the corresponding LIPIcs Volume Portal

Kaposi, Ambrus ; Kovács, András ; Lafont, Ambroise

For Finitary Induction-Induction, Induction Is Enough

pdf-format:
LIPIcs-TYPES-2019-6.pdf (0.6 MB)

Abstract

Inductive-inductive types (IITs) are a generalisation of inductive types in type theory. They allow the mutual definition of types with multiple sorts where later sorts can be indexed by previous ones. An example is the Chapman-style syntax of type theory with conversion relations for each sort where e.g. the sort of types is indexed by contexts. In this paper we show that if a model of extensional type theory (ETT) supports indexed W-types, then it supports finitely branching IITs. We use a small internal type theory called the theory of signatures to specify IITs. We show that if a model of ETT supports the syntax for the theory of signatures, then it supports all IITs. We construct this syntax from indexed W-types using preterms and typing relations and prove its initiality following Streicher. The construction of the syntax and its initiality proof were formalised in Agda.

BibTeX - Entry

@InProceedings{kaposi_et_al:LIPIcs:2020:13070,
  author =	{Ambrus Kaposi and Andr{\'a}s Kov{\'a}cs and Ambroise Lafont},
  title =	{{For Finitary Induction-Induction, Induction Is Enough}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{6:1--6:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Marc Bezem and Assia Mahboubi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13070},
  URN =		{urn:nbn:de:0030-drops-130707},
  doi =		{10.4230/LIPIcs.TYPES.2019.6},
  annote =	{Keywords: type theory, inductive types, inductive-inductive types}
}

Keywords: type theory, inductive types, inductive-inductive types
Collection: 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Issue Date: 2020
Date of publication: 24.09.2020
Supplementary Material: The contents of Section 4 were formalised in Agda, the formalisation is available at https://github.com/amblafont/UniversalII.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI