Pith. sign in

REVIEW 5 major objections 5 minor 7 references

A Foundation for Synthetic Stone Duality

T0 review · 5 major / 5 minor · reviewed 2026-08-11 · deepseek-v4-flash

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

Pith's one-line read Four axioms on top of homotopy type theory yield a synthetic topology for light condensed sets in which all functions are continuous and Brouwer's fixed-point theorem is provable.

desk verdict A genuinely new axiomatic foundation for synthetic topology in HoTT, with real internal theorems, but its validity in the intended model of light condensed sets is conjectured rather than proved. read the letter →

arxiv 2412.03203 v1 pith:B6RWNQDB submitted 2024-12-04 math.LO

Felix Cherubini , Thierry Coquand , Freek Geerligs , Hugo Moeneclaey This is my paper · ORCID
classification math.LO MSC 03B3803F65
keywords homotopytypetheorylightcondensedsetssynthetictopologyStonedualitycompactHausdorffspacesBrouwerfixed-pointtheoremMarkov'sprincipleCechcohomology
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

This paper proposes that homotopy type theory — a formal language in which mathematical objects are types rather than sets — can serve as an internal language for the mathematical universe of light condensed sets, a modern way of building topological spaces out of profinite pieces. To do this, it adds four axioms and shows that they yield a synthetic topology inside the theory: open propositions induce a topology on every type, every function is continuous, and on Stone spaces, second-countable compact Hausdorff spaces, and the unit interval this topology is the classical one. The axioms also imply Markov's principle and LLPO, refute WLPO, and give an internal proof of Brouwer's fixed-point theorem for the disk. If the axioms are true of light condensed sets — which the paper takes as a working assumption and conjecture — then a large part of condensed mathematics and classical topology becomes derivable in one machine-checkable system.

What carries the argument

The key machinery is the type of countably presented Boolean algebras, denoted $\mathrm{Boole}$, together with its spectrum $\mathrm{Sp}(B)$ of Boolean homomorphisms into $2$. The Stone duality axiom — evaluation $B \to 2^{\mathrm{Sp}(B)}$ is an isomorphism — makes $\mathrm{Sp}$ a dual equivalence between $\mathrm{Boole}$ and the type of Stone spaces, so Stone spaces behave as sequential limits of finite sets. The remaining axioms (surjections are formal surjections, local choice, dependent choice) make these spectra interact with arbitrary types the way light condensed sets do. A proposition is open when it is a countable disjunction of decidable propositions, and the collection of open propositions is a dominance: a class of propositions that induces a topology on every type, which is what makes the statement that every function is continuous meaningful. For the cohomological application, the mechanism also includes the first cohomology group $H^1(X,\mathbb{Z})$ defined as maps into the delooping $B\mathbb{Z}$, compared with Cech cohomology of a Stone cover, and localization at the unit interval to run Brouwer's fixed-point argument.

What would settle it

Look in the intended model of light condensed sets for a countably presented Boolean algebra $B$ whose evaluation map $B \to 2^{\mathrm{Sp}(B)}$ is not an isomorphism, or for a surjection of spectra $\mathrm{Sp}(C) \to \mathrm{Sp}(B)$ not induced by an injection $B \to C$. Either would break the first two axioms, and with them the derived theorems on continuity, vanishing of $H^1$, and Brouwer's fixed point as statements about condensed sets. A concrete starting point is the Boolean algebra $B_\infty$ with generators $g_n$ and relations $g_m \wedge g_n = 0$ for $m \neq n$, where the axioms force every map $N_\infty \to 2$ to be represented by an element of the algebra.

Watch

Extended reading notes

Core claim

