pith. sign in

arxiv: 2603.25710 · v2 · pith:B6COR6AFnew · submitted 2026-03-26 · 💻 cs.LO · cs.PL· math.CT

Stone Duality for Monads

Richard Garner , Alyssa Renata , Nicolas Wu This is my paper

Pith reviewed 2026-05-21 10:26 UTC · model grok-4.3

classification 💻 cs.LO cs.PLmath.CT
keywords Stone dualitymonadslocalesadjunctionhyperaffine-unary monadslocalic categoriestransition systemsretrofunctors
0
0 comments X

The pith

A contravariant idempotent adjunction between ranked monads on sets and localic internal categories gives a Stone duality whose fixed points are hyperaffine-unary monads and ample localic categories.

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

The paper constructs a contravariant idempotent adjunction between the category of ranked monads on sets and the category of internal categories with internal retrofunctors in locales. One direction sends each monad to its localic behaviour category, the universal transition system for interacting with the monad's computations. The other direction sends each localic category to a monad whose elements are A-indexed families of local sections to the source map that jointly partition the locale of objects. The fixed points of the adjunction are the hyperaffine-unary monads, in which every term admits a read-only operation predicting its output, and the ample localic categories, whose source maps are local homeomorphisms and whose object locales are strongly zero-dimensional. The equivalence further restricts to classical Stone duality when Boolean algebras are viewed as monads of partitions and their Stone spaces as localic categories with only identity morphisms.

Core claim

We introduce a contravariant idempotent adjunction between ranked monads on Set and internal categories and internal retrofunctors in locales. The left adjoint takes a monad T to its localic behaviour category LB T, understood as the universal transition system for interacting with T. The right adjoint takes a localic category LC to the monad Γ LC where (Γ LC) A is the set of A-indexed families of local sections to the source map which jointly partition the locale of objects. The fixed points consist of hyperaffine-unary monads, where term t admits a read-only operation t-bar predicting the output of t, and ample localic categories whose source maps are local homeomorphisms and whose locale,

What carries the argument

The localic behaviour category LB T of a monad T, serving as the universal transition system for computations given by the monad.

If this is right

  • Hyperaffine-unary monads are exactly those whose Eilenberg-Moore categories are Cartesian closed.
  • The duality translates notions of computation given by monads into spatial transition systems given by localic categories.
  • Boolean algebras viewed as monads of partitions correspond to Stone spaces viewed as localic categories with only identity morphisms.
  • Ample localic categories provide canonical models for the transition behaviour of hyperaffine-unary monads.

Where Pith is reading between the lines

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

  • Properties of hyperaffine-unary monads could be derived from geometric features of their dual ample localic categories.
  • The construction might extend from sets to other base categories such as toposes to produce analogous dualities.
  • Monads used in programming semantics for effects could be classified by whether they satisfy the hyperaffine-unary condition.
  • The duality opens a route to study computational effects through invariants of localic categories.

Load-bearing premise

The localic behaviour category must function as the universal transition system for every monad and the families of local sections from the right adjoint must partition the object locale for the adjunction and its fixed points to hold.

What would settle it

A concrete ranked monad T that is hyperaffine-unary but whose localic behaviour category LB T does not recover T under the right adjoint would falsify the idempotence of the adjunction.

Figures

Figures reproduced from arXiv: 2603.25710 by Alyssa Renata, Nicolas Wu, Richard Garner.

Figure 1
Figure 1. Figure 1: The Stone Adjunctions are the comodels of Power and Shkaravska [27]. For a monad T, a T-comodel (W,L−M) in a category C consists of an object of states W ∈ C along with a cointerpretation LtM: W → P a∈A W for each computation t ∈ T A, subject to compatibility with the monad structure of T. We think of LtM for t ∈ T A as a transition on W which along the way also produces a return value in the set A. A good… view at source ↗
read the original abstract

