The (Relative) Monad–Theory Correspondence
University of Cambridge
Abstract:
It has long been known that the two classical approaches to categorical algebra – one employing algebraic theories, and the other employing monads – are equivalent. More precisely, the category of algebraic theories is equivalent to the category of finitary monads on the category of sets, and the models for a given algebraic theory coincide with the algebras for the corresponding monad. It is also known that this relationship admits vast generalisations: throughout the last fifty years, there have been abundant variations on the notion of theory, and correspondences have been established with appropriate classes of monads. Most recently, Lucyshyn-Wright, and Bourke and Garner have given general monad–theory correspondences that subsume many of those previously appearing in the literature. However, despite the proliferation of literature regarding the monad–theory correspondence, it remains an enigmatic phenomenon. In other words, it is not clear why the correspondence should exist at all.
I will present a new perspective on the monad–theory correspondence that illuminates its true nature. The essential insight is that theories correspond precisely to relative monads via the Kleisli construction. Relative monads may then, in well-behaved circumstances, be extended to monads with the same categories of algebras. Having sketched out a new proof of the monad–theory correspondence in this light, I will then show how several of the constructions that have arisen in the study of theories and monads, such as the definition of the category of models for a theory, and the structure–semantics adjunction, are elucidated by this understanding. In doing so, I will answer the question: ``If theories correspond to relative monads via the Kleisli construction, what concept corresponds to relative monads via the Eilenberg–Moore construction?''
This is a report on joint work with Dylan McDermott.