Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2605.15126 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909053845766144 |
|---|---|
| author | Coquand, Thierry Höfer, Jonas Sattler, Christian |
| author_facet | Coquand, Thierry Höfer, Jonas Sattler, Christian |
| contents | There have recently been several developments in synthetic mathematics using extensions of dependent type theory with univalence and higher inductive types: simplicial homotopy type theory, synthetic algebraic geometry and synthetic Stone duality. We provide a foundation of higher sheaf models of type theory in a constructive metatheory and, in particular, build constructive models of these formal systems. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_15126 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Constructive higher sheaf models with applications to synthetic mathematics Coquand, Thierry Höfer, Jonas Sattler, Christian Logic in Computer Science Logic There have recently been several developments in synthetic mathematics using extensions of dependent type theory with univalence and higher inductive types: simplicial homotopy type theory, synthetic algebraic geometry and synthetic Stone duality. We provide a foundation of higher sheaf models of type theory in a constructive metatheory and, in particular, build constructive models of these formal systems. |
| title | Constructive higher sheaf models with applications to synthetic mathematics |
| topic | Logic in Computer Science Logic |
| url | https://arxiv.org/abs/2605.15126 |