Comparing semantic frameworks for dependently-sorted algebraic theories
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866929651116408832 |
|---|---|
| author | Ahrens, Benedikt Lumsdaine, Peter LeFanu North, Paige Randall |
| author_facet | Ahrens, Benedikt Lumsdaine, Peter LeFanu North, Paige Randall |
| contents | Algebraic theories with dependency between sorts form the structural core of Martin-Löf type theory and similar systems. Their denotational semantics are typically studied using categorical techniques; many different categorical structures have been introduced to model them (contextual categories, categories with families, display map categories, etc.) Comparisons of these models are scattered throughout the literature, and a detailed, big-picture analysis of their relationships has been lacking.
We aim to provide a clear and comprehensive overview of the relationships between as many such models as possible. Specifically, we take *comprehension categories* as a unifying language and show how almost all established notions of model embed as sub-2-categories (usually full) of the 2-category of comprehension categories. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2412_19946 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Comparing semantic frameworks for dependently-sorted algebraic theories Ahrens, Benedikt Lumsdaine, Peter LeFanu North, Paige Randall Category Theory Programming Languages Logic 18C50 Categorical semantics of formal languages (primary), 03G30 Categorical logic and topoi, 03B15 Higher-order logic and type theory Algebraic theories with dependency between sorts form the structural core of Martin-Löf type theory and similar systems. Their denotational semantics are typically studied using categorical techniques; many different categorical structures have been introduced to model them (contextual categories, categories with families, display map categories, etc.) Comparisons of these models are scattered throughout the literature, and a detailed, big-picture analysis of their relationships has been lacking. We aim to provide a clear and comprehensive overview of the relationships between as many such models as possible. Specifically, we take *comprehension categories* as a unifying language and show how almost all established notions of model embed as sub-2-categories (usually full) of the 2-category of comprehension categories. |
| title | Comparing semantic frameworks for dependently-sorted algebraic theories |
| topic | Category Theory Programming Languages Logic 18C50 Categorical semantics of formal languages (primary), 03G30 Categorical logic and topoi, 03B15 Higher-order logic and type theory |
| url | https://arxiv.org/abs/2412.19946 |