arxiv: 2605.15126 · v1 · submitted 2026-05-14 · 💻 cs.LO · math.LO

Recognition: 2 theorem links

· Lean Theorem

Constructive higher sheaf models with applications to synthetic mathematics

Thierry Coquand , Jonas H\"ofer , Christian Sattler

Authors on Pith no claims yet

Pith reviewed 2026-05-15 02:59 UTC · model grok-4.3

classification 💻 cs.LO math.LO

keywords higher sheaf modelsconstructive metatheoryunivalencehigher inductive typessynthetic mathematicsdependent type theoryhomotopy type theorysheaf semantics

0 comments

The pith

Higher sheaf models of type theory with univalence and higher inductive types can be built in 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 develops a foundation for higher sheaf models of dependent type theory inside constructive mathematics. Recent synthetic mathematics has used extensions of type theory that include univalence and higher inductive types to treat topics such as simplicial homotopy theory, algebraic geometry, and Stone duality. The authors show how to construct the corresponding sheaf models without invoking non-constructive principles such as excluded middle or choice axioms in the background theory. A reader would care because the result places these synthetic developments on the same constructive footing as ordinary type theory and set theory. This makes it possible to carry out the synthetic arguments while remaining inside a computable and formally verifiable framework.

Core claim

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.

What carries the argument

Constructive higher sheaf models for dependent type theory extended by univalence and higher inductive types.

If this is right

Synthetic algebraic geometry acquires a constructive model.
Simplicial homotopy type theory can be interpreted without classical logic.
Synthetic Stone duality receives a constructive sheaf-theoretic semantics.
Other synthetic developments built on univalent type theory become available inside constructive foundations.

Where Pith is reading between the lines

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

The models may support program extraction or computational content from synthetic proofs.
The same technique could be applied to further extensions of type theory beyond those listed.
These constructions give an explicit bridge from synthetic mathematics to ordinary constructive set theory.

Load-bearing premise

Higher sheaf models satisfying univalence and higher inductive types can be assembled using only constructive methods in the metatheory.

What would settle it

A specific construction of a simplicial homotopy type theory model whose internal logic is shown to require the law of excluded middle or a choice principle would refute the central claim.

read the original abstract

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.

Desk Editor's Note private letter to a colleague

Coquand, Höfer and Sattler give an explicit constructive construction of higher sheaf models for univalent type theory with HITs, which is new and removes the usual classical assumptions in the metatheory.

read the letter

The main point is that they build higher sheaf models for dependent type theory extended with univalence and higher inductive types inside a fully constructive metatheory. This directly supports interpretations of simplicial homotopy type theory, synthetic algebraic geometry, and synthetic Stone duality without non-constructive steps in the background logic. That is the concrete advance over earlier sheaf-model work, which often needed classical choice or excluded middle at the meta level. The construction is presented as a foundation rather than a reduction, and the abstract plus stress-test notes give no sign of hidden circularity or invented entities. The citation pattern tracks the relevant synthetic mathematics literature cleanly. The math appears formally grounded enough to be worth checking in detail, especially the verification that the models preserve univalence and the higher inductive types. A possible soft spot is that the higher-categorical aspects of the sheaf toposes could contain subtle gaps in the constructive proofs that only surface on line-by-line reading, but nothing in the available description indicates a load-bearing flaw. This is for people already working in homotopy type theory or formal synthetic geometry who need constructive models they can trust inside proof assistants. A reader who follows Coquand-style type theory or wants to formalize geometry without classical detours will find usable material. It deserves a serious referee because the claim is technically sharp, the evidence is reproducible in principle, and the area is active enough that the details matter.

Referee Report

0 major / 2 minor

Summary. The paper claims to provide a foundation of higher sheaf models of type theory in a constructive metatheory, and in particular to build constructive models of formal systems extending dependent type theory with univalence and higher inductive types, with applications to simplicial homotopy type theory, synthetic algebraic geometry, and synthetic Stone duality.

Significance. If the constructions are correct, the work supplies a direct constructive foundation for these synthetic developments rather than a reduction to classical set theory. This strengthens the metatheoretic justification for univalent type theory with HITs in sheaf models and supports the reliability of synthetic proofs in the cited areas.

minor comments (2)

[Abstract] The abstract states the existence of the constructions but does not name the precise constructive metatheory (e.g., which variant of Martin-Löf type theory or set theory is used as the ambient theory); adding this would clarify the scope of constructivity.
Notation for the higher sheaf toposes and the interpretation of univalence/HITs is introduced without a dedicated preliminary section; a short table or diagram summarizing the key functors and their constructivity properties would improve readability.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment of our work on constructive higher sheaf models and the recommendation for minor revision. No specific major comments were raised in the report, so we have no point-by-point responses to provide at this stage. We will incorporate any minor suggestions during the revision process to strengthen the presentation of the constructive metatheory and its applications to synthetic mathematics.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper constructs higher sheaf models of type theory directly from a constructive metatheory, providing foundations for extensions with univalence and higher inductive types. No load-bearing step reduces by definition, fitted parameter, or self-citation chain to the inputs; the models are built explicitly against external type-theoretic benchmarks without renaming known results or smuggling ansatzes. The derivation chain is self-contained and independent.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The claim rests on standard axioms of dependent type theory extended by univalence and higher inductive types, plus the assumption that sheaf models can be lifted constructively.

axioms (2)

domain assumption Dependent type theory extended with univalence and higher inductive types
Invoked in the abstract as the base for the synthetic systems being modeled.
domain assumption Constructive metatheory
The paper specifies that all constructions must remain within a constructive setting.

pith-pipeline@v0.9.0 · 5341 in / 1080 out tokens · 42827 ms · 2026-05-15T02:59:00.283425+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

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

IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We provide a foundation of higher sheaf models of type theory in a constructive metatheory... using lex modalities... cobar modality... descent data operation D
IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

construct models of HoTT... supporting higher inductive types... Blechschmidt’s duality axiom

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]

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]

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]

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]

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]

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]

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]

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]

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

work page 1973
[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]

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]

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]

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]

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. FLAP , 4(10):3127--3170, 2017. URL: http://collegepublications.co.uk/ifcolog/?00019

work page 2017
[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]

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]

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]

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]

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]

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]

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

work page 1988
[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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

Modalities in homotopy type theory.Logical Methods in Computer Science, 16, January 2020.doi:10.23638/LMCS-16(1:2)2020

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]

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]

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]

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]

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]

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]

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