From Semantics to Syntax: A Type Theory for Comprehension Categories
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908658223284224 |
|---|---|
| author | Najmaei, Niyousha van der Weide, Niels Ahrens, Benedikt North, Paige Randall |
| author_facet | Najmaei, Niyousha van der Weide, Niels Ahrens, Benedikt North, Paige Randall |
| contents | Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories.
We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with $Π$-, $Σ$-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_10868 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | From Semantics to Syntax: A Type Theory for Comprehension Categories Najmaei, Niyousha van der Weide, Niels Ahrens, Benedikt North, Paige Randall Programming Languages Logic in Computer Science Category Theory Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories. We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with $Π$-, $Σ$-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations. |
| title | From Semantics to Syntax: A Type Theory for Comprehension Categories |
| topic | Programming Languages Logic in Computer Science Category Theory |
| url | https://arxiv.org/abs/2503.10868 |