The Formal Theory of Monads, Univalently

TL;DR

This paper formalizes the theory of monads within univalent foundations, enabling rigorous reasoning about monads and their structures in a higher-level abstract setting, with all results verified in Coq.

Contribution

It extends the formal theory of monads to univalent foundations, defining bicategories of monads, Eilenberg-Moore objects, and relating monads to adjunctions within this framework.

Findings

Bicategory of monads is univalent.

Eilenberg-Moore and Kleisli categories give rise to Eilenberg-Moore objects.

Formalization achieved in Coq using UniMath.

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.