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. Proceedings of the ACM on Programming Languages, 3(POPL), 1-24. https://doi.org/10.1145/3290315

• Journal Article Type: Article
• 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
• Journal: Proceedings of the ACM on Programming Languages
• Electronic ISSN: 2475-1421
• Publisher: Association for Computing Machinery (ACM)
• Peer Reviewed: Peer Reviewed
• Volume: 3
• Issue: POPL
• Article Number: 2
• Pages: 1-24
• 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