Paper: Constructive Higher Sheaf Models with Applications to Synthetic Mathematics (at LICS 2026)

Authors: Thierry Coquand Jonas Höfer Christian Sattler

Open access: https://doi.org/10.4230/LIPIcs.LICS.2026.31

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.

BibTeX

  @InProceedings{CoquandHoferSattler-ConstructiveHigherS,
    author = 	 {Thierry Coquand and Jonas Höfer and Christian Sattler},
    title = 	 {Constructive Higher Sheaf Models with Applications to Synthetic Mathematics},
    booktitle =  {Proceedings of the Forty-First Annual Symposium on Logic in Computer Science (LICS 2026)},
    year =	 {2026},
    month =	 {July}, 
    pages =      {31:1--31:26},
    location =   {Lisbon, Portugal}, 
    publisher =	 {Schloss Dagstuhl -- Leibniz-Zentrum für Informatik},
    doi =        {10.4230/LIPIcs.LICS.2026.31}
  }