C-systems were defined by Cartmell as the algebraic structures that correspond exactly to generalised 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. We construct this equivalence as the restriction of an equivalence between more general structures, called CE-systems and E-systems, respectively. To this end, we identify C-systems and B-systems as "stratified" CE-systems and E-systems, respectively; that is, systems whose contexts are built iteratively via context extension, starting from the empty context.

@article{paperbot3447,
  title = {Algebraic Presentations of Type Dependency},
  author = {Benedikt Ahrens and Jacopo Emmenegger and Paige Randall North and Egbert Rijke},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 21, Issue 1},
  year = {2025},
  doi = {10.46298/lmcs-21(1:14)2025}
}