Algebraic Presentations of Dependent Type Theories

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

Research output: Working paperPreprintAcademic


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. 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.
Original languageEnglish
Publication statusPublished - 18 Nov 2021


  • math.CT


Dive into the research topics of 'Algebraic Presentations of Dependent Type Theories'. Together they form a unique fingerprint.

Cite this