The Formal Theory of Monads, Univalently

This paper significantly advances the formal theory of monads within the framework of univalent foundations (UF). The central innovation is the development of a formalized treatment of monads that allows for reasoning about them at a high level of abstraction, capturing various kinds of monads within a single, coherent framework. Crucially, the authors formalize and prove that the bicategory of monads is univalent. This means equality between monads in the formalization corresponds to a suitable notion of equivalence, a crucial property in UF.

Key innovations and contributions include:

1. Formalization in UF: Translating Street’s formal theory of monads into univalent foundations using Coq and the UniMath library. This enables the use of homotopy type theory (HoTT) principles like univalence for reasoning about monads.

2. Univalence of the Bicategory of Monads: Demonstrating that the constructed bicategory of monads in UF is univalent. This is crucial for ensuring that the formal notion of equality between monads corresponds to equivalence, allowing for robust reasoning in UF.

3. Eilenberg-Moore Objects: Defining Eilenberg-Moore objects within this framework and showing that both Eilenberg-Moore categories and Kleisli categories give rise to Eilenberg-Moore objects, bridging the gap between these two fundamental constructions.

4. Monads and Adjunctions: Relating monads and adjunctions in arbitrary bicategories, proving both that every adjunction gives rise to a monad, and conversely, under certain conditions, every monad gives rise to an adjunction. This captures the fundamental connection between monads and adjunctions at a high level of generality.

5. Kleisli Categories in UF: Addressing the challenges of defining Kleisli categories in UF, particularly in ensuring univalence, and providing a correct construction based on Rezk completion. The authors prove that in univalent foundations every monad gives rise to an adjunction via the Kleisli category.

Main prior ingredients needed for this work include:

• Bicategory theory: An understanding of bicategories as a generalization of categories, including objects, 1-cells, and 2-cells, along with their composition laws and coherence conditions. Street’s original formal theory of monads relies on this structure.
• Univalent Foundations (HoTT): Familiarity with UF, including the univalence axiom and its consequences, like function extensionality and proof relevance.
• Formalization in Coq: Expertise in using the Coq proof assistant for formalizing mathematical concepts and proving theorems, as the work is implemented using Coq and relies on the UniMath library.
• Eilenberg-Moore categories: Familiarity with Eilenberg-Moore categories (aka the category of algebras for a monad).
• Kleisli categories: Familiarity with Kleisli categories (aka the category of free algebras for a monad).