Projective Presentations of Lex Modalities

Mark Damuni Williams

REVIEW 4 major objections 6 minor 14 references

Projective Presentations of Lex Modalities

T0 review · 4 major / 6 minor · reviewed 2026-08-09 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read By representing a lex modality as a presentation of types, the paper turns Grothendieck topologies into explicit internal sheaf conditions and proves local choice and cohomology vanishing.

desk verdict Genuinely useful presentation framework for topological modalities, but the cohomology descent lemma is false as stated and needs repair. read the letter →

arxiv 2501.19187 v1 pith:4YAA2DGO submitted 2025-01-31 cs.LO math.CT

Mark Damuni Williams This is my paper · ORCID

classification cs.LOmath.CT MSC 03B3818F1018F20

keywords homotopytypetheorylexmodalitiesGrothendiecktopologiessheafconditionsiteratedjoinslocalchoicecohomologysyntheticalgebraicgeometry

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Homotopy type theory is the internal language of higher toposes, and modalities are the internal way to cut out subuniverses. This paper defines a presentation of a lex modality (a pullback-preserving modality, the internal analogue of a subtopos): a collection $T$ of types containing $1$ and closed under dependent sums, which is meant to internalize the data of a Grothendieck topology. Its central claim is that a presentation determines its sheaves by a finite sheaf condition at every truncation level: for $n\ge 0$, an $(n-2)$-type $X$ is a $T$-sheaf exactly when every $T$-cover $f:A\to B$ induces an equivalence $(B\to X)\simeq(A^{\ast_B n}\to X)$. When all types in the presentation are projective, the paper obtains explicit computational tools for the modality, including a formula for sheafifying propositions, a local choice principle, internal reasoning about the sheaf subuniverse, and vanishing of first cohomology on projective types. These tools are then applied to synthetic algebraic geometry and triangulated type theory, proving subcanonicality of the Zariski, étale, and fppf presentations and showing that the interval is simplicial without two of the previously used axioms.

What carries the argument

The central object is a presentation: a collection $T$ of types containing the unit type and closed under dependent sums, thought of as the fibers of covering families. Closure under $\Sigma$ is what makes covers compose and pull back, so the collection actually behaves like a topology. The technical workhorse is the iterated join $A^{\ast_B n}$ of a cover $f:A\to B$; by the join-of-maps lemma its fibers are the iterated joins of the fibers of $f$, which is exactly what lets a sheaf condition be written without coherence data. Lemma 4.6 states that dependent products of $n$-type families over $A^{\ast(n+3)}$ already agree with those over $A^{\ast(n+2)}$, and this stabilization is what cuts the infinite join colimit down to a finite equivalence test. On top of that, projectivity of the types in $T$, an internal axiom-of-choice condition on type families, is what makes quantifiers commute with truncations, producing the explicit sheafification formula, local choice, and the cohomology vanishing theorem.

What would settle it

A proof assistant check of Lemma 4.6, beginning with the case $A=S^1$, $n=1$, where the claim says dependent products of $1$-type families over $A^{\ast 4}$ equal those over $A^{\ast 3}$, would settle the stabilization premise; a counterexample to that equivalence would force the exact form of Corollary 4.9 to be re-indexed.

Watch

Extended reading notes

Core claim

The paper's discovery is that presentations are a workable internal stand-in for Grothendieck topologies. A presentation $T$ generates a modality by nullifying at the propositional truncations of the types in $T$; the modal types are the $T$-sheaves, and a map is a $T$-cover when all its fibers lie in $T$. The main theorem, Corollary 4.9, is that for every $n\ge 0$, an $(n-2)$-type $X$ is a $T$-sheaf if and only if for every $T$-cover $f:A\to B$ the natural map $(B\to X)\to(A^{\ast_B n}\to X)$ is an equivalence, where $\ast_B$ is the join of maps over $B$. This gives the ordinary sheaf condition for sets and internal stack conditions at higher truncation levels, with iterated joins replacing the coherence data that would otherwise be needed. If $T$ is projective, the sheafification of a proposition is explicit: the sheafification of $P$ is the proposition that there exists $A\in T$ with $A\to P$; the paper derives a $T$-local partial choice principle, and for abelian groups $A$ satisfying a descent exactness condition it proves $H^1_{T}(X,A)=0$ for projective $X$. The applications show the Zariski, étale, and fppf presentations are subcanonical, that quasi-coherent modules have stable cohomology across those subtoposes, and that the interval in triangulated type theory is simplicial using duality alone.

