Document Open Access Logo

Constructive Higher Sheaf Models with Applications to Synthetic Mathematics

Authors Thierry Coquand , Jonas Höfer , Christian Sattler

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.31.pdf
  • Filesize: 1.37 MB
  • 26 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Constructive mathematics
Keywords
  • Dependent type theory
  • homotopy type theory
  • univalence
  • models of type theory
  • higher sheaves
  • constructive mathematics
  • synthetic mathematics

Metrics

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.

Cite As Get BibTex

Thierry Coquand, Jonas Höfer, and Christian Sattler. Constructive Higher Sheaf Models with Applications to Synthetic Mathematics. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 31:1-31:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.31

Author Details

Thierry Coquand
  • University of Gothenburg, Sweden
  • Chalmers University of Technology, Gothenburg, Sweden
Jonas Höfer
  • University of Gothenburg, Sweden
  • Chalmers University of Technology, Gothenburg, Sweden
Christian Sattler
  • University of Gothenburg, Sweden
  • Chalmers University of Technology, Gothenburg, Sweden

Funding

ForCUTT project, ERC advanced grant 101053291.
  • Sattler, Christian: US Air Force Office of Scientific Research, award number FA9550-24-1-0302.

Acknowledgements

We thank the anonymous referees for the helpful feedback on how to improve the presentation. We thank Evan Cavallo for helpful discussions.

