Algebraic Presentations of Type Dependency
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2021
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915144857026560 |
|---|---|
| author | Ahrens, Benedikt Emmenegger, Jacopo North, Paige Randall Rijke, Egbert |
| author_facet | Ahrens, Benedikt Emmenegger, Jacopo North, Paige Randall Rijke, Egbert |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2111_09948 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Algebraic Presentations of Type Dependency Ahrens, Benedikt Emmenegger, Jacopo North, Paige Randall Rijke, Egbert Category Theory 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. |
| title | Algebraic Presentations of Type Dependency |
| topic | Category Theory |
| url | https://arxiv.org/abs/2111.09948 |