Benedikt Ahrens ; Jacopo Emmenegger ; Paige Randall North ; Egbert Rijke - Algebraic Presentations of Type Dependency

lmcs:10075 - Logical Methods in Computer Science, February 6, 2025, Volume 21, Issue 1 - https://doi.org/10.46298/lmcs-21(1:14)2025
Algebraic Presentations of Type DependencyArticle

Authors: Benedikt Ahrens ; Jacopo Emmenegger ; Paige Randall North ; Egbert Rijke

    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.


    Volume: Volume 21, Issue 1
    Published on: February 6, 2025
    Accepted on: December 17, 2024
    Submitted on: September 22, 2022
    Keywords: Mathematics - Category Theory

    Consultation statistics

    This page has been seen 417 times.
    This article's PDF has been downloaded 257 times.