Constructing quotient inductive-inductive types

Kaposi, Ambrus; Kovac, Andras; Altenkirch, Thorsten

Abstract

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.

Citation

Kaposi, A., Kovac, A., & Altenkirch, T. (2019). Constructing quotient inductive-inductive types. In Proceedings of the ACM on Programming Languages archive Volume 3 Issue POPL, January 2019 (1-24). https://doi.org/10.1145/3290315

• Presentation Conference Type: Conference Paper (Published)
• Conference Name: 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019)
• 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
• DOI: https://doi.org/10.1145/3290315
• Public URL: https://nottingham-repository.worktribe.com/output/1314154
• Publisher URL: https://dl.acm.org/citation.cfm?doid=3302515.3290315
• Contract Date: Nov 29, 2018