Skip to Main content Skip to Navigation
Conference papers

For Finitary Induction-Induction, Induction is Enough

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Nathalie Fontaine Connect in order to contact the contributor
Submitted on : Wednesday, March 2, 2022 - 12:48:57 PM
Last modification on : Friday, August 5, 2022 - 2:54:52 PM
Long-term archiving on: : Tuesday, May 31, 2022 - 6:49:57 PM


Publisher files allowed on an open archive


Distributed under a Creative Commons Attribution 4.0 International License



Ambrus Kaposi, András Kovács, Ambroise Lafont. For Finitary Induction-Induction, Induction is Enough. TYPES 2019: 25th International Conference on Types for Proofs and Programs, Jun 2019, Oslo, Norway. pp.6:1-6:30, ⟨10.4230/LIPIcs.TYPES.2019.6⟩. ⟨hal-03594037⟩



Record views


Files downloads