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.
Slides (prez.pdf) | 90KiB |
Fri 18 JanDisplayed time zone: Belfast change
10:35 - 12:03 | |||
10:35 22mTalk | Higher Inductive Types in Cubical Computational Type Theory Research Papers Link to publication DOI Pre-print Media Attached File Attached | ||
10:57 22mTalk | Constructing Quotient Inductive-Inductive Types Research Papers Thorsten Altenkirch University of Nottingham, Ambrus Kaposi University of Nottingham, András Kovács Eötvös Loránd University Link to publication DOI Media Attached File Attached | ||
11:19 22mTalk | Definitional Proof-Irrelevance without K Research Papers Gaetan Gilbert , Jesper Cockx Chalmers | University of Gothenburg, Matthieu Sozeau Inria, Nicolas Tabareau Inria Link to publication DOI Media Attached File Attached | ||
11:41 22mTalk | Bisimulation as Path Type for Guarded Recursive Types Research Papers Link to publication DOI Media Attached File Attached |