Load-bearing premise

Everything in the paper's sheaf condition rests on the unformalized Lemma 4.6 claim that dependent products of $n$-type families over an $(n+3)$-fold iterated join already equal those over the $(n+2)$-fold join, so a one-level error there would shift every sheaf test.

Editorial extensions

If this is right

Membership in the subuniverse becomes checkable: for a projective presentation, a type is a sheaf exactly when the explicit cover-by-cover equivalence holds at its truncation level.
Local choice lets constructions in the sheaf subuniverse proceed by first choosing a cover, the way Zariski-local choice is used in synthetic algebraic geometry.
The Zariski, étale, and fppf presentations are subcanonical, so the affine spectra used to generate these topologies are themselves sheaves.
Quasi-coherent modules satisfy descent for these presentations, giving $H^1=0$ on projective affine spectra and stability of cohomology between the corresponding subtoposes.
In triangulated type theory, the sheaf condition reduces the statement that the interval $I$ is simplicial to a lattice-theoretic calculation, removing the need for two additional axioms.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Editorial inference: the same join-based sheaf condition should give a uniform statement of stack conditions for every finite $n$ in homotopy type theory, since the paper shows each level only needs the stabilization lemma rather than explicit coherence data.
Editorial inference: the descent condition on abelian groups is a cocycle condition, so Theorem 6.12 looks like the first case of a Čech-cohomology comparison; the paper itself points in this direction in Remark 6.14.
Editorial inference: because projectivity is what makes the formulas explicit, one natural test is whether the main theorems survive for presentations generated by projective covers rather than projective objects, which would broaden the class of topologies covered.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Read Damuni Williams' paper. The main contribution is a genuinely useful abstraction: presentations of lex modalities that internalize Grothendieck topologies, with explicit sheaf conditions built from iterated joins. The projective presentation setup, the local choice principle, and the applications—removing axioms from simplicial HoTT and the subcanonicality checks—are new and mostly convincing. The lattice-theoretic proof that I is simplicial is a highlight.

The cohomology section has a real problem. Lemma 6.10 claims descent for all T-covers goes from descent on presentation fibers to the full Čech complex. The proof says product preserves exactness. In HoTT, exactness supplies pointwise mere preimages; assembling them over an arbitrary base type requires choice. This is not a pedantic point: take T generated by inhabited finite types, which satisfies descent for every abelian group, and the two-interval cover U+V→S^1. The fibres are 1 or 2, so it's a T-cover, and Lemma 6.10 would make the Čech complex exact, forcing H^1_Cech(S^1,Z)=0, which is false. So Lemma 6.10 is false as stated. Theorem 6.12 applies it to a projective X, and that extra hypothesis might repair the product step, but as written the proof is invalid. Corollary 7.23 also overstates: only quasicoherent modules are shown to satisfy descent, not every abelian group.

There are smaller technical rough spots: Lemma 4.6's stabilization lemma is sketched and load-bearing; Lemma 5.6 has notational abuse and a hidden projectivity step, though it can be fixed. These are minor relative to the cohomology gap.

The framework and the sheaf condition portions are solid enough to justify a serious referee. The cohomology section needs substantive correction before the paper can be accepted. I would recommend sending to peer review with a request for a careful check of Section 6, and I'd bring the paper to a reading group to discuss the sheaf conditions and the choice issue.

Referee Report

4 major / 6 minor

