TY - CHAP
T1 - Semantics for two-dimensional type theory
AU - Ahrens, Benedikt
AU - North, Paige Randall
AU - Van Der Weide, Niels
PY - 2022/2
Y1 - 2022/2
N2 - 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 frst step towards a theory of syntax and semantics for higher-dimensional directed type theory.
AB - 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 frst step towards a theory of syntax and semantics for higher-dimensional directed type theory.
KW - Comprehension bicategory
KW - Computer-checked proof
KW - Dependent types
KW - Directed type theory
UR - https://www.mendeley.com/catalogue/2a935339-9322-3c94-8017-73ce19ea0f24/
U2 - 10.1145/3531130.3533334
DO - 10.1145/3531130.3533334
M3 - Chapter
SN - 9781450393515
T3 - Proceedings - Symposium on Logic in Computer Science
BT - LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science
ER -