Ambrus Kaposi
Constructing quotient inductive-inductive types
Kaposi, Ambrus; Kovac, Andras; Altenkirch, Thorsten
Authors
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 |
Files
Constructing Quotient Inductive-Inductive Types
(395 Kb)
PDF
Publisher Licence URL
https://creativecommons.org/licenses/by/4.0/
You might also like
Monads need not be endofunctors
(2015)
Journal Article
Type theory in type theory using quotient inductive types
(2016)
Presentation / Conference Contribution
Normalisation by evaluation for dependent types
(2016)
Presentation / Conference Contribution
Notions of anonymous existence in Martin-Löf type theory
(2017)
Journal Article
Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type
(2017)
Presentation / Conference Contribution
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: discovery-access-systems@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search