The paper's central claim is that four axioms on top of homotopy type theory suffice to carry out a synthetic theory of Stone duality and compact Hausdorff spaces in the internal language of light condensed sets. The axioms state that every countably presented Boolean algebra is recovered from its spectrum (Stone duality: evaluation $B \to 2^{\mathrm{Sp}(B)}$ is an isomorphism), that injective algebra maps correspond exactly to surjections of spectra, that local choice holds for Stone spectra, and that dependent choice holds. In this system open propositions form a dominance, so every type carries an intrinsic topology and every function is continuous; on Stone spaces, second-countable compact Hausdorff spaces, and the unit interval this topology is the classical one. The system proves Markov's principle and LLPO, refutes WLPO, identifies Stone spaces with totally disconnected compact Hausdorff spaces, shows $H^1(S,\mathbb{Z})=0$ for Stone spaces and $H^1(X,\mathbb{Z})=\check{H}^1(X,S,\mathbb{Z})$ for compact Hausdorff spaces with a Cech cover, and proves Brouwer's fixed-point theorem internally. The authors state that the validity of the axioms in the light condensed set model is a working assumption and a conjecture, not established in this paper.

Load-bearing premise

The load-bearing premise is that the four axioms are valid statements about the internal logic of light condensed sets; the paper does not prove this and presents it as a working assumption and a conjecture awaiting a constructive justification.

Editorial extensions

If this is right

  • Every function between types is continuous for the induced topology; in particular every map $[0,1] \to [0,1]$ is continuous in the usual epsilon-delta sense (Theorem 5.0.9).
  • The system proves Markov's principle and LLPO and refutes WLPO, so the internal logic of light condensed sets is a specific constructive logic rather than plain intuitionistic logic (Theorems 1.4.1, 1.4.3, 1.4.4).
  • Stone spaces are exactly the totally disconnected compact Hausdorff spaces, and both Stone and compact Hausdorff types are closed under dependent pair types — a statement that needs types, not just sets (Theorem 4.3.7, Lemma 4.2.2).
  • $H^1(S,\mathbb{Z})=0$ for every Stone space; for every compact Hausdorff space with a Cech cover, $H^1(X,\mathbb{Z})$ equals its Cech cohomology; and $H^1([0,1],\mathbb{Z})=0$ (Lemma 6.2.3, Theorem 6.3.5, Proposition 6.4.3).
  • Brouwer's fixed-point theorem holds internally for the disk: every map $D^2 \to D^2$ has a fixed point (Theorem 6.5.10).

Reading between the lines

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

  • Inference: if the completeness conjecture is right, the four axioms could serve as a practical internal calculus for light condensed sets, letting proofs about profinite sets, compact Hausdorff spaces, and cohomology be formalized in homotopy type theory without leaving the axiomatic system.
  • Inference: the exact combination of Markov's principle, LLPO, and the negation of WLPO gives the internal logic a precise place among constructive systems; it is worth testing whether other toposes share this signature, which would show how characteristic the light condensed set model is.
  • Inference: the Cech-cohomology route should extend to higher cohomology groups and to the circle; the paper already notes that a similar computation for $S^1$ would give $H^1(S^1,\mathbb{Z}) = \mathbb{Z}$, opening the way to synthetic degree theory and further fixed-point or invariance theorems.
  • Inference: a concrete next step is to formalize the four axioms together with the proofs of the principles of omniscience, continuity, and Brouwer's theorem in a proof assistant; that would verify the derivation chain even while the model-theoretic justification remains open.
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.

Referee Report

5 major / 5 minor

Summary. The paper develops a synthetic form of Stone duality in homotopy type theory by adjoining four axioms: Stone duality, surjections are formal surjections, local choice, and dependent choice. On this axiomatic basis it proves Markov's principle, LLPO, and the negation of WLPO; introduces a synthetic topology via open and closed propositions; establishes that Stone and compact Hausdorff types have the expected closure properties; shows that every function from the unit interval to itself is continuous in the epsilon-delta sense; and derives a Čech-cohomology comparison theorem leading to an internal proof of Brouwer's fixed-point theorem. The manuscript presents this development as capturing the internal logic of the higher topos of light condensed sets, but it does not prove that the four axioms are valid in that model; the completeness of the axiom system is only conjectured, and the intended justification in a constructive metatheory is left to future work.

