Constructive higher sheaf models with applications to synthetic mathematics
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _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 |