B-systems and C-systems are equivalent

Title

B-systems and C-systems are equivalent

 Author

Ahrens, B.P. (TU Delft Programming Languages; University of Birmingham)
Emmenegger, Jacopo (University of Genova)
North, Paige Randall (Universiteit Utrecht)
Rijke, Egbert (University of Ljubljana)

Date

2023

 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.


 To reference this document use:

http://resolver.tudelft.nl/uuid:28efc53e-64a8-43df-a84d-fa5b27541eb8

 DOI

https://doi.org/10.1017/jsl.2023.41

 ISSN

0022-4812

 Source

The Journal of Symbolic Logic

 Part of collection

Institutional Repository

 Document type

journal article

 Rights

© 2023 B.P. Ahrens, Jacopo Emmenegger, Paige Randall North, Egbert Rijke
Files
PDF b_systems_and_c_systems_a ... valent.pdf 272.96 KB
Close viewer