{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:26Z","timestamp":1753894406979,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"accepted":{"date-parts":[[2025,2,6]]},"abstract":"<jats:p>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 &amp;quot;stratified&amp;quot; CE-systems and E-systems, respectively; that is, systems whose contexts are built iteratively via context extension, starting from the empty context.<\/jats:p>","DOI":"10.46298\/lmcs-21(1:14)2025","type":"journal-article","created":{"date-parts":[[2025,2,6]],"date-time":"2025-02-06T09:40:07Z","timestamp":1738834807000},"source":"Crossref","is-referenced-by-count":0,"title":["Algebraic Presentations of Type Dependency"],"prefix":"10.46298","volume":"Volume 21, Issue 1","author":[{"given":"Benedikt","family":"Ahrens","sequence":"first","affiliation":[]},{"given":"Jacopo","family":"Emmenegger","sequence":"additional","affiliation":[]},{"given":"Paige Randall","family":"North","sequence":"additional","affiliation":[]},{"given":"Egbert","family":"Rijke","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2025,2,6]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/15199\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/15199\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,6]],"date-time":"2025-02-06T09:40:08Z","timestamp":1738834808000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/10075"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,6]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-21(1:14)2025","relation":{"has-preprint":[{"id-type":"arxiv","id":"2111.09948v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2111.09948v2","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2111.09948","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2111.09948","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2025,2,6]]},"article-number":"10075"}}