Significance. If the four axioms really are valid internally in the topos of light condensed sets, this is a significant contribution: it would give a compact HoTT-level foundation from which strong constructive principles and nontrivial topological and cohomological theorems follow. The paper is honest about its limitations, explicitly records Wärn's example of a non-internally-valid property, and contains many non-formal but plausible proofs. The strongest aspects are the axiomatic derivation of Markov's principle, LLPO and ¬WLPO; the synthetic treatment of Stone and compact Hausdorff spaces; and the use of higher types to prove Brouwer's fixed-point theorem. The main weakness is semantic: the central claim that the axioms hold in light condensed sets is not established, and several compressed arguments (the interval definition, a compactness step in Lemma 4.1.4, and the use of local choice in Lemma 6.2.3) need to be supplied before the reader can fully trust the results. No machine-checked formalization is provided; that is not a defect for a mathematical paper, but it makes these compressed steps more consequential.

major comments (5)
  1. [Introduction and §1.2 (Axiom Local choice)] The paper's central interpretational claim is that the four axioms in §1.2 are internally valid in the topos of light condensed sets. This claim is not proved; the introduction only conjectures completeness and refers to future work [CRS21]. In particular, Local choice is a strong choice principle, and its validity in the intended model is not demonstrated. This is load-bearing: Local choice is used essentially in Lemma 4.2.2 and in Lemma 6.2.3, which underlie Theorem 6.3.5 and Theorem 6.5.10. The authors themselves note (Introduction) that Wärn found a property of light condensed sets that is not internally valid, so internal validity is not automatic. Please either prove validity of Local choice in the intended model or explicitly reframe the paper's theorems as conditional on the four axioms, with the condensed-set interpretation stated as a conjecture.
  2. [§5 (Definitions 5.0.1–5.0.3 and Theorem 5.0.4)] The unit interval I is not formally defined as a type. The text says it can be defined using Cauchy or Dedekind reals and then cites [BB85], but these constructions are not equivalent in general HoTT, and the later theorems—Theorem 5.0.9 and Theorem 6.5.10—depend on the choice. Please specify the exact type constructor used for I, prove or cite that cs : 2^N → I is surjective, and make precise the sense in which the topology on I is generated by open intervals (the step leading to Theorem 5.0.9).
  3. [§4.1, Lemma 4.1.4] The proof of Lemma 4.1.4 asserts 'there is some k : N with ⋁_{n≤k} c_n = 1' from 0 = 1 in B/(c_n)_{n:N}. This is a finiteness/compactness property of countably presented Boolean algebras that is not proved or referenced, and it is not automatic in a constructive metatheory. Lemma 4.1.4 is used in Corollary 4.1.5 and Lemma 4.3.4, so the missing argument is load-bearing. I suggest making this step a separate lemma with a complete proof.
  4. [§6.2, Lemma 6.2.3] The proof of Lemma 6.2.3 is too compressed: 'We use local choice to get T : S → Stone such that ∏_{x:S}||T_x|| with β : ∏_{x:S}(α(x) = ∗)^{T_x}' skips the construction of the family T from α and the verification that local choice applies to the relevant propositional family. Since Lemma 6.2.3 is what yields H^1(S,Z)=0 and enters Theorem 6.3.5, the full construction should be written out.
  5. [§6.5, Theorem 6.5.10] The proof of Brouwer's fixed-point theorem is a sketch. The existence and uniqueness of the intersection point r(x) of the line H_x(t) = f(x) + t·d_x with S^1 is asserted via 'exactly one solution' of a quadratic equation, but the constructive justification is not given, and the verification that the resulting map r : D^2 → S^1 preserves S^1 and is a retraction is only stated. Please expand this proof or supply the missing analytic lemmas with precise references to [BB85].
minor comments (5)
  1. [§6.1, Definition 6.1.1] The formula for d1 has a typo: it reads '+ βx(u,w)' at the end, but the standard coboundary formula requires '+ βx(u,v)'.
  2. [§6.4, Lemma 6.4.2] In the proof, after fixing n as the index of the sequence, the text writes 'α(n) = β(0,1)+...+β(n−1,n)' using n again for a point of I_n; this clashes with the outer n and should be rewritten with a fresh variable.
  3. [§1.1, Lemma 1.1.9] There is a missing closing parenthesis in the statement: 'Sp(2/(αn)n:N' should be 'Sp(2/(αn)n:N)'.
  4. [Introduction] There are a few typos, for example 'Hausforff' should be 'Hausdorff'.
  5. [§5, Lemma 5.0.7] Lemma 5.0.7 is stated without proof; in a constructive setting this deserves at least a one-sentence justification or reference, since it is used to identify open subsets of I with countable unions of open intervals.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper's results are explicit derivations from four stated axioms, not consequences of their own conclusions, and the unproved validity of the axioms in the intended model is a model-correctness gap rather than a circular step.

