The Bénabou-Roubaud theorem via string diagrams

Abstract

We give a complete proof of the Bénabou-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.

This article provides a formal and self-contained account of the authors unpublished 2016 note