The Formal Theory of Monads, Univalently
Niels van der Weide
TL;DR
This work advances the formal theory of monads by embedding Street’s framework into univalent foundations, allowing monads to be studied internally to arbitrary bicategories. It constructs the bicategory of monads $\mathsf{Mnd}(\mathsf{B})$, proves its univalence when $\mathsf{B}$ is univalent, and develops Eilenberg-Moore objects, Kleisli objects, and the adjunction–monad correspondence within this setting. The authors provide systematic constructions via displayed bicategories, demonstrate numerous examples across bicategories of categories and enriched structures, and establish equivalent formulations of universality and monadicity using EM-cones and Kleisli objects. The formalization in Coq/UniMath demonstrates practical applicability to a broad range of semantic settings, including linear logic and enriched category theory, with clear avenues for extension. This univalent framework simplifies and unifies proofs by allowing induction on adjoint equivalences and leveraging Rezk completion for univalence in Kleisli constructions.
Abstract
We develop the formal theory of monads, as established by Street, in univalent foundations. This allows us to formally reason about various kinds of monads on the right level of abstraction. In particular, we define the bicategory of monads internal to a bicategory, and prove that it is univalent. We also define Eilenberg-Moore objects, and we show that both Eilenberg-Moore categories and Kleisli categories give rise to Eilenberg-Moore objects. Finally, we relate monads and adjunctions in arbitrary bicategories. Our work is formalized in Coq using the UniMath library.