{"id":"8118fa79-a3ca-4e5d-a186-1b2b51fd727d","arxiv_id":"2501.19187","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Presentations of topological modalities in HoTT yield internal sheaf conditions, local choice, and cohomology stability, applied to synthetic algebraic geometry and simplicial type theory.","lead":"This paper builds a framework in homotopy type theory for 'presentations' of topological modalities, internalizing Grothendieck topologies. It uses presentations to derive internal sheaf conditions, a local choice principle, and cohomology comparisons, with applications to synthetic algebraic geometry and directed type theory.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Cohomology descent lemma 6.10 is false as stated: product exactness over arbitrary bases fails in HoTT, so Theorem 6.12's proof has a gap and Corollary 7.23 overstates to all abelian groups.","rationale":"The reader's weakest assumption, Lemma 4.6, is a legitimate technical concern about an unformalized stabilization argument, and I do not dispute it. However, the more immediately falsifiable problem is in the cohomology section: Lemma 6.10's product-exactness step is not a theorem of HoTT without a projectivity or choice assumption on the base type. The S^1 counterexample shows the lemma is false as stated, which means the proof of Theorem 6.12, a central claim, has a genuine gap. The theorem's conclusion is plausibly repairable because the base X in Theorem 6.12 is assumed projective, so the proof can be fixed by adding that hypothesis to Lemma 6.10. I therefore do not move the verdict: the paper is still conditionally acceptable pending repair of this gap and correction of Corollary 7.23. This does not change the reader's overall assessment, but it identifies a different and more concrete load-bearing assumption than Lemma 4.6.","tokens_in":19841,"tokens_out":41564,"duration_ms":422900,"concrete_test":"Verify the S^1 counterexample: let T be the presentation generated by inhabited finite types, A=Z, X=S^1, and Z=U+V for the standard open cover by two intervals. Check that descent for T holds for all abelian groups (finite nonempty sets have acyclic Čech complexes), that φ is a T-cover with fibres 1 and 2, and that the middle cohomology of the asserted exact sequence is H^1_Čech(S^1,Z)=Z, not 0. If this computation is confirmed, Lemma 6.10 is false; then re-check Theorem 6.12 with Lemma 6.10 replaced by the projective-base version, and restrict Corollary 7.23 to quasicoherent modules.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Lemma 6.10 asserts that if A satisfies descent for a presentation T, then for every T-cover φ:Z→X the displayed sequence A^Z → A^{Z×_X Z} → A^{Z×_X Z×_X Z} is exact. The proof says 'product preserves exactness'. In HoTT this is false for arbitrary types: exactness of the fibre sequences gives, for each x:X, the mere existence of a preimage, and assembling these into a section of the product requires choice for X. Concretely, take T to be the presentation generated by inhabited finite types. Then descent for T holds for every abelian group A, because for every nonempty finite set X the Čech complex A^X → A^{X×X} → A^{X×X×X} is exact. Now let φ:U+V→S^1 be the standard two-interval open cover; its fibres are 1 or 2, hence T-covers. Lemma 6.10 would make the Čech complex of this cover exact in the middle, forcing H^1_Čech(S^1,A)=0. Taking A=Z, the transition functions on the two components of U∩V give H^1_Čech(S^1,Z)=Z, a contradiction. Thus Lemma 6.10 as stated is false. Theorem 6.12 only applies the lemma when X is projective, and with that extra hypothesis the product-exactness step can be repaired; but as written the central cohomology proof is not valid. Corollary 7.23 is a separate overstatement: only quasicoherent modules are shown to satisfy descent, not every abelian group.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":20180,"tokens_out":32921,"duration_ms":355567,"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":[{"comment":"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":"Section 6, Theorem 6.12"},{"comment":"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":"Section 6, Lemma 6.10"},{"comment":"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":"Section 7, Corollary 7.23"},{"comment":"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.","section":"Section 4, Lemma 4.6"}],"minor_comments":[{"comment":"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.","section":"Lemma 3.5 proof"},{"comment":"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.","section":"Lemma 5.6"},{"comment":"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":"Corollary 4.9 proof"},{"comment":"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.","section":"Section 6, Definition 6.2"},{"comment":"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).","section":"Theorem 6.12 proof"},{"comment":"There are many typographical errors, including \"acc ess\", \"presentaitons\", \"cohomolgoy\", and \"fintiely prestented\"; a careful proofreading pass is needed.","section":"Throughout"}],"recommendation":"major_revision","confidential_remarks":"The skeptical counterexample to Lemma 6.10 appears valid, and the coefficient-modality issue in Theorem 6.12 is also real. These are load-bearing but locally repairable, so I recommend major revision rather than rejection. The sheaf-condition and projective-presentation framework is promising, and the proof that I is simplicial appears to be independent of the broken cohomology lemmas; that part is a strength. I would encourage the author to either formalize the stabilization lemma or give a fully detailed proof, since the sheaf tests depend on it."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nThe 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.\n\nThere 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.\n\nThe 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.","headline":"Genuinely useful presentation framework for topological modalities, but the cohomology descent lemma is false as stated and needs repair.","tokens_in":20704,"tokens_out":6600,"would_cite":true,"duration_ms":62349,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B38","18F10","18F20"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["homotopy type theory","lex modalities","Grothendieck topologies","sheaf conditions","iterated joins","local choice","cohomology","synthetic algebraic geometry"],"falsifier":"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.","tokens_in":19635,"feed_emoji":"🧩","tokens_out":15294,"duration_ms":150110,"temperature":0.7,"pith_summary":"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.","feed_headline":"Internal sheaf tests unlock subuniverses in HoTT","feed_subtitle":"Projective presentations give explicit membership tests, local choice, and vanishing of first cohomology in type theory.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the modality framework, lex-modality stability properties, and truncation preservation used throughout.","marker":"[13]"},{"why":"Gives the join-of-maps fiber identity and image-as-colimit results that underlie the sheaf condition and Lemma 4.6.","marker":"[11]"},{"why":"Fixes the HoTT type-theoretic conventions and univalence axiom for all arguments.","marker":"[14]"},{"why":"Supplies the internal notion of topology that motivates presentations and the synthetic algebraic geometry application.","marker":"[9]"},{"why":"Provides the synthetic algebraic geometry setting and the local choice principle that the paper generalizes to projective presentations.","marker":"[3]"},{"why":"Supplies the triangulated type theory and the simplicial modality whose interval axiom is reproved without extra assumptions.","marker":"[4]"},{"why":"Supplies the duality axiom for classifying toposes of algebraic theories used throughout the applications.","marker":"[1]"},{"why":"Gives the lattice congruence theorem used to prove that the interval is simplicial.","marker":"[6]"},{"why":"Supplies the classifying spaces for abelian groups used to define cohomology in the subuniverse.","marker":"[7]"},{"why":"Provides constructive local-global principles used in the Zariski sheaf proof.","marker":"[8]"}],"fun_headline_variants":["Projective presentations make sheaf conditions explicit","Explicit sheaf tests for HoTT modalities","Local choice from projective presentations in HoTT","Cohomology stability across toposes via sheaf conditions","Presentations internalize Grothendieck topologies for HoTT"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Projective presentations make sheaf conditions explicit","Explicit sheaf tests for HoTT modalities","Local choice from projective presentations in HoTT","Cohomology stability across toposes via sheaf conditions","Presentations internalize Grothendieck topologies for HoTT"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000826,"raw_usage":{"total_tokens":3716,"prompt_tokens":1153,"completion_tokens":2563,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":769,"completion_tokens_details":{"reasoning_tokens":2487}},"tokens_in":769,"tokens_out":2563,"duration_ms":20371,"temperature":1.0,"reasoning_tokens":2487,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-09T21:03:25.209027+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"Moda lities in homotopy type theory","cited_arxiv_id":null,"evidence_quote":"Supplies the modality framework, lex-modality stability properties, and truncation preservation used throughout."},{"cited_title":"Homotopy Type Theory: Univalent Foundations of Mathematics","cited_arxiv_id":null,"evidence_quote":"Fixes the HoTT type-theoretic conventions and univalence axiom for all arguments."},{"cited_title":"Sheaves in Synthetic Algebraic Geometry","cited_arxiv_id":null,"evidence_quote":"Supplies the internal notion of topology that motivates presentations and the synthetic algebraic geometry application."},{"cited_title":"A Foundation for Synthetic Algebraic Geometry","cited_arxiv_id":"2307.00073","evidence_quote":"Provides the synthetic algebraic geometry setting and the local choice principle that the paper generalizes to projective presentations."},{"cited_title":"A General Nullstellensatz for Generalised Spaces","cited_arxiv_id":null,"evidence_quote":"Supplies the duality axiom for classifying toposes of algebraic theories used throughout the applications."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Gives the lattice congruence theorem used to prove that the interval is simplicial."},{"cited_title":"Eilenberg-MacLane s paces in homotopy type theory","cited_arxiv_id":null,"evidence_quote":"Supplies the classifying spaces for abelian groups used to define cohomology in the subuniverse."}],"review_version":1}