Constructive higher sheaf models with applications to synthetic mathematics
Fuente:
arXiv
Guardado en:
| Autores principales: | , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _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 |