Bicategorical type theory: Semantics and syntax

Benedikt Ahrens, Paige Randall North, Niels Van Der Weide*

*Corresponding author for this work

Research output: Contribution to journalArticleScientificpeer-review

1 Citation (Scopus)
50 Downloads (Pure)

Abstract

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.

Original languageEnglish
Pages (from-to)868-912
Number of pages45
JournalMathematical Structures in Computer Science
Volume33
Issue number10
DOIs
Publication statusPublished - 2023

Keywords

  • comprehension bicategory
  • computer-checked proof
  • dependent types
  • Directed type theory

Fingerprint

Dive into the research topics of 'Bicategorical type theory: Semantics and syntax'. Together they form a unique fingerprint.

Cite this