TY - JOUR
T1 - Bicategorical type theory
T2 - Semantics and syntax
AU - Ahrens, Benedikt
AU - North, Paige Randall
AU - Van Der Weide, Niels
PY - 2023
Y1 - 2023
N2 - We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is naturally interpreted in a class of structured bicategories. We start by developing the semantics, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; we study both specific examples as well as classes of examples constructed from other data. From the notion of comprehension bicategory, we extract the syntax of bicategorical type theory, that is, judgment forms and structural inference rules. 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.
AB - We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is naturally interpreted in a class of structured bicategories. We start by developing the semantics, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; we study both specific examples as well as classes of examples constructed from other data. From the notion of comprehension bicategory, we extract the syntax of bicategorical type theory, that is, judgment forms and structural inference rules. 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.
KW - comprehension bicategory
KW - computer-checked proof
KW - dependent types
KW - Directed type theory
UR - http://www.scopus.com/inward/record.url?scp=85175003705&partnerID=8YFLogxK
U2 - 10.1017/S0960129523000312
DO - 10.1017/S0960129523000312
M3 - Article
AN - SCOPUS:85175003705
SN - 0960-1295
JO - Mathematical Structures in Computer Science
JF - Mathematical Structures in Computer Science
ER -