Constructive higher sheaf models with applications to synthetic mathematics
Logic in Computer Science
2026-05-19 v2 Logic
Abstract
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.
Keywords
Cite
@article{arxiv.2605.15126,
title = {Constructive higher sheaf models with applications to synthetic mathematics},
author = {Thierry Coquand and Jonas Höfer and Christian Sattler},
journal= {arXiv preprint arXiv:2605.15126},
year = {2026}
}
Comments
Synchronize with submitted version