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

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

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
Pages (from-to)	1513-1521
Journal	Journal of Symbolic Logic
Volume	89
Issue number	4
Early online date	2023
DOIs	https://doi.org/10.1017/jsl.2023.41
Publication status	Published - Dec 2024

Bibliographical note

Publisher Copyright:
© 2023 Cambridge University Press. All rights reserved.

Keywords

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

Access to Document

10.1017/jsl.2023.41Licence: CC BY

b-systems-and-c-systems-are-equivalentFinal published version, 193 KBLicence: CC BY

Cite this

@article{214102a825ba421ca97b0f32d9bdfc9e,

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'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 = "ontextual categories, Martin-L{\"o}f type theory, semantics of type theory, B-systems, C-systems",

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

year = "2024",

month = dec,

doi = "10.1017/jsl.2023.41",

language = "English",

volume = "89",

pages = "1513--1521",

journal = "Journal of Symbolic Logic",

issn = "0022-4812",

publisher = "Cambridge University Press",

number = "4",

}

TY - JOUR

T1 - B-systems and C-systems are equivalent

AU - Ahrens, Benedikt

AU - Emmenegger, Jacopo

AU - North, Paige Randall

AU - Rijke, Egbert

PY - 2024/12

Y1 - 2024/12

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 - ontextual categories

KW - Martin-Löf type theory

KW - semantics of type theory

KW - B-systems

KW - C-systems

UR - https://www.scopus.com/pages/publications/85164333395

U2 - 10.1017/jsl.2023.41

DO - 10.1017/jsl.2023.41

M3 - Article

SN - 0022-4812

VL - 89

SP - 1513

EP - 1521

JO - Journal of Symbolic Logic

JF - Journal of Symbolic Logic

IS - 4

ER -

B-systems and C-systems are equivalent

Abstract

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this