Algebraic Presentations of Type Dependency

TL;DR

This paper establishes an equivalence between C-systems and B-systems, key algebraic structures in type theory, by relating them through more general CE- and E-systems, confirming a conjecture by Voevodsky.

Contribution

It proves Voevodsky's conjecture by constructing an equivalence between C-systems and B-systems via stratified CE- and E-systems, unifying their algebraic frameworks.

Findings

Proves the equivalence of C-systems and B-systems.

Identifies C- and B-systems as stratified CE- and E-systems.

Confirms a conjecture by Voevodsky.

Abstract

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.