Projects per year
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 language | English |
---|---|
Journal | Mathematical Structures in Computer Science |
Early online date | 17 Oct 2023 |
DOIs | |
Publication status | E-pub ahead of print - 17 Oct 2023 |
Bibliographical note
Acknowledgements:We gratefully acknowledge the work by the Coq development team in providing the Coq proof assistant and surrounding infrastructure, as well as their support in keeping UniMath compatible with Coq. We are very grateful to Dan Licata and Bob Harper for their help in understanding their interpretation and how it relates to our framework. We thank the anonymous referees of the short version, and of the present long version, as well as editor Richard Garner, for their insightful comments and helpful advice. This work was partially funded by EPSRC under agreement number EP/T000252/1. This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0334. This research was supported by the NWO project “The Power of Equality” OCENW.M20.380, which is financed by the Dutch Research Council (NWO).
Keywords
- Directed type theory
- dependent types
- comprehension bicategory
- computer-checked proof
Fingerprint
Dive into the research topics of 'Bicategorical type theory: semantics and syntax'. Together they form a unique fingerprint.Projects
- 1 Finished
-
A theory of type theories
Ahrens, B. (Principal Investigator)
Engineering & Physical Science Research Council
1/03/20 → 31/08/22
Project: Research Councils