Synthetic 1-Categories in Directed Type Theory
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914104217698304 |
|---|---|
| author | Altenkirch, Thorsten Neumann, Jacob |
| author_facet | Altenkirch, Thorsten Neumann, Jacob |
| contents | The field of directed type theory seeks to design type theories capable of reasoning synthetically about (higher) categories, by generalizing the symmetric identity types of Martin-Löf Type Theory to asymmetric hom-types. We articulate the directed type theory of the category model, with appropriate modalities for keeping track of variances and a powerful directed-J rule capable of proving results about arbitrary terms of hom-types; we put this rule to use in making several constructions in synthetic 1-category theory. Because this theory is expressed entirely in terms of generalized algebraic theories, we know automatically that this directed type theory admits a syntax model and is the first step towards directed higher observational type theory. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_19520 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Synthetic 1-Categories in Directed Type Theory Altenkirch, Thorsten Neumann, Jacob Category Theory Logic in Computer Science The field of directed type theory seeks to design type theories capable of reasoning synthetically about (higher) categories, by generalizing the symmetric identity types of Martin-Löf Type Theory to asymmetric hom-types. We articulate the directed type theory of the category model, with appropriate modalities for keeping track of variances and a powerful directed-J rule capable of proving results about arbitrary terms of hom-types; we put this rule to use in making several constructions in synthetic 1-category theory. Because this theory is expressed entirely in terms of generalized algebraic theories, we know automatically that this directed type theory admits a syntax model and is the first step towards directed higher observational type theory. |
| title | Synthetic 1-Categories in Directed Type Theory |
| topic | Category Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2410.19520 |