Name
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.
|
Year | DOI | Venue |
|---|---|---|
2019 | 10.1145/3290315 | Proceedings of the ACM on Programming Languages |
Keywords | Field | DocType |
category with families,generalised algebraic theory,higher inductive types,homotopy type theory,inductive-inductive types,logical relations,quotient inductive types | Uniqueness,Algebra,Computer science,Quotient,sort,Type theory,Theoretical computer science,Mathematical proof,Homotopy type theory,Finitary,Syntax | Journal |
Volume | Issue | ISSN |
3 | POPL | 2475-1421 |
Citations | PageRank | References |
1 | 0.37 | 13 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ambrus Kaposi | 1 | 16 | 4.29 |
| András Bálint Kovács | 2 | 2 | 1.74 |
| Thorsten Altenkirch | 3 | 668 | 56.85 |