We introduce a contravariant idempotent adjunction between (i) the category of ranked monads on $\mathsf{Set}$; and (ii) the category of internal categories and internal retrofunctors in the category of locales. The left adjoint takes a monad $T$-viewed as a notion of computation, following Moggi-to its localic behaviour category $\mathsf{LB}T$. This behaviour category is understood as "the universal transition system" for interacting with $T$: its "objects" are states and the "morphisms" are transitions. On the other hand, the right adjoint takes a localic category $\mathsf{LC}$-similarly understood as a transition system-to the monad $\Gamma\mathsf{LC}$ where $(\Gamma\mathsf{LC})A$ is the set of $A$-indexed families of local sections to the source map which jointly partition the locale of objects. The fixed points of this adjunction consist of (i) hyperaffine-unary monads, i.e., those monads where term $t$ admits a read-only operation $\bar{t}$ predicting the output of $t$; and (ii) ample localic categories, i.e., whose source maps are local homeomorphisms and whose locale of objects are strongly zero-dimensional. The hyperaffine-unary monads arise in earlier works by Johnstone and Garner as a syntactic characterization of those monads with Cartesian closed Eilenberg-Moore categories. This equivalence is the Stone duality for monads; so-called because it further restricts to the classical Stone duality by viewing a Boolean algebra $B$ as a monad of $B$-partitions and the corresponding Stone space as a localic category with only identity morphisms.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 3 minor

Summary. The manuscript introduces a contravariant idempotent adjunction between the category of ranked monads on Set and the category of internal categories equipped with internal retrofunctors in the category of locales. The left adjoint sends a monad T to its localic behaviour category LB T, constructed as the universal transition system whose objects are states and morphisms are transitions compatible with T. The right adjoint sends a localic category LC to the monad Gamma LC whose value on A is the set of A-indexed families of local sections of the source map that jointly partition the locale of objects. The fixed points are precisely the hyperaffine-unary monads (those admitting read-only predictor operations bar t for each term t) and the ample localic categories (those whose source maps are local homeomorphisms and whose object locales are strongly zero-dimensional). The duality further restricts to classical Stone duality by viewing Boolean algebras as partition monads and Stone spaces as localic categories with only identity morphisms, and it recovers the Johnstone-Garner characterization of monads with Cartesian closed Eilenberg-Moore categories.

Significance. If the adjunction and fixed-point characterization are verified, the result supplies a geometric duality that interprets computational monads in terms of localic transition systems and conversely, extending classical Stone duality while connecting directly to existing syntactic characterizations of hyperaffine-unary monads. The construction is parameter-free once the ranked monad and localic category data are fixed, and the restriction to partition monads and Stone spaces provides an immediate consistency check with established results. This could prove useful for transferring results between monad semantics and locale-theoretic geometry, particularly for questions about Cartesian closed algebras.

major comments (2)
  1. [§4] §4, construction of LB T: the universal property of the localic behaviour category as the free transition system for T is load-bearing for the left-adjoint claim, yet the verification that every T-compatible transition system factors uniquely through LB T is only sketched; an explicit diagram chase showing how the monad multiplication interacts with the locale morphisms would strengthen the argument.
  2. [§5.1] §5.1, definition of Gamma LC: the assertion that the A-indexed local sections jointly partition the object locale is used to prove that Gamma LC is a monad and that the adjunction is idempotent, but the proof that this partition condition is preserved under composition of retrofunctors relies on the strongly zero-dimensional assumption without an intermediate lemma; this step is central to identifying the fixed points as ample categories.
minor comments (3)
  1. The notion of 'ranked monad' is introduced without a self-contained definition or comparison to ordinary monads; a short paragraph or reference to the precise extra structure required for LB T to be well-defined would aid readers.
  2. [Figure 2] Figure 2 (the diagram of the adjunction unit and counit) uses locale-theoretic notation that is not fully explained in the caption; adding a sentence clarifying the meaning of the double arrow for retrofunctors would improve clarity.
  3. [Abstract] The abstract states that the fixed points 'consist of' the two classes, but the body only proves one inclusion explicitly; the converse inclusion (every hyperaffine-unary monad arises as Gamma LB T) should be cross-referenced to the relevant proposition for easier navigation.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading, positive evaluation, and recommendation of minor revision. The two major comments identify places where additional detail would strengthen the exposition of the adjunction and its fixed-point characterization. We address each point below and will incorporate the suggested clarifications.

