pith. sign in

arxiv: 2605.15126 · v2 · pith:4D77BGG2new · submitted 2026-05-14 · 💻 cs.LO · math.LO

Constructive higher sheaf models with applications to synthetic mathematics

Thierry Coquand , Jonas H\"ofer , Christian Sattler This is my paper

Pith reviewed 2026-05-20 20:05 UTC · model grok-4.3

classification 💻 cs.LO math.LO
keywords higher sheaf modelsdependent type theoryunivalencehigher inductive typesconstructive metatheorysynthetic mathematicssimplicial homotopy type theory
0
0 comments X

The pith

Higher sheaf models of dependent type theory with univalence and higher inductive types can be built inside a constructive metatheory.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper constructs higher sheaf models for type theories extended by univalence and higher inductive types while working entirely in constructive mathematics. This supplies explicit models for systems used in synthetic homotopy theory, synthetic algebraic geometry, and synthetic Stone duality. A reader would care because these synthetic approaches can now be interpreted without assuming classical principles such as the law of excluded middle. The construction therefore gives a direct foundation for carrying out synthetic mathematics in a setting that remains valid constructively.

Core claim

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, including simplicial homotopy type theory, synthetic algebraic geometry, and synthetic Stone duality.

What carries the argument

Higher sheaf models, which interpret dependent type theory with univalence and higher inductive types inside a topos-like structure that can be defined constructively.

If this is right

  • Simplicial homotopy type theory admits a constructive model.
  • Synthetic algebraic geometry can be carried out inside a constructive metatheory.
  • Synthetic Stone duality receives an explicit constructive interpretation.
  • The same method yields models for other extensions of dependent type theory by univalence and higher inductive types.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The construction may allow synthetic developments to be formalized directly in constructive proof assistants without adding classical axioms.
  • It could connect existing constructive topos theory with higher-dimensional structures used in homotopy type theory.
  • Similar techniques might extend to other sheaf-like models for type theories beyond the ones treated here.

Load-bearing premise

Higher sheaf models of dependent type theory extended by univalence and higher inductive types can be constructed while remaining inside a constructive metatheory.

What would settle it

A concrete case in which the proposed construction of a higher sheaf model for univalence plus a specific higher inductive type requires the axiom of choice or produces an inconsistency when formalized in a constructive metatheory would refute the central claim.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The manuscript develops a foundation for higher sheaf models of dependent type theory in a constructive metatheory. It constructs models of type theory extended by univalence and higher inductive types over suitable sites, and applies these to synthetic mathematics including simplicial homotopy type theory, synthetic algebraic geometry, and synthetic Stone duality.

Significance. If the constructions hold, the result is significant for foundations of synthetic mathematics, as it supplies fully constructive models that avoid excluded middle or choice. The paper ships explicit, choice-free constructions of the sheafification functor and the interpretation of path spaces, carried out parameter-free in the metatheory; these are concrete strengths that enhance applicability to computability and constructive reasoning.

minor comments (3)
  1. §2.3: the internalization of the sheaf condition for higher sheaves is introduced without an explicit comparison to the standard 1-sheaf case; adding a short remark on how the higher case reduces would improve readability.
  2. Notation for the path-space interpretation in §4.1 uses an overloaded symbol for the sheafified equality; a distinct symbol or a clarifying sentence would prevent confusion with the underlying type theory.
  3. The applications section (§5) references synthetic Stone duality but does not include a brief statement of the site chosen for that model; adding one sentence would make the connection to the general construction immediate.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of the manuscript, the recognition of its significance for constructive foundations of synthetic mathematics, and the recommendation for minor revision. No specific major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper's central construction proceeds by defining a notion of higher sheaves over a site directly in the internal language of a topos within a constructive metatheory, then explicitly building the sheafification functor and interpreting univalence and higher inductive types via choice-free, parameter-free definitions of path spaces and related structures. These steps are carried out as independent constructive verifications that do not reduce to fitted parameters, self-definitional equations, or load-bearing self-citations whose content is itself unverified; the argument remains self-contained against external benchmarks of constructivity without invoking excluded middle or choice.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Review performed on abstract only; no specific free parameters, axioms, or invented entities can be extracted from the provided text.