References

  1. Peter Aczel. On Relating Type Theories and Set Theories. In T. Altenkirch, B. Reus, and W. Naraschewski, editors, Types for Proofs and Programs, pages 33-46. Springer, 1998. Google Scholar
  2. Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. Two-level type theory and applications. Mathematical Structures in Computer Science, 33(8):688-743, 2023. URL: https://doi.org/10.1017/S0960129523000130.
  3. M. Artin, A. Grothendieck, and J. L. Verdier. Théorie de Topos et Cohomologie Etale des Schémas. Tome 1: Théorie des topos, Séminaire de Géométrie Algébrique du Bois-Marie 1963-1964 (SGA 4), volume 269 of Lecture Notes in Mathematics. Springer-Verlag, Berlin, 1972. Dirigé par M. Artin, A. Grothendieck, et J. L. Verdier. Avec la collaboration de N. Bourbaki, P. Deligne et B. Saint-Donat. Google Scholar
  4. Steve Awodey. Natural models of homotopy type theory. Mathematical Structures in Computer Science, 28(2):241-286, 2018. URL: https://doi.org/10.1017/S0960129516000268.
  5. Marc Bezem, Thierry Coquand, and Erik Parmann. Non-Constructivity in Kan Simplicial Sets. In Thorsten Altenkirch, editor, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs), pages 92-106, Dagstuhl, Germany, 2015. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.92.
  6. Mark Bickford. Formalizing category theory and presheaf models of type theory in Nuprl, 2018. URL: https://arxiv.org/abs/1806.06114.
  7. Ingo Blechschmidt. A general nullstellensatz for generalized spaces, 2019. URL: https://rawgit.quasicoherent.io/iblech/internal-methods/master/paper-qcoh.pdf.
  8. Kenneth S. Brown. Abstract homotopy theory and generalized sheaf cohomology. Transactions of the American Mathematical Society, 186:419-458, 1973. Google Scholar
  9. John Cartmell. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209-243, 1986. URL: https://doi.org/10.1016/0168-0072(86)90053-9.
  10. Felix Cherubini, Thierry Coquand, Freek Geerligs, and Hugo Moeneclaey. A foundation for synthetic stone duality, 2024. URL: https://arxiv.org/abs/2412.03203.
  11. Felix Cherubini, Thierry Coquand, and Matthias Hutzler. A foundation for synthetic algebraic geometry. Mathematical Structures in Computer Science, 34(9):1008-1053, 2024. URL: https://doi.org/10.1017/S0960129524000239.
  12. Felix Cherubini, Thierry Coquand, Matthias Ritter, and David Wärn. Projective space in synthetic algebraic geometry, 2025. URL: https://arxiv.org/abs/2405.13916.
  13. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1-5:34, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  14. Thierry Coquand. A survey of constructive presheaf models of univalence. ACM SIGLOG News, 5(3):54-65, July 2018. URL: https://doi.org/10.1145/3242953.3242962.
  15. Thierry Coquand, Jonas Höfer, and Christian Sattler. A note about models of synthetic algebraic geometry, 2025. URL: https://arxiv.org/abs/2512.06025.
  16. Thierry Coquand, Jonas Höfer, and Christian Sattler. Constructive higher sheaf models with applications to synthetic mathematics, 2026. URL: https://arxiv.org/abs/2605.15126.
  17. Thierry Coquand, Simon Huber, and Anders Mörtberg. On higher inductive types in cubical type theory. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 255-264. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209197.
  18. Thierry Coquand, Simon Huber, and Christian Sattler. Canonicity and homotopy canonicity for cubical type theory. Logical Methods in Computer Science, 18(1), 2022. URL: https://doi.org/10.46298/LMCS-18(1:28)2022.
  19. Thierry Coquand, Fabian Ruch, and Christian Sattler. Constructive sheaf models of type theory. Mathematical Structures in Computer Science, 31(9):979-1002, 2021. URL: https://doi.org/10.1017/S0960129521000359.
  20. Peter Dybjer. Internal type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs, International Workshop TYPES'95, Torino, Italy, June 5-8, 1995, Selected Papers, volume 1158 of Lecture Notes in Computer Science, pages 120-134. Springer, 1995. URL: https://doi.org/10.1007/3-540-61780-9_66.
  21. Th. Ehrhard. Une sémantique catégorique des types dépendents. PhD thesis, University of Paris VII, 1988. Google Scholar
  22. Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz. The yoneda embedding in simplicial type theory. In 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 127-142, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00017.
  23. Alexander Grothendieck. Revêtements étales et groupe fondamental. Séminaire de Géométrie Algébrique du Bois-Marie 1960-61 (SGA 1), volume 224 of Lecture Notes in Mathematics. Springer-Verlag, 1971. Dirigé par A. Grothendieck. Augmenté de deux exposés de Mme M. Raynaud. URL: https://doi.org/10.1007/BFb0058656.
  24. Martin Hofmann. Syntax and semantics of dependent types. In Semantics and Logics of Computation, Publications of the Newton Institute, pages 79-130. Cambridge University Press, 1997. Google Scholar
  25. Peter T. Johnstone. Sketches of an elephant: a topos theory compendium. Vol. 2, volume 44 of Oxford Logic Guides. The Clarendon Press, Oxford University Press, Oxford, 2002. Google Scholar
  26. Ambrus Kaposi, Simon Huber, and Christian Sattler. Gluing for Type Theory. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1-25:19, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2019.25.
  27. Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of univalent foundations (after Voevodsky). J. Eur. Math. Soc. (JEMS), 23(6):2071-2126, 2021. URL: https://doi.org/10.4171/JEMS/1050.
  28. Anders Kock. General algebra-geometry duality. Prepublications Math., pages 33-34, 1981. URL: https://tildeweb.au.dk/au76680/GAGD.pdf.
  29. Anders Kock. Duality for generic algebras, 2014. URL: https://arxiv.org/abs/1412.6660.
  30. Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. Internal Universes in Models of Homotopy Type Theory. In Hélène Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), volume 108 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:17, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.22.
  31. Per Martin-Löf. Intuitionistic Type Theory, volume 1 of Studies in Proof Theory. Lecture Notes. Bibliopolis, Naples, 1984. Notes by Giovanni Sambin. Google Scholar
  32. Ian Orton and Andrew M. Pitts. Axioms for modelling cubical type theory in a topos. Logical Methods in Computer Science, Volume 14, Issue 4, December 2018. URL: https://doi.org/10.23638/LMCS-14(4:23)2018.
  33. Emily Riehl and Michael Shulman. A type theory for synthetic ∞-categories. Higher Structures, 1(1):147-224, 2017. URL: https://doi.org/10.1007/s42001-017-0005-6.
  34. Egbert Rijke. The join construction, 2017. URL: https://arxiv.org/abs/1701.07538.
  35. Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science, Volume 16, Issue 1, January 2020. URL: https://doi.org/10.23638/LMCS-16(1:2)2020.
  36. Fabian Ruch. Groupoid-Valued Presheaf Models of Univalent Type Theory. PhD thesis, University of Gothenburg, 2022. URL: https://gupea.ub.gu.se/bitstream/handle/2077/73854/avhandling.pdf.
  37. Christian Sattler. A constructive ∞-groupoid model of homotopy type theory. Invited talk. URL: https://www.cse.chalmers.se/~sattler/docs/types2025.pdf.
  38. Michael Shulman. All (∞,1)-toposes have strict univalent universes, 2019. URL: https://arxiv.org/abs/1904.07004.
  39. Alex Simpson. Equivalence and conditional independence in atomic sheaf logic. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’24, pages 1-14. ACM, July 2024. URL: https://doi.org/10.1145/3661814.3662132.
  40. Jonathan Sterling and Lingyuan Ye. Domains and classifying topoi, 2025. URL: https://doi.org/10.48550/arXiv.2505.13096.
  41. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact