A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911484255141888 |
|---|---|
| author | Bezem, Marc Coquand, Thierry Dybjer, Peter Escardó, Martín |
| author_facet | Bezem, Marc Coquand, Thierry Dybjer, Peter Escardó, Martín |
| contents | We present generalized algebraic theories corresponding to slightly modified versions of two of the type theories in our paper Type Theory with Explicit Universe Polymorphism. We first present a generalized algebraic theory for categories with families with extra structure corresponding to Martin-Lof type theory with an external tower of universes. We then present a generalized algebraic theory for level-indexed categories with families with extra structure corresponding to Martin-Lof type theory with explicit universe polymorphism: a theory with universe level judgments, internally indexed universes, and level-indexed products. In this way we get abstract characterizations of the two theories as initial models of their respective generalized algebraic theories. We thus abstract from details of the grammar and inference rules of the type theories and highlight their high-level structure. More broadly, the present work can be viewed as a case study of a uniform approach to categorical logic based on generalized algebraic theories and categories with families. We also discuss the relevance to Voevodsky's initiality conjecture project. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_04010 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism Bezem, Marc Coquand, Thierry Dybjer, Peter Escardó, Martín Logic in Computer Science We present generalized algebraic theories corresponding to slightly modified versions of two of the type theories in our paper Type Theory with Explicit Universe Polymorphism. We first present a generalized algebraic theory for categories with families with extra structure corresponding to Martin-Lof type theory with an external tower of universes. We then present a generalized algebraic theory for level-indexed categories with families with extra structure corresponding to Martin-Lof type theory with explicit universe polymorphism: a theory with universe level judgments, internally indexed universes, and level-indexed products. In this way we get abstract characterizations of the two theories as initial models of their respective generalized algebraic theories. We thus abstract from details of the grammar and inference rules of the type theories and highlight their high-level structure. More broadly, the present work can be viewed as a case study of a uniform approach to categorical logic based on generalized algebraic theories and categories with families. We also discuss the relevance to Voevodsky's initiality conjecture project. |
| title | A Generalized Algebraic Theory for Type Theory with Explicit Universe Polymorphism |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2603.04010 |