Bicategorical type theory: semantics and syntax

Benedikt Ahrens; Paige Randall North; Niels van der Weide

doi:10.1017/S0960129523000312

Bicategorical type theory: semantics and syntax

Benedikt Ahrens, Paige Randall North, Niels van der Weide^*

^*Corresponding author for this work

Computer Science

Research output: Contribution to journal › Article › peer-review

4 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 language	English
Journal	Mathematical Structures in Computer Science
Early online date	17 Oct 2023
DOIs	https://doi.org/10.1017/S0960129523000312
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

Access to Document

10.1017/S0960129523000312Licence: Creative Commons: Attribution (CC BY)

AhrensB2023BicategoricalFinal published version, 581 KBLicence: Creative Commons: Attribution (CC BY)

A theory of type theories
Ahrens, B.
Engineering & Physical Science Research Council
1/03/20 → 31/08/22
Project: Research Councils

Cite this

@article{59cd35de21d5436fa0907a807a16046e,

title = "Bicategorical type theory: semantics and syntax",

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.",

keywords = "Directed type theory, dependent types, comprehension bicategory, computer-checked proof",

author = "Benedikt Ahrens and North, {Paige Randall} and {van der Weide}, Niels",

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). ",

year = "2023",

month = oct,

day = "17",

doi = "10.1017/S0960129523000312",

language = "English",

journal = "Mathematical Structures in Computer Science",

issn = "0960-1295",

publisher = "Cambridge University Press",

}

TY - JOUR

T1 - Bicategorical type theory

T2 - semantics and syntax

AU - Ahrens, Benedikt

AU - North, Paige Randall

AU - van der Weide, Niels

N1 - 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).

PY - 2023/10/17

Y1 - 2023/10/17

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 - Directed type theory

KW - dependent types

KW - comprehension bicategory

KW - computer-checked proof

U2 - 10.1017/S0960129523000312

DO - 10.1017/S0960129523000312

M3 - Article

SN - 0960-1295

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

ER -

Bicategorical type theory: semantics and syntax

Abstract

Bibliographical note

Keywords

Access to Document

Fingerprint

Projects

A theory of type theories

Cite this