Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2604.18668 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910149876121600 |
|---|---|
| author | Lossin, Benno |
| author_facet | Lossin, Benno |
| contents | We study $\infty$-categories in the synthetic simplicial type theory developed by Riehl and Shulman. In particular, we define cocartesian fibrations and prove their closure properties using a novel equivalence between LARI adjunctions and initial sections. We formalize our work using the experimental proof assistant rzk and upstream our work to the formalization effort by Riehl et al. In addition to our new work, we also give an introduction to general type theory, homotopy type theory, and the simplicial type theory used by the rest of the thesis. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_18668 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Fibrations in Directed Type Theory Lossin, Benno Category Theory We study $\infty$-categories in the synthetic simplicial type theory developed by Riehl and Shulman. In particular, we define cocartesian fibrations and prove their closure properties using a novel equivalence between LARI adjunctions and initial sections. We formalize our work using the experimental proof assistant rzk and upstream our work to the formalization effort by Riehl et al. In addition to our new work, we also give an introduction to general type theory, homotopy type theory, and the simplicial type theory used by the rest of the thesis. |
| title | Fibrations in Directed Type Theory |
| topic | Category Theory |
| url | https://arxiv.org/abs/2604.18668 |