Strong monads and premonoidal categories play a central role in clarifying the denotational semantics of effectful programming languages. Unfortunately, this theory excludes many modern semantic models in which the associativity and unit laws only hold up to coherent isomorphism: for instance, because composition is defined using a universal property. This paper remedies the situation. We define premonoidal bicategories and a notion of strength for pseudomonads, and show that the Kleisli bicategory of a strong pseudomonad is premonoidal. As often in 2-dimensional category theory, the main difficulty is to find the correct coherence axioms on 2-cells. We therefore justify our definitions with numerous examples and by proving a correspondence theorem between actions and strengths, generalizing a well-known category-theoretic result.
翻译:强幺半群和拟幺半范畴在阐明带效应编程语言的指称语义中扮演着核心角色。遗憾的是,该理论排除了许多现代语义模型,其中结合律和单位律仅保持至相干同构:例如,因为组合是通过泛性质定义的。本文解决了这个问题。我们定义了拟幺半双范畴以及伪幺半群上的强度概念,并证明了强伪幺半群的Kleisli双范畴是拟幺半的。如同二维范畴论中常见的情况,主要难点在于为2-胞元找到正确的相干公理。因此,我们通过大量例子以及证明作用与强度之间的对应定理(推广了一个众所周知的范畴论结果)来论证我们的定义。