Demystifying Codensity Monads via Duality
Fabian Lenke, Nico Wittrock, Stefan Milius, Henning Urbat
TL;DR
The paper addresses the problem of understanding and systematizing codensity presentations of monads by introducing a duality-based density framework. It proves a general theorem showing that in a codensity setting the induced monad is isomorphic to the codensity monad of a presenting functor, reducing codensity proofs to density arguments. The work unifies and extends numerous known presentations (e.g., ultrafilter, Vietoris, and various probability monads) and yields new codensity presentations for the filter monads, the lower Vietoris monad, and the expectation monad, among others. This framework clarifies structural connections across logic, denotational semantics, topology, and probability, and points to broad applicability and future extensions to higher-categorical monad theory and additional monads.
Abstract
Codensity monads provide a universal method to generate complex monads from simple functors. Recently, a wide range of important monads in logic, denotational semantics, and probabilistic computation, such as several incarnations of the ultrafilter monad, the Vietoris monad, and the Giry monad, have been presented as codensity monads, using complex arguments. We propose a unifying categorical approach to codensity presentations of monads, based on the idea of relating the presenting functor to a dense functor via a suitable duality between categories. We prove a general presentation result applying to every such situation and demonstrate that most codensity presentations known in the literature emerge from this strikingly simple duality-based setup, drastically alleviating the complexity of their proofs and in many cases completely reducing them to standard duality results. Additionally, we derive a number of novel codensity presentations using our framework, including the first non-trivial codensity presentations for the filter monads on sets and topological spaces, the lower Vietoris monad on topological spaces, and the expectation monad on sets.