Kripke-Joyal forcing for type theory and uniform fibrations
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2021
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914788731256832 |
|---|---|
| author | Awodey, S. Gambino, N. Hazratpour, S. |
| author_facet | Awodey, S. Gambino, N. Hazratpour, S. |
| contents | We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an application, we prove several properties of algebraic weak factorisation systems considered in Homotopy Type Theory. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2110_14576 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Kripke-Joyal forcing for type theory and uniform fibrations Awodey, S. Gambino, N. Hazratpour, S. Logic Category Theory 03G30, 03B38, 18F20, 18N45 We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an application, we prove several properties of algebraic weak factorisation systems considered in Homotopy Type Theory. |
| title | Kripke-Joyal forcing for type theory and uniform fibrations |
| topic | Logic Category Theory 03G30, 03B38, 18F20, 18N45 |
| url | https://arxiv.org/abs/2110.14576 |