B-systems and C-systems are equivalent

Benedikt Ahrens; Jacopo Emmenegger; Paige Randall North; Egbert Rijke

doi:10.1017/jsl.2023.41

B-systems and C-systems are equivalent

Benedikt Ahrens^*, Jacopo Emmenegger, Paige Randall North, Egbert Rijke

^*Corresponding author for this work

Computer Science

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

55 Downloads (Pure)

Abstract

C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky’s construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky.

Original language	English
Journal	Journal of Symbolic Logic
Early online date	29 Jun 2023
DOIs	https://doi.org/10.1017/jsl.2023.41
Publication status	E-pub ahead of print - 29 Jun 2023

Bibliographical note

Funding:
This work was partially funded by EPSRC under agreement number EP/T000252/1, and by the K&A Wallenberg Foundation under agreement number KAW 2019.0494. This material is based upon work supported by the Air Force Office of Scientific Research under award numbers FA9550-21-1-0334 and FA9550-21-1-0024.

Keywords

contextual categories
semantics of type theory
Martin-Löf type theory
B-systems
C-systems

Access to Document

10.1017/jsl.2023.41Licence: Creative Commons: Attribution (CC BY)

AhrensB2023BSystemsFinal published version, 193 KBLicence: Creative Commons: Attribution (CC BY)

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

Cite this

@article{6295ae7808cc435ebc41b128bbd3aee3,

title = "B-systems and C-systems are equivalent",

abstract = "C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky{\textquoteright}s construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky.",

keywords = "contextual categories, semantics of type theory, Martin-L{\"o}f type theory, B-systems, C-systems",

author = "Benedikt Ahrens and Jacopo Emmenegger and North, {Paige Randall} and Egbert Rijke",

note = "Funding: This work was partially funded by EPSRC under agreement number EP/T000252/1, and by the K&A Wallenberg Foundation under agreement number KAW 2019.0494. This material is based upon work supported by the Air Force Office of Scientific Research under award numbers FA9550-21-1-0334 and FA9550-21-1-0024.",

year = "2023",

month = jun,

day = "29",

doi = "10.1017/jsl.2023.41",

language = "English",

journal = "Journal of Symbolic Logic",

issn = "0022-4812",

publisher = "Association for Symbolic Logic",

}

TY - JOUR

T1 - B-systems and C-systems are equivalent

AU - Ahrens, Benedikt

AU - Emmenegger, Jacopo

AU - North, Paige Randall

AU - Rijke, Egbert

N1 - Funding: This work was partially funded by EPSRC under agreement number EP/T000252/1, and by the K&A Wallenberg Foundation under agreement number KAW 2019.0494. This material is based upon work supported by the Air Force Office of Scientific Research under award numbers FA9550-21-1-0334 and FA9550-21-1-0024.

PY - 2023/6/29

Y1 - 2023/6/29

N2 - C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky’s construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky.

AB - C-systems were defined by Cartmell as models of generalized algebraic theories. B-systems were defined by Voevodsky in his quest to formulate and prove an initiality conjecture for type theories. They play a crucial role in Voevodsky’s construction of a syntactic C-system from a term monad. In this work, we construct an equivalence between the category of C-systems and the category of B-systems, thus proving a conjecture by Voevodsky.

KW - contextual categories

KW - semantics of type theory

KW - Martin-Löf type theory

KW - B-systems

KW - C-systems

U2 - 10.1017/jsl.2023.41

DO - 10.1017/jsl.2023.41

M3 - Article

SN - 0022-4812

JO - Journal of Symbolic Logic

JF - Journal of Symbolic Logic

ER -

B-systems and C-systems are equivalent

Abstract

Bibliographical note

Keywords

Access to Document

Fingerprint

Projects

A theory of type theories

Cite this