pith-pipeline@v0.9.0 · 5572 in / 918 out tokens · 30130 ms · 2026-05-20T20:05:28.647248+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

41 extracted references · 41 canonical work pages · 4 internal anchors

  1. [1]

    On Relating Type Theories and Set Theories

    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

    work page 1998

  2. [2]

    Two-level type theory and applications

    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. https://doi.org/10.1017/S0960129523000130 doi:10.1017/S0960129523000130

    work page doi:10.1017/s0960129523000130 2023

  3. [3]

    Artin, A

    M. Artin, A. Grothendieck, and J. L. Verdier. Th \'e orie de Topos et Cohomologie Etale des Sch \'e mas. Tome 1: Th\'eorie des topos, S\'eminaire de G\'eom\'etrie Alg\'ebrique du Bois-Marie 1963--1964 (SGA 4) , volume 269 of Lecture Notes in Mathematics . Springer-Verlag, Berlin, 1972. Dirig\'e par M. Artin, A. Grothendieck, et J. L. Verdier. Avec la coll...

    work page 1963

  4. [4]

    Natural models of homotopy type theory

    Steve Awodey. Natural models of homotopy type theory. Mathematical Structures in Computer Science , 28(2):241--286, 2018. https://doi.org/10.1017/S0960129516000268 doi:10.1017/S0960129516000268

    work page doi:10.1017/s0960129516000268 2018

  5. [5]

    Non-Constructivity in Kan Simplicial Sets

    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 ...

    work page doi:10.4230/lipics.tlca.2015.92 2015

  6. [6]

    Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl

    Mark Bickford. Formalizing category theory and presheaf models of type theory in N uprl, 2018. URL: https://arxiv.org/abs/1806.06114, https://arxiv.org/abs/1806.06114 arXiv:1806.06114

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  7. [7]

    A general nullstellensatz for generalized spaces, 2019

    Ingo Blechschmidt. A general nullstellensatz for generalized spaces, 2019. URL: https://rawgit.quasicoherent.io/iblech/internal-methods/master/paper-qcoh.pdf

    work page 2019

  8. [8]

    Kenneth S. Brown. Abstract homotopy theory and generalized sheaf cohomology. Transactions of the American Mathematical Society , 186:419--458, 1973

    work page 1973

  9. [9]

    Generalised algebraic theories and contextual categories

    John Cartmell. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic , 32:209--243, 1986. URL: https://www.sciencedirect.com/science/article/pii/0168007286900539, https://doi.org/10.1016/0168-0072(86)90053-9 doi:10.1016/0168-0072(86)90053-9

    work page doi:10.1016/0168-0072(86)90053-9 1986

  10. [10]

    A foundation for synthetic stone duality, 2024

    Felix Cherubini, Thierry Coquand, Freek Geerligs, and Hugo Moeneclaey. A foundation for synthetic stone duality, 2024. URL: https://arxiv.org/abs/2412.03203, https://arxiv.org/abs/2412.03203 arXiv:2412.03203

    work page arXiv 2024

  11. [11]

    A foundation for synthetic algebraic geometry

    Felix Cherubini, Thierry Coquand, and Matthias Hutzler. A foundation for synthetic algebraic geometry. Mathematical Structures in Computer Science , 34(9):1008--1053, 2024. https://doi.org/10.1017/S0960129524000239 doi:10.1017/S0960129524000239

    work page doi:10.1017/s0960129524000239 2024

  12. [12]

    Projective space in synthetic algebraic geometry, 2025

    Felix Cherubini, Thierry Coquand, Matthias Ritter, and David Wärn. Projective space in synthetic algebraic geometry, 2025. URL: https://arxiv.org/abs/2405.13916, https://arxiv.org/abs/2405.13916 arXiv:2405.13916

    work page arXiv 2025

  13. [13]

    Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom

    Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\" o 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,...

    work page doi:10.4230/lipics.types.2015.5 2015

  14. [14]

    A survey of constructive presheaf models of univalence

    Thierry Coquand. A survey of constructive presheaf models of univalence. ACM SIGLOG News , 5(3):54--65, 7 2018. https://doi.org/10.1145/3242953.3242962 doi:10.1145/3242953.3242962

    work page doi:10.1145/3242953.3242962 2018

  15. [15]

    A note about models of synthetic algebraic geometry, 2025

    Thierry Coquand, Jonas H \"o fer, and Christian Sattler. A note about models of synthetic algebraic geometry, 2025. URL: https://arxiv.org/abs/2512.06025, https://arxiv.org/abs/2512.06025 arXiv:2512.06025

    work page arXiv 2025

  16. [16]

    o rtberg. On higher inductive types in cubical type theory. In Anuj Dawar and Erich Gr \

    Thierry Coquand, Simon Huber, and Anders M \" o rtberg. On higher inductive types in cubical type theory. In Anuj Dawar and Erich Gr \" a 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. https://doi.org/10.1145/3209108.3209197 doi:10.1145/320...

    work page doi:10.1145/3209108.3209197 2018

  17. [17]

    Canonicity and homotopy canonicity for cubical type theory

    Thierry Coquand, Simon Huber, and Christian Sattler. Canonicity and homotopy canonicity for cubical type theory. Logical Methods in Computer Science , 18(1), 2022. https://doi.org/10.46298/LMCS-18(1:28)2022 doi:10.46298/LMCS-18(1:28)2022

    work page doi:10.46298/lmcs-18(1:28)2022 2022

  18. [18]

    Constructive sheaf models of type theory

    Thierry Coquand, Fabian Ruch, and Christian Sattler. Constructive sheaf models of type theory. Mathematical Structures in Computer Science , 31(9):979--1002, 2021. https://doi.org/10.1017/S0960129521000359 doi:10.1017/S0960129521000359

    work page doi:10.1017/s0960129521000359 2021

  19. [19]

    Internal type theory

    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, https://doi.org/10.1007/3-540-61...

    work page doi:10.1007/3-540-61780-9 1995

  20. [20]

    Th. Ehrhard. Une s\'emantique cat\'egorique des types d\'ependents . PhD thesis, University of Paris VII, 1988

    work page 1988

  21. [21]

    The yoneda embedding in simplicial type theory

    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. https://doi.org/10.1109/LICS65433.2025.00017 doi:10.1109/LICS65433.2025.00017

    work page doi:10.1109/lics65433.2025.00017 2025

  22. [22]

    Rev\^etements \'etales et groupe fondamental

    Alexander Grothendieck. Rev\^etements \'etales et groupe fondamental. S\'eminaire de G\'eom\'etrie Alg\'ebrique du Bois-Marie 1960--61 (SGA 1) , volume 224 of Lecture Notes in Mathematics . Springer-Verlag, 1971. Dirig\'e par A. Grothendieck. Augment\'e de deux expos\'es de Mme M. Raynaud. https://doi.org/10.1007/BFb0058656 doi:10.1007/BFb0058656

    work page doi:10.1007/bfb0058656 1960

  23. [23]

    Syntax and semantics of dependent types

    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

    work page 1997

  24. [24]

    Johnstone

    Peter T. Johnstone. Sketches of an elephant: a topos theory compendium. V ol. 2 , volume 44 of Oxford Logic Guides . The Clarendon Press, Oxford University Press, Oxford, 2002

    work page 2002

  25. [25]

    Gluing for Type Theory

    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 \"u ...

    work page doi:10.4230/lipics.fscd.2019.25 2019

  26. [26]

    The simplicial model of univalent foundations (after V oevodsky)

    Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The simplicial model of univalent foundations (after V oevodsky). J. Eur. Math. Soc. (JEMS) , 23(6):2071--2126, 2021. https://doi.org/10.4171/JEMS/1050 doi:10.4171/JEMS/1050

    work page doi:10.4171/jems/1050 2071

  27. [27]

    General algebra-geometry duality

    Anders Kock. General algebra-geometry duality. Prepublications Math. , pages 33--34, 1981. URL: https://tildeweb.au.dk/au76680/GAGD.pdf

    work page 1981

  28. [28]

    Duality for generic algebras

    Anders Kock. Duality for generic algebras, 2014. URL: https://arxiv.org/abs/1412.6660, https://arxiv.org/abs/1412.6660 arXiv:1412.6660

    work page internal anchor Pith review Pith/arXiv arXiv 2014

  29. [29]

    Licata, Ian Orton, Andrew M

    Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters. Internal Universes in Models of Homotopy Type Theory . In H\' e l\` e 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, Germa...

    work page doi:10.4230/lipics.fscd.2018.22 2018

  30. [30]

    Intuitionistic Type Theory , volume 1 of Studies in Proof Theory

    Per Martin-L \"o f. Intuitionistic Type Theory , volume 1 of Studies in Proof Theory. Lecture Notes . Bibliopolis, Naples, 1984. Notes by Giovanni Sambin

    work page 1984

  31. [31]

    Ian Orton and Andrew M. Pitts. Axioms for modelling cubical type theory in a topos. Logical Methods in Computer Science , Volume 14, Issue 4, Dec 2018. URL: https://lmcs.episciences.org/4491, https://doi.org/10.23638/LMCS-14(4:23)2018 doi:10.23638/LMCS-14(4:23)2018

    work page doi:10.23638/lmcs-14(4:23)2018 2018

  32. [32]

    A type theory for synthetic -categories

    Emily Riehl and Michael Shulman. A type theory for synthetic -categories. Higher Structures , 1(1):147--224, 2017. https://doi.org/10.1007/s42001-017-0005-6 doi:10.1007/s42001-017-0005-6

    work page doi:10.1007/s42001-017-0005-6 2017

  33. [33]

    The join construction

    Egbert Rijke. The join construction, 2017. URL: https://arxiv.org/abs/1701.07538, https://arxiv.org/abs/1701.07538 arXiv:1701.07538

    work page internal anchor Pith review Pith/arXiv arXiv 2017

  34. [34]

    Introduction to Homotopy Type Theory

    Egbert Rijke. Introduction to Homotopy Type Theory . Cambridge Studies in Advanced Mathematics. Cambridge University Press, 2025

    work page 2025

  35. [35]

    Modalities in homotopy type theory

    Egbert Rijke, Michael Shulman, and Bas Spitters. Modalities in homotopy type theory. Logical Methods in Computer Science , Volume 16, Issue 1, Jan 2020. URL: https://lmcs.episciences.org/3826, https://doi.org/10.23638/LMCS-16(1:2)2020 doi:10.23638/LMCS-16(1:2)2020

    work page doi:10.23638/lmcs-16(1:2)2020 2020

  36. [36]

    Groupoid-Valued Presheaf Models of Univalent Type Theory

    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

    work page 2022

  37. [37]

    A constructive \( \)-groupoid model of homotopy type theory

    Christian Sattler. A constructive \( \)-groupoid model of homotopy type theory. Invited talk. URL: https://www.cse.chalmers.se/ sattler/docs/types2025.pdf

    work page

  38. [38]

    All $(\infty,1)$-toposes have strict univalent universes

    Michael Shulman. All ( ,1) -toposes have strict univalent universes, 2019. URL: https://arxiv.org/abs/1904.07004, https://arxiv.org/abs/1904.07004 arXiv:1904.07004

    work page internal anchor Pith review Pith/arXiv arXiv 2019

  39. [39]

    Equivalence and conditional independence in atomic sheaf logic

    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, page 1–14. ACM, July 2024. URL: http://dx.doi.org/10.1145/3661814.3662132, https://doi.org/10.1145/3661814.3662132 doi:10.1145/3661814.3662132

    work page doi:10.1145/3661814.3662132 2024

  40. [40]

    Domains and classifying topoi, 2025

    Jonathan Sterling and Lingyuan Ye. Domains and classifying topoi, 2025. URL: https://arxiv.org/abs/2505.13096, https://arxiv.org/abs/2505.13096 arXiv:2505.13096

    work page arXiv 2025

  41. [41]

    Homotopy Type Theory: Univalent Foundations of Mathematics

    The Univalent Foundations Program . Homotopy Type Theory: Univalent Foundations of Mathematics . https://homotopytypetheory.org/book, Institute for Advanced Study, 2013

    work page 2013