Concurrent monads as internal monads and their internal resolutions
Bjarki Gunnarsson
University of Iceland
Abstract:
Concurrent monads on ordered monoidal categories were recently defined by Rivas and Uustalu. The concurrent monads of Rivas and Uustalu are lax-monoidal functors whose monoidality interacts the structure of the monad, akin to lax-monoidal monads. The Kleisli categories of concurrent monads can be used to model parallel composition with effects. I have been working on formalizing results around concurrent monads in Agda, and am going to cover how a transport hell issue was solved. Additionally, concurrent monads turn out to be exactly the internal monads in a certain 2-category, similar to MonCat_ell. I'll talk about the „monoidal“ resolution of concurrent monads, and how this resolution can fit in a slightly bigger 2-category.