Abstract
We propose a general notion of model for two-dimensional type theory, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; they include interpretations of directed type theory previously studied in the literature. From comprehension bicategories, we extract a core syntax, that is, judgment forms and structural inference rules, for a two-dimensional type theory. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library. This work is the first step towards a theory of syntax and semantics for higher-dimensional directed type theory.
Original language | English |
---|---|
Title of host publication | Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022 |
Place of Publication | New York |
Publisher | ACM |
Number of pages | 14 |
ISBN (Print) | 978-1-4503-9351-5 |
DOIs | |
Publication status | Published - 2022 |
Event | 37th Annual ACM/IEEE Symposium on Logic in Computer Science - Haifa, Israel Duration: 2 Aug 2022 → 5 Aug 2022 Conference number: 27 |
Conference
Conference | 37th Annual ACM/IEEE Symposium on Logic in Computer Science |
---|---|
Abbreviated title | LICS ’22 |
Country/Territory | Israel |
City | Haifa |
Period | 2/08/22 → 5/08/22 |
Keywords
- directed type theory
- dependent types
- comprehension bicategory,
- computer-checked proof