read point-by-point responses

  1. Referee: [§4] §4, construction of LB T: the universal property of the localic behaviour category as the free transition system for T is load-bearing for the left-adjoint claim, yet the verification that every T-compatible transition system factors uniquely through LB T is only sketched; an explicit diagram chase showing how the monad multiplication interacts with the locale morphisms would strengthen the argument.

    Authors: We agree that the verification of the universal property for LB T in §4 is presented in outline form and would be improved by an explicit diagram chase. In the revised manuscript we will expand the relevant subsection to include a detailed commutative diagram that tracks the interaction of the monad multiplication μ with the locale morphisms arising from a T-compatible transition system, thereby making the unique factorization fully rigorous. revision: yes

  2. Referee: [§5.1] §5.1, definition of Gamma LC: the assertion that the A-indexed local sections jointly partition the object locale is used to prove that Gamma LC is a monad and that the adjunction is idempotent, but the proof that this partition condition is preserved under composition of retrofunctors relies on the strongly zero-dimensional assumption without an intermediate lemma; this step is central to identifying the fixed points as ample categories.

    Authors: We accept that the argument in §5.1 for preservation of the joint-partition condition under retrofunctor composition would benefit from an explicit intermediate lemma. The revised version will insert a new lemma immediately preceding the relevant proposition; the lemma will isolate the preservation step and invoke the strongly zero-dimensional hypothesis on the object locale in a self-contained manner, thereby clarifying the identification of the fixed points as ample localic categories. revision: yes

Circularity Check

0 steps flagged

No significant circularity in the derivation chain

full rationale

The paper constructs a contravariant idempotent adjunction between ranked monads on Set and internal categories/retrofunctors in locales, defining the left adjoint LB T explicitly as the universal transition system for a monad T and the right adjoint Gamma LC as the monad of A-indexed partitioning local sections. Fixed points are identified with hyperaffine-unary monads (defined via read-only predictors bar t) and ample localic categories (source maps as local homeomorphisms, strongly zero-dimensional objects), with the hyperaffine-unary class explicitly referenced to independent prior characterizations in works by Johnstone and Garner as monads with Cartesian closed Eilenberg-Moore categories. The further restriction to classical Stone duality via partition monads and Stone spaces is presented as a special case of the same construction. No load-bearing step reduces by the paper's equations or self-citation to a definitional tautology or fitted input; the central claims remain independently motivated and externally aligned.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The result rests on standard background from category theory, locale theory, and monad theory. No free parameters or invented entities are visible in the abstract; the constructions are defined in terms of existing categorical notions.

axioms (2)
  • standard math Existence and basic properties of the category of ranked monads on Set and the category of internal categories and retrofunctors in locales.
    Invoked when the adjunction is stated between these two categories.
  • standard math The locale-theoretic notions of local homeomorphism and strongly zero-dimensional locale.
    Used to define ample localic categories.

pith-pipeline@v0.9.0 · 5842 in / 1529 out tokens · 40138 ms · 2026-05-21T10:26:18.754194+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

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

  • IndisputableMonolith/Foundation/RealityFromDistinction.lean reality_from_one_distinction unclear
    ?
    unclear

    Relation between the paper passage and the cited Recognition theorem.

    We introduce a contravariant idempotent adjunction between (i) the category of ranked monads on Set; and (ii) the category of internal categories and internal retrofunctors in the category of locales. ... The fixed points ... are hyperaffine-unary monads ... and ample localic categories ... This equivalence is the Stone duality for monads.

  • IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear
    ?
    unclear

    Relation between the paper passage and the cited Recognition theorem.

    The sheaf of transitions FT ... quotient of the free BJ-set T1[B]J ... by the smallest BJ-congruence identifying t> >=u ≈ P(t)(λ[t↦→a].t> >u(a))

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

