Stone Duality for Monads

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 left adjoint takes a monad T-viewed as a notion of computation, following Moggi-to its localic behaviour category LBT. 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 LC-similarly understood as a transition system-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 of this adjunction consist of (i) hyperaffine-unary monads, i.e., those monads where term t admits a read-only operation 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.