The 2-Adjunction that relates Universal Arrows and Extensive Monads

TL;DR

This paper constructs an explicit 2-adjunction between the 2-category of universal arrows $ extbf{UArr}( ext{Cat})$ and the 2-category of extensive monads $ extbf{EMnd}( ext{Cat})$, mirroring the classical adjunction–monad correspondence. It introduces a left 2-functor $oldsymbol{ ext{Φ}}$ that sends universal arrows to extensive monads and a right 2-functor $oldsymbol{ ext{Ψ}}$ in the opposite direction, together with a unit $oldsymbol{ ext{η}}^{oldsymbol{ ext{ΨΦ}}}$ and a counit $oldsymbol{ ext{ε}}^{oldsymbol{ ext{ΦΨ}}}$ establishing a 2-adjunction. The work also proves isomorphisms between $ extbf{UArr}( ext{Cat})$ and $ extbf{Adj}_{R}( ext{Cat})$ and between $ extbf{EMnd}( ext{Cat})$ and $ extbf{Mnd}_{E}( ext{Cat})$, and discusses its relevance for higher order theories and potential extensions to Gray-categories and pseudo adjunctions. It provides a detailed 2-categorical framework that can serve as a foundation for both theoretical developments in higher category theory and practical tools for reasoning about extensive monads in computer science.

Abstract

In this article the 2-adjunction that relates universal arrows and extensive monads is constructed explicitly. This 2-adjunction resembles the one that relates adjunctions and monads since the 2-category of universal arrows is isomorphic to the 2-category of adjunctions and the 2-category of extensive monads is isomorphic to the 2-category of monads. This article would be useful as a foundation for a theory relating pseudo adjunctions and pseudo monads for Gray-categories. On the other hand, it might function as an accesible tool for computer scientists on extensive monads.

Theorems & Definitions (20)

• Definition 2.1.1
• Proposition 2.4.1
• Lemma 3.5.1
• Lemma 3.5.2
• Proposition 3.5.3
• Proposition 4.1.1
• Proposition 4.2.1
• Proposition 4.2.2
• Proposition 4.3.1
• Proposition 4.3.2