B-systems and C-systems are equivalent

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

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-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 languageEnglish
JournalJournal of Symbolic Logic
Early online date29 Jun 2023
DOIs
Publication statusE-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

Fingerprint

Dive into the research topics of 'B-systems and C-systems are equivalent'. Together they form a unique fingerprint.

Cite this