Summary. This paper introduces presentations of lex/topological modalities in homotopy type theory: a collection T of types closed under dependent sums and containing the unit, which generates a sheafification modality by nullifying at the propositional truncations of its members. It defines T-covers, proves an internal sheaf condition expressed through iterated joins (Corollary 4.9), and, for projective presentations, gives an explicit sheafification of propositions, a local choice principle, and a cohomology vanishing theorem for H^1. Applications include subcanonicality checks for Zariski-, étale-, and fppf-style presentations and a proof that the interval I is simplicial in triangulated type theory with fewer axioms than in previous work.

Significance. If the framework is correct, it is a useful internalisation of Grothendieck-topos sheaf conditions in HoTT, with explicit computational content: membership in the modal subuniverse is detected by concrete sheaf tests, and projective presentations yield a local choice principle and cohomology computations. The paper gives due credit to the external motivation and includes several clean ingredients, in particular the totalisation lemma (Lemma 4.8) and the reduction of subcanonicality to algebraic gluing statements. At the same time, the cohomology section contains a false lemma as stated and an overclaiming corollary, and the stabilization lemma on iterated joins is only sketched; these issues are load-bearing and need repair. The paper is not machine-checked, and a formalization would substantially increase confidence.

major comments (4)

[Section 6, Theorem 6.12] The proof identifies the loop space at the basepoint of ©K(A,1) with A, writing "(pt = pt) ≃ A by definition of K(A,1), exploiting lexness of ©." By Proposition 6.6 this is valid only when A is a group sheaf, i.e., a modal abelian group; otherwise the loop space is ©A. The hypothesis that A satisfies descent for T is not shown to imply that A is modal. Please add the sheaf/modality hypothesis on the coefficient, or prove that descent implies it. This affects the validity of Theorem 6.12 and of Corollaries 7.18 and 7.23 as stated.
[Section 6, Lemma 6.10] The step "product preserves exactness" is not valid in HoTT without a choice principle on the base type. Exactness of each fibre-wise sequence gives, for each x:X, mere existence of a preimage; assembling these into a section of the product requires projectivity (or an external choice principle) for X. As stated the lemma is false: take T generated by inhabited finite types, for which every abelian group satisfies descent, and take the standard two-interval open cover U+V→S^1. The fibres are 1 or 2, so the cover is a T-cover, yet Lemma 6.10 would force the Čech complex of this cover to be exact in the middle, giving H^1_Čech(S^1,Z)=0 for A=Z, contradicting H^1(S^1,Z)=Z. The lemma should be restricted to a projective base type, with a proof using that hypothesis; Theorem 6.12 has the projective base, so it can be repaired, but the lemma as written is false.
[Section 7, Corollary 7.23] The conclusion "for any abelian group G we have H^1(Spec(A),G)=0" does not follow from Theorem 7.22. Theorem 7.22 establishes descent only for quasicoherent R-modules, and the proof explicitly uses the identification M^{Spec(A)} = M⊗_R A. An arbitrary abelian group need not carry an R-module structure and need not satisfy descent for the relevant presentation. The corollary should be restricted to quasicoherent modules, or a separate descent proof for all abelian groups must be supplied.
[Section 4, Lemma 4.6] The stabilization lemma is load-bearing for Corollary 4.7, the sheaf condition in Corollary 4.9, and all subsequent sheaf tests, but its proof is only a sketch. In particular, the verification of the second composite is compressed into the sentence "This means that this map ... is equal to φ, and we are done," and the induction step for the gluing data requires careful handling of the pushout coherences. If the stabilization level is off by one, the sheaf tests used throughout would shift. Please provide a complete proof with all composites and coherences, or a machine-checked formalization.

minor comments (6)

