Samskeiða einöld í 2-ríkjum

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. This interaction allows parallel composition to be modeled in the monad's Kleisli category. In this thesis, we begin by a short recap of monads and resolutions and then move onto ordered category theory and 2-category theory. Monoidal categories are also introduced and finally ordered monoidal categories, concurrent categories and concurrent monads. As the main observation, we introduce a 2-category whose internal monads are exactly concurrent monads. But the Kleisli adjunctions of the underlying monads of concurrent monads are not internal adjunctions in this 2-category. We define a more accommodating 2-category where they are. Most of the content of this thesis is formalized in Agda, including the proof that concurrent monads can be recovered from concurrent categories and that the State monad is a concurrent monad.