Skip to main content

Research Repository

Advanced Search

Constructing quotient inductive-inductive types

Kaposi, Ambrus; Kovac, Andras; Altenkirch, Thorsten

Constructing quotient inductive-inductive types Thumbnail


Ambrus Kaposi

Andras Kovac


Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In addition, equality constructors are also allowed. We work in a setting with uniqueness of identity proofs, hence we use the term QIIT instead of higher inductive-inductive type. An example of a QIIT is the well-typed (intrinsic) syntax of type theory quotiented by conversion. In this paper first we specify finitary QIITs using a domain-specific type theory which we call the theory of signatures. The syntax of the theory of signatures is given by a QIIT as well. Then, using this syntax we show that all specified QIITs exist and they have a dependent elimination principle. We also show that algebras of a signature form a category with families (CwF) and use the internal language of this CwF to show that dependent elimination is equivalent to initiality.

Conference Name 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019)
Conference Location Cascais/Lisbon, Portugal
Start Date Jan 16, 2019
End Date Jan 18, 2019
Acceptance Date Oct 16, 2018
Online Publication Date Jan 16, 2019
Publication Date Jan 2, 2019
Deposit Date Nov 29, 2018
Publicly Available Date Nov 30, 2018
Publisher Association for Computing Machinery (ACM)
Volume 3
Pages 1-24
Series ISSN 2475-1421
Book Title Proceedings of the ACM on Programming Languages archive Volume 3 Issue POPL, January 2019
Chapter Number 2
Public URL
Publisher URL


You might also like

Downloadable Citations