{"id":"arxiv/2605.15126","url":"https://arxiv.org/abs/2605.15126","tags":["cs.LO","math.LO"],"score":0,"title":"Constructive higher sheaf models with applications to synthetic mathematics","domain":"cs.LO","source":"arxiv","authors":["Thierry Coquand","Jonas Höfer","Christian Sattler"],"reviews":0,"subject":"cs.LO","summary":"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.","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-05-14","reactions":{}}