full rationale

This paper is an axiomatic development in homotopy type theory. The four axioms in Section 1.2 (Stone duality, surjections are formal surjections, local choice, dependent choice) are explicitly stated as assumptions. The main theorems—Markov's principle, LLPO, negation of WLPO, continuity of all functions on the unit interval, H^1(S,Z)=0, and Brouwer's fixed-point theorem—are each proved by internal derivations from these axioms, and none is definitionally identical to an axiom. For example, Theorem 1.4.1 (negation of WLPO) uses Stone duality to represent a function on Cantor space by a finitely generated Boolean element and then derives a contradiction; it does not assume the negation of WLPO. Similarly, the proof of H^1(S,Z)=0 uses local choice to trivialize a BZ-valued map on a Stone cover, but the conclusion is not equivalent to the axiom and the derivation is nontrivial. The paper does cite prior work by some of the same authors: [CCH23] in Remark 1.3.1 for the dual equivalence between Boole and Stone, and [CRS21] in the introduction as a hoped-for constructive metatheoretic justification. The first is a standard categorical consequence of the current Stone duality and surjections axioms and is not itself a premise of the paper's central results; the second is explicitly a conjecture ('we think that this system can be justified'), not a load-bearing proof. The real weakness noted by the paper itself—namely, that the axioms are only conjectured to be valid in the higher topos of light condensed sets, and that David Wärn found an internally invalid property in a related setting—is a model-validity risk and a correctness concern, not a circularity. The derivation chain is self-contained and conditional on the stated axioms, so no circular step can be exhibited.

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

The entire edifice rests on the four axioms, which are asserted to be internally valid in light condensed sets. No consistency proof is supplied; the authors conjecture completeness and defer a constructive justification to future work. The theorems are consequences of these axioms, so their truth for condensed sets is conditional on the axioms holding.

assumptions (5)
  • domain assumption Stone duality: for any countably presented Boolean algebra B, the evaluation map B -> 2^{Sp(B)} is an isomorphism.
    Postulated as internally valid for light condensed sets. Used throughout, e.g., to compute f as a boolean polynomial in Theorem 1.4.1 and to identify Stone spaces with profinite sets.
  • domain assumption Surjections are formal surjections: for g : B -> C in Boole, g is injective iff (.) o g : Sp(C) -> Sp(B) is surjective.
    Used to turn injective Boolean algebra maps into surjective spectrum maps, e.g., to prove LLPO (Theorem 1.4.4) and to show evaluation maps are surjective in Lemma 4.3.6.
  • domain assumption Local choice: for B : Boole and a type family P over Sp(B) with mere inhabitation, there merely exists C : Boole and a surjection q : Sp(C) -> Sp(B) with P(q(t)) for all t.
    Used in Theorem 3.3.1 to express closed sets as images of Stone maps and in Lemma 6.2.3 to trivialize cohomology classes locally.
  • domain assumption Dependent choice: given types E_n with surjections E_{n+1} -> E_n, the projection from the sequential limit lim_k E_k to E_0 is surjective.
    Used to prove properties of overtly discrete types (Lemma 2.0.3) and to support the definition of the unit interval via Cauchy reals in Section 5.
  • standard math HoTT background: univalence and higher inductive types are assumed as the base type theory.
    The whole paper is developed in homotopy type theory; these are the ambient foundational assumptions.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Foundation for Synthetic Stone Duality." pith.science (2026). https://pith.science/paper/B6RWNQDB

@misc{pith2026241203203,
  author       = {Pith},
  title        = {Pith review of: A Foundation for Synthetic Stone Duality},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/B6RWNQDB}},
  note         = {Machine review of arXiv:2412.03203}
}
read the original abstract