31 extracted references · 31 canonical work pages · 1 internal anchor

  1. [1]

    Aguiar, M.,Internal Categories and Quantum Groups, Cornell University (1997)

    work page 1997

  2. [2]

    Ahman, D. and A. Bauer,Runners in Action, pages 29–55, Lecture notes in computer science, Springer International Publishing (2020). https://doi.org/10.1007/978-3-030-44914-8_2

    work page doi:10.1007/978-3-030-44914-8_2 2020

  3. [3]

    Ahman, D. and T. Uustalu,Directed containers as categories, Electronic Proceedings in Theoretical Computer Science 207, pages 89–98 (2016). https://doi.org/10.4204/eptcs.207.5

    work page doi:10.4204/eptcs.207.5 2016

  4. [4]

    Ahman, D. and T. Uustalu,Taking updates seriously, in: R. Eramo and M. Johnson, editors,Proceedings of the Sixth International Workshop on Bidirectional Transformations, pages 59–73, CEUR Workshop Proceedings (2017)

    work page 2017

  5. [5]

    Chapman and T

    Altenkirch, T., J. Chapman and T. Uustalu,Monads need not be endofunctors, in: C. L. Ong, editor,Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 601...

    work page doi:10.1007/978-3-642-12032-9_21 2010

  6. [6]

    M.,Actions of boolean rings on sets, Algebra universalis28, pages 153–187 (1991)

    Bergman, G. M.,Actions of boolean rings on sets, Algebra universalis28, pages 153–187 (1991). https://doi.org/10.1007/bf01190851

    work page doi:10.1007/bf01190851 1991

  7. [7]

    Clarke, B.,Internal split opfibrations and cofunctors, Theory and Applications of Categories35, pages 1608–1633 (2020)

    work page 2020

  8. [8]

    Cockett, R. and R. Garner,Generalising the ´ etale groupoid–complete pseudogroup correspondence, Advances in mathematics 392, page 108030 (2021). https://doi.org/10.1016/j.aim.2021.108030

    work page doi:10.1016/j.aim.2021.108030 2021

  9. [9]

    C.,The bicategory of topoi and spectra, Reprints in Theory and Applications of Categories25, pages 1–16 (2016)

    Cole, J. C.,The bicategory of topoi and spectra, Reprints in Theory and Applications of Categories25, pages 1–16 (2016)

    work page 2016

  10. [10]

    https://doi.org/10.1017/s0960129521000219

    Garner, R.,The costructure–cosemantics adjunction for comodels for computational effects, Mathematical structures in computer science32, pages 374–419 (2022). https://doi.org/10.1017/s0960129521000219

    work page doi:10.1017/s0960129521000219 2022

  11. [11]

    https://doi.org/10.46298/lmcs-19(1:2)2023

    Garner, R.,Stream processors and comodels, Logical Methods in Computer Science19, Issue 1(2023). https://doi.org/10.46298/lmcs-19(1:2)2023

    work page doi:10.46298/lmcs-19(1:2)2023 2023

  12. [12]

    https://doi.org/10.1007/s00012-024-00869-1

    Garner, R.,Cartesian closed varieties I: the classification theorem, Algebra universalis85(2024). https://doi.org/10.1007/s00012-024-00869-1

    work page doi:10.1007/s00012-024-00869-1 2024

  13. [13]

    https://doi.org/10.1017/prm.2024.80

    Garner, R.,Cartesian closed varieties II: links to algebra and self-similarity, Proceedings of the Royal Society of Edinburgh: Section A Mathematics pages 1–45 (2025). https://doi.org/10.1017/prm.2024.80

    work page doi:10.1017/prm.2024.80 2025

  14. [14]

    Goncharov, S. and L. Schr¨ oder,A relatively complete generic hoare logic for order-enriched effects, in:2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE (2013). https://doi.org/10.1109/lics.2013.33

    work page doi:10.1109/lics.2013.33 2013

  15. [15]

    Kozen and J

    Harel, D., D. Kozen and J. Tiuryn,Dynamic logic, pages 99–217, Springer Netherlands (2001). https://doi.org/10.1007/978-94-017-0456-4_2

    work page doi:10.1007/978-94-017-0456-4_2 2001

  16. [16]

    https://doi.org/10.1016/s0022-4049(96)00165-x

    Johnstone, P.,Cartesian monads on toposes, Journal of pure and applied algebra116, pages 199–220 (1997). https://doi.org/10.1016/s0022-4049(96)00165-x

    work page doi:10.1016/s0022-4049(96)00165-x 1997

  17. [17]

    T.,Stone Spaces, Cambridge University Press (1982)

    Johnstone, P. T.,Stone Spaces, Cambridge University Press (1982)

    work page 1982

  18. [18]

    T.,Collapsed toposes and cartesian closed varieties, Journal of algebra129, pages 446–480 (1990)

    Johnstone, P. T.,Collapsed toposes and cartesian closed varieties, Journal of algebra129, pages 446–480 (1990). https://doi.org/10.1016/0021-8693(90)90230-l

    work page doi:10.1016/0021-8693(90)90230-l 1990

  19. [19]

    T.,Sketches of an Elephant: Volume 2, Oxford University Press (2002)

    Johnstone, P. T.,Sketches of an Elephant: Volume 2, Oxford University Press (2002)

    work page 2002

  20. [20]

    Rivas and T

    Katsumata, S.-Y., E. Rivas and T. Uustalu,Interaction laws of monads and comonads, in:Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, ACM (2020). https://doi.org/10.1145/3373718.3394808

    work page doi:10.1145/3373718.3394808 2020

  21. [21]

    Kelly, G. M. and A. J. Power,Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads, Journal of Pure and Applied Algebra89, pages 163–179 (1993). https://doi.org/10.1016/0022-4049(93)90092-8 16 Garner, Renata, Wu

    work page doi:10.1016/0022-4049(93)90092-8 1993

  22. [22]

    https://doi.org/10.1016/0890-5401(91)90052-4

    Moggi, E.,Notions of computation and monads, Information and Computation93, pages 55–92 (1991). https://doi.org/10.1016/0890-5401(91)90052-4

    work page doi:10.1016/0890-5401(91)90052-4 1991

  23. [23]

    Niu, N. and D. I. Spivak,Polynomial Functors: A Mathematical Theory of Interaction, London Mathematical Society Lecture Note Series, Cambridge University Press (2025)

    work page 2025

  24. [24]

    Paterson, A. L. T.,Groupoids, inverse semigroups, and their operator algebras, volume 170 ofProgress in Mathematics, Birkh¨ auser (1999)

    work page 1999

  25. [25]

    Plotkin, G. and J. Power,Notions of Computation Determine Monads, pages 342–356, Lecture notes in computer science, Springer Berlin Heidelberg (2002). https://doi.org/10.1007/3-540-45931-6_24

    work page doi:10.1007/3-540-45931-6_24 2002

  26. [26]

    Plotkin, G. and J. Power,Computational effects and operations: An overview, Electronic Notes in Theoretical Computer Science73, pages 149–163 (2004). https://doi.org/10.1016/j.entcs.2004.08.008

    work page doi:10.1016/j.entcs.2004.08.008 2004

  27. [27]

    Power, J. and O. Shkaravska,From comodels to coalgebras: State and arrays, Electronic notes in theoretical computer science106, pages 297–314 (2004). https://doi.org/10.1016/j.entcs.2004.02.041

    work page doi:10.1016/j.entcs.2004.02.041 2004

  28. [28]

    https://doi.org/10.1016/j.entcs.2015.12.024

    Uustalu, T.,Stateful runners of effectful computations, Electronic notes in theoretical computer science319, pages 403–421 (2015). https://doi.org/10.1016/j.entcs.2015.12.024

    work page doi:10.1016/j.entcs.2015.12.024 2015

  29. [29]

    Uustalu, T. and N. Voorneveld,Algebraic and Coalgebraic Perspectives on Interaction Laws, pages 186–205, Lecture notes in computer science, Springer International Publishing (2020). https://doi.org/10.1007/978-3-030-64437-6_10

    work page doi:10.1007/978-3-030-64437-6_10 2020

  30. [30]

    Van Name, J.,Ultraparacompactness and ultranormality, arXiv:1306.6086v1 [math.GN] (2013)

    work page internal anchor Pith review Pith/arXiv arXiv 2013

  31. [31]

    Vickers, S.,Topology via Logic, Cambridge University Press (1996). 17 Garner, Renata, Wu A Omitted Proofs A.1 Proof of lemma 2.18 Each open ˆx=λy.⋁{b|x≡by}is aBJ-set homomorphism since ify 1≡cy2 then c∧ˆx(y1) = ⋁ {c∧b|x≡by1}3= ⋁ {c∧b|x≡c∧by1}= ⋁ {c∧b|x≡c∧by2}=c∧ˆx(y2), where 3 holds from right-to-left because we can take the b on the LHS to be the b∧con t...

    work page 1996