[Lemma 3.5 proof] The dependent sum is written with X and Y interchanged: the family should be Y(x) for x:X, so the displayed sums should be Σ_{x:X}Y(x). The equalities involving © and Σ also need a justification or citation.
[Lemma 5.6] The notation "P A" and "P g(x)" is ambiguous; use P^A and g(x)→P to distinguish the exponential type from application of the proposition P to a type.
[Corollary 4.9 proof] In the converse direction, "for any X∈T" should read "for any A∈T"; also, the notation A^{*_B}^n should be specified for n=0.
[Section 6, Definition 6.2] Cohomology is defined for a group G, but the subsequent theory applies only to abelian groups (or abelian group objects); this should be stated explicitly.
[Theorem 6.12 proof] The step from pointwise equality ∏_{x:X} χ(x)=pt to "χ is merely the constant map" should explicitly invoke function extensionality for the path type of ©K(A,1).
[Throughout] There are many typographical errors, including "acc ess", "presentaitons", "cohomolgoy", and "ﬁntiely prestented"; a careful proofreading pass is needed.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity; results are derived from stated axioms and external theorems.

full rationale

The derivation chain is self-contained and does not reduce to its inputs by construction. Presentations are defined as collections of types closed under Σ and containing 1, and the associated modality is defined by nullification at propositional truncations; Corollary 4.9's sheaf condition is then proved from these definitions together with independent join-theoretic results (Rijke [11]) and an inductive stabilization lemma (Lemma 4.6), whose proof does not presuppose the sheaf condition. Lemma 5.6 and the local choice principle (Lemma 5.9) follow from the explicitly stated projectivity assumption rather than from the conclusions they support. In the cohomology section, descent is an input hypothesis about the abelian group A, and Theorem 6.12 derives vanishing of H^1 for projective X from it; the theorem is not a restatement of the descent definition, and H^1_© is defined independently via Eilenberg-Mac Lane spaces. The axioms in Section 7 (Blechschmidt duality, projectivity of spectra, constancy of maps to N) are added as assumptions and then used to derive subcanonicality and local-choice consequences; they are not invoked to prove themselves, and the surrounding external justifications are cited from non-overlapping literature. There is no load-bearing self-citation chain, no fitted parameter renamed as a prediction, and no uniqueness theorem imported from the author's own prior work. The only notable concern is a possible correctness gap in Lemma 6.10's 'product preserves exactness' step, which would be a mathematical flaw rather than circularity; it does not make the paper's central claims equivalent to their assumptions by definition.

Assumptions & free parameters 0 free parameters · 7 assumptions · 0 invented entities

The central derivation relies on standard HoTT axioms (univalence, higher inductive types), cited theorems about modalities and joins, and three explicitly introduced synthetic axioms (duality, projectivity, constancy of maps to N) that are justified by external models but not derived in HoTT. There are no fitted numeric parameters and no invented entities.

assumptions (7)

standard math Univalence and higher inductive types (including propositional truncation and nullification)
Used throughout; the paper states it follows the HoTT book conventions (Section 2).
standard math Lex modalities preserve truncation levels and satisfy ©(x=y)≃η(x)=η(y)
Cited from [13, Corollary 3.9 and Theorem 3.1.ix]; used in Proposition 6.6 and Theorem 6.12.
standard math Facts about joins: fibers of joins and image as colimit of iterated joins
Cited from [11, Theorem 2.2 and related]; used in Lemmas 4.3, 4.4 and the sheaf condition.
domain assumption Axiom 7.3 (Blechschmidt duality): A → U_T^{Spec(A)} is an equivalence for finitely presented U_T-algebras
Added as an axiom for the synthetic theory; externally true in the classifying topos, but not proved inside HoTT here.
domain assumption Axiom 7.5: Spec(A) is projective for finitely presented U_T-algebras A
Added as an axiom; justified by representables in presheaf toposes being projective, but the internal proof is not given.
domain assumption Axiom 7.8: maps Spec(A) → N are constant (diagonal N → N^{Spec(A)} is an equivalence)
Added as an axiom; proven externally for presheaf categories with initial object in Lemma 7.9.
standard math Theorem 7.26 on congruences in distributive lattices
Cited from [6, Chapter 9, Theorem 3]; used in the proof that I is simplicial.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Projective Presentations of Lex Modalities." pith.science (2026). https://pith.science/paper/4YAA2DGO