The language of homotopy type theory has proved to be appropriate as an internal language for various higher toposes, for example with Synthetic Algebraic Geometry for the Zariski topos. In this paper we apply such techniques to the higher topos corresponding to the light condensed sets of Dustin Clausen and Peter Scholze. This seems to be an appropriate setting to develop synthetic topology, similar to the work of Mart\'in Escard\'o. To reason internally about light condensed sets, we use homotopy type theory extended with 4 axioms. Our axioms are strong enough to prove Markov's principle, LLPO and the negation of WLPO. We also define a type of open propositions, inducing a topology on any type. This leads to a synthetic topological study of (second countable) Stone and compact Hausdorff spaces. Indeed all functions are continuous in the sense that they respect this induced topology, and this topology is as expected for these classes of types. For example, any map from the unit interval to itself is continuous in the usual epsilon-delta sense. We also use the synthetic homotopy theory given by the higher types of homotopy type theory to define and work with cohomology. As an application, we prove Brouwer's fixed-point theorem internally.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

7 extracted references · 5 canonical work pages

  1. [7]

    url: https://arxiv.org/abs/2411.06636 (cit

    arXiv: 2411.06636 [math.CT] . url: https://arxiv.org/abs/2411.06636 (cit. on p. 1). 17

    work page arXiv

  2. [8]

    url: https://doi.org/10.1007/978-3-642-61667- 9 (cit

    doi: 10.1007/978-3-642-61667-9 . url: https://doi.org/10.1007/978-3-642-61667- 9 (cit. on pp. 1, 12, 15, 16). [BC] Reid Barton and Johan Commelin. lean-ctt-snapshot. url: https://github.com/jcommelin/ lean-ctt-snapshot (cit. on pp. 1, 7). [CCH23] Felix Cherubini, Thierry Coquand, and Matthias Hutzler. A Foundation for Synthetic Alge- braic Geometry

    work page doi:10.1007/978-3-642-61667-9

  3. [14]

    Brouwer’s fixed-point theorem in real-co hesive homotopy type theory

    isbn: 978-1-4503-7104-9. doi: 10.1145/3373718.3394801. url: https://doi.org/10.1145/3373718.3394801 (cit. on p. 6). [Shu18] Michael Shulman. “Brouwer’s fixed-point theorem in real-co hesive homotopy type theory”. In: Mathematical Structures in Computer Science 28.6 (2018), pp. 856–941. doi: 10.1017/S0960129517000147 (cit. on p. 2). [W¨ ar23] David W¨ arn. ...

    arXiv 2018

  4. [279]

    Springer-Verlag, Berlin, 1985, pp

    Grundlehren der math- ematischen Wissenschaften. Springer-Verlag, Berlin, 1985, pp. x ii+477. isbn: 3-540-15066-

    work page 1985

  5. [2021]

    Synthetic Topology and Constructive Metric Spaces

    arXiv: 2104.10399 [math.GN] . url: https://arxiv.org/abs/2104.10399 (cit. on pp. 1, 5, 6). [Pro13] The Univalent Foundations Program. Homotopy type theory: Univalent foundations of math- ematics. https://homotopytypetheory.org/book, 2013 (cit. on pp. 1, 2, 3, 12). [RSS20] Egbert Rijke, Michael Shulman, and Bas Spitters. “Modalitie s in homotopy type theor...

    work page Pith review arXiv 2013

  6. [2023]

    Con structive sheaf models of type the- ory

    arXiv: 2307.00073 [math.AG] . url: https://www.felix-cherubini. de/iag.pdf (cit. on pp. 1, 3). [CRS21] Thierry Coquand, Fabian Ruch, and Christian Sattler. “Con structive sheaf models of type the- ory”. In: Math. Struct. Comput. Sci. 31.9 (2021), pp. 979–1002. doi: 10.1017/S0960129521000359. url: https://doi.org/10.1017/S0960129521000359 (cit. on p. 2). [...

    arXiv 2021

  7. [2024]

    On internally projective sheaves of groups

    arXiv: 2409.12835 [math.CT] . url: https://arxiv.org/abs/2409.12835 (cit. on p. 2). [Wei24] Niels van der Weide. The internal languages of univalent categories

    work page Pith review arXiv

Pith tools

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