The B\'enabou-Roubaud theorem via string diagrams

TL;DR

This paper provides a complete, diagrammatic proof of the Bénabou-Roubaud monadic descent theorem, connecting monadic and Grothendieck's perspectives through string diagrams and internal categories.

Contribution

It introduces a novel, graphical proof method for the theorem, unifying different conceptual frameworks using string diagrams and internal-category characterizations.

Findings

Complete proof of the Bénabou-Roubaud theorem using string diagrams

Establishes equivalence between descent data and internal categories

Links monadic and Grothendieck's descent viewpoints

Abstract

We give a complete proof of the B\'enabou-Roubaud monadic descent theorem using the graphical calculus of string diagrams. Our proof links the monadic and Grothendieck's original viewpoint on descent via an internal-category-based characterization of the category of descent data, equivalent to the one of Janelidze and Tholen.