@misc{pith2026250119187,
  author       = {Pith},
  title        = {Pith review of: Projective Presentations of Lex Modalities},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/4YAA2DGO}},
  note         = {Machine review of arXiv:2501.19187}
}

read the original abstract

Modalities in homotopy type theory are used to create and access subuniverses of a given type universe. These have significant applications throughout mathematics and computer science, and in particular can be used to create universes in which certain logical principles are true. We define presentations of topological modalities, which act as an internalisation of the notion of a Grothendieck topology. A specific presentation of a modality gives access to a surprising amount of computational information, such as explicit methods of determining membership of the subuniverse via internal sheaf conditions. Furthermore, assuming all terms of the presentation satisfy the axiom of choice, we are able to describe generic and powerful computational tools for modalities. This assumption is validated for presentations given by representables in presheaf categories. We deduce a local choice principle, and an internal reconstruction of Kripke-Joyal style reasoning. We use the local choice principle to show how to relate cohomology between universes, showing that a certain class of abelian groups has cohomolgoy stable between universes. We apply the methods to a prominent example, a type theory axiomatising the classifying topos of an algebraic theory, which specialises to give type theories for synthetic algebraic geometry and synthetic higher category theory. We apply the sheaf conditions to show that several presentations of interest are subcanonical, and apply the cohomology methods to show that quasi-coherent modules have cohomology stable between the Zariski, \'etale and fppf toposes.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

14 extracted references · 11 canonical work pages

[1]

A General Nullstellensatz for Generalised Spaces

Ingo Blechschmidt. A General Nullstellensatz for Generalised Spaces . 2024. url: https ://rawgit.com/iblech/internal-methods/master/paper- qcoh.pdf

work page 2024
[2]

Čech Cohomology in Homotopy Type Theory

Ingo Blechschmidt, Felix Cherubini, and David Wärn. Čech Cohomology in Homotopy Type Theory. 2024. url: https://www.felix-cherubini.de/chech.pdf

work page 2024
[3]

A Foundation for Synthetic Algebraic Geometry

Felix Cherubini, Thierry Coquand, and Matthias Hutzler . A Foundation for Synthetic Al- gebraic Geometry. 2023. arXiv: 2307.00073 [math.AG]

work page Pith review arXiv 2023
[4]

Directed univalence in simpli- cial homotopy type theory

Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchhol tz. Directed univalence in simpli- cial homotopy type theory . 2024. arXiv: 2407.09146 [cs.LO]

arXiv 2024
[5]

Multimodal Dependent Type Theory

Daniel Gratzer et al. “Multimodal Dependent Type Theory ”. In: Logical Methods in Com- puter Science Volume 17, Issue 3 (July 2021). issn: 1860-5974. doi: 10.46298/lmcs-17(3 :11)2021. url: http://dx.doi.org/10.46298/lmcs-17(3:11)2021

work page doi:10.46298/lmcs-17(3 2021
[6]

G. Gratzer. Lattice Theory: First Concepts and Distributive Lattices . Dover Books on Math- ematics Series. Dover Publications, 2009. isbn: 9780486471730. url: https://books.goo gle.co.uk/books?id=6FJPTsmF1RAC

work page 2009
[7]

Eilenberg-MacLane s paces in homotopy type theory

Daniel R. Licata and Eric Finster. “Eilenberg-MacLane s paces in homotopy type theory”. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL A nnual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual AC M/IEEE Symposium on Logic in Computer Science (LICS) . CSL-LICS ’14. Vienna, Austria: Association for Com- puting Machinery,...

work page arXiv 2014
[8]

Commutative Algebra: Constructive Methods: Finite Projective Modules

Henri Lombardi and Claude Quitté. Commutative Algebra: Constructive Methods: Finite Projective Modules. Springer Netherlands, 2015. isbn: 9789401799447. doi: 10.1007/978 -94-017-9944-7 . url: http://dx.doi.org/10.1007/978-94-017-9944-7

doi:10.1007/978 2015

Show all 14 references

[9]

Sheaves in Synthetic Algebraic Geometry

Hugo Moeneclaey. Sheaves in Synthetic Algebraic Geometry . 2024. url: https://felix -cherubini.de/sheaves.pdf . 25

2024
[10]

Orbifolds as microlinear types in synthetic diﬀerential co hesive homotopy type theory

David Jaz Myers. Orbifolds as microlinear types in synthetic diﬀerential co hesive homotopy type theory. 2022. arXiv: 2205.15887 [math.AT]

2022 arXiv
[11]

The join construction

Egbert Rijke. The join construction . 2017. arXiv: 1701.07538 [math.CT]

2017 arXiv
[12]

A Type Theory with a Tiny Object

Mitchell Riley. A Type Theory with a Tiny Object . 2024. arXiv: 2403.01939 [math.CT] . url: https://arxiv.org/abs/2403.01939

2024 arXiv
[13]

Moda lities in homotopy type theory

Bas Spitters, Michael Shulman, and Egbert Rijke. “Moda lities in homotopy type theory”. In: Logical Methods in Computer Science 16 (2020)

2020
[14]

Homotopy Type Theory: Univalent Foundations of Mathematics

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

2013

Pith tools

Reviewed August 9, 2026 · model on record in the stance chip above.

[1] [1]

A General Nullstellensatz for Generalised Spaces

Ingo Blechschmidt. A General Nullstellensatz for Generalised Spaces . 2024. url: https ://rawgit.com/iblech/internal-methods/master/paper- qcoh.pdf

work page 2024

[2] [2]

Čech Cohomology in Homotopy Type Theory

Ingo Blechschmidt, Felix Cherubini, and David Wärn. Čech Cohomology in Homotopy Type Theory. 2024. url: https://www.felix-cherubini.de/chech.pdf

work page 2024

[3] [3]

A Foundation for Synthetic Algebraic Geometry

Felix Cherubini, Thierry Coquand, and Matthias Hutzler . A Foundation for Synthetic Al- gebraic Geometry. 2023. arXiv: 2307.00073 [math.AG]

work page Pith review arXiv 2023

[4] [4]

Directed univalence in simpli- cial homotopy type theory

Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchhol tz. Directed univalence in simpli- cial homotopy type theory . 2024. arXiv: 2407.09146 [cs.LO]

arXiv 2024

[5] [5]

Multimodal Dependent Type Theory

Daniel Gratzer et al. “Multimodal Dependent Type Theory ”. In: Logical Methods in Com- puter Science Volume 17, Issue 3 (July 2021). issn: 1860-5974. doi: 10.46298/lmcs-17(3 :11)2021. url: http://dx.doi.org/10.46298/lmcs-17(3:11)2021

work page doi:10.46298/lmcs-17(3 2021

[6] [6]

G. Gratzer. Lattice Theory: First Concepts and Distributive Lattices . Dover Books on Math- ematics Series. Dover Publications, 2009. isbn: 9780486471730. url: https://books.goo gle.co.uk/books?id=6FJPTsmF1RAC

work page 2009

[7] [7]

Eilenberg-MacLane s paces in homotopy type theory

Daniel R. Licata and Eric Finster. “Eilenberg-MacLane s paces in homotopy type theory”. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL A nnual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual AC M/IEEE Symposium on Logic in Computer Science (LICS) . CSL-LICS ’14. Vienna, Austria: Association for Com- puting Machinery,...

work page arXiv 2014

[8] [8]

Commutative Algebra: Constructive Methods: Finite Projective Modules

Henri Lombardi and Claude Quitté. Commutative Algebra: Constructive Methods: Finite Projective Modules. Springer Netherlands, 2015. isbn: 9789401799447. doi: 10.1007/978 -94-017-9944-7 . url: http://dx.doi.org/10.1007/978-94-017-9944-7

doi:10.1007/978 2015