symmetric monoidal (∞,1)-category of spectra
A strong monad over a monoidal category $V$ is a monad in the bicategory of $V$-actegories.
If $V$ is a monoidal closed category, then a strong monad is the same thing as a $V$-enriched monad.
For $V$ a monoidal category a strong monad over $V$ is a monad
in the $2$-category $V\text{-}Act$ of left $V$-actegories on categories
on the object $V$ itself.
Here we regard $V$ as equipped with the canonical $V$-action on itself.
If we write $\mathbf{B}V$ for the one-object bicategory obtained by delooping $V$ once, we have
where on the right we have the $2$-category of lax 2-functors from $\mathbf{B}V$ to Cat, lax natural transformations of and modifications.
The category $V$ defines a canonical functor $\hat V : \mathbf{B}V \to Cat$.
The strong monad, being a monad in this lax functor bicategory is given by
a lax natural transformation $T : \hat V \to \hat V$;
unit: $\eta : Id_V \Rightarrow T$
product: $\mu : T \circ T \Rightarrow T$
satisfying the usual uniticity and associativity constraints.
By the general logic of $(2,1)$-transformations the components of $T$ are themselves a certain functor.
Then the usual diagrams that specify a strong monad
unitalness and functoriality of the component functor of $T$;
naturalness of unit and product modifications.
A more concrete definition is given in:
and later in
A strong monad over a category $C$ with finite products is a monad $(T, \eta, \mu)$ together with a natural transformation $t_{A,B}$ from $A \times T\;B$ to $T(A\times B)$ subject to three diagrams.
“Strengthening with 1 is irrelevant”:
“Consecutive applications of strength commute”:
“Strength commutes with monad unit and multiplication”:
More generally, if a monoidal category $V$ acts on a category $C$
then a $V$-strength for a monad $T$ on $C$ is a family of morphisms $t_{A,B}:A\bullet T(B)\to T(A\bullet B)$ satisfying similar commutative diagrams.
Moggi proposed the following typing rules for a sequence operator:
To interpret these rules in a category, where types are interpreted as objects and judgements are interpreted as morphisms, we require
For each object $X$, an object $T(X)$;
a morphism $\eta_X:X\to T(X)$ for each $X$ (equivalently, a natural family of functions $C(\Gamma,X)\to C(\Gamma, T(X))$);
a family of functions $*_{\Gamma,\Delta}:C(\Gamma\otimes X, T(Y))\times C(\Delta,T(X))\to C(\Gamma\otimes \Delta,T(Y))$ natural in $\Gamma$ and $\Delta$,
such that
With the subscripts:
Such a structure is the same thing as a strong monad. One way to see this is to notice that it is essentially the same as the Kleisli triple form of an $\hat C$-enriched monad on $C$, where $\hat C$ is the category of presheaves on $C$ regarded with the Day convolution monoidal structure. More concretely,
is a strength map.
(Moggi)
Let $C$ be a category with finite products and let $T$ be a strong monad on $C$. For any points $x:1\to X$, $y:1\to T(Y)$, we have
Hence if $1$ is a generator, i.e. $C(1,-):C\to Set$ is faithful, then there is at most one strength for any ordinary monad on $C$.
In other words, a monad being strong is a property rather than structure in a category with enough points.
Strong monads were defined by Kock, as an alternative description of enriched monads.
Usually strong monads are described explicitly in terms of the components of the above structure. The above repackaging of that definition appears in the blog post
Strong monads are important in Moggi’s theory of notions of computation (see monad (in computer science)):
Last revised on August 15, 2019 at 07:49:07. See the history of this page for a list of all contributions to it.