Constructing quotient inductive-inductive types
| Autor: | András Kovács, Thorsten Altenkirch, Ambrus Kaposi |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Syntax (programming languages)
020207 software engineering 0102 computer and information sciences 02 engineering and technology Type (model theory) Term (logic) Mathematical proof 01 natural sciences Algebra Type theory 010201 computation theory & mathematics 0202 electrical engineering electronic engineering information engineering Homotopy type theory Finitary Safety Risk Reliability and Quality Software Quotient Mathematics |
| Zdroj: | Proceedings of the ACM on Programming Languages. 3:1-24 |
| ISSN: | 2475-1421 |
| DOI: | 10.1145/3290315 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|