B-systems and C-systems are equivalent

Journal article (2023)

Authors

B.P. Ahrens Programming Languages - EEMCS , University of Birmingham
Jacopo Emmenegger University of Genova
Paige Randall North Universiteit Utrecht
Egbert Rijke University of Ljubljana
Research Group
Programming Languages (EEMCS) (TU Delft)
Copyright: © 2023 B.P. Ahrens, Jacopo Emmenegger, Paige Randall North, Egbert Rijke
DOI: https://doi.org/10.1017/jsl.2023.41
More Info
expand_more

Published Date

2023

Language

English

Faculty

Electrical Engineering, Mathematics and Computer Science

Department

Software Technology

Research Group

Programming Languages

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.