In computer science, a Monad is always an Applicative Functor. It’s regarded as intermediate structure between functors and monads.

And it is the programming equivalent of lax monoidal functors with tensorial strength in category theory. So a Monad in programming is always a lax monoidal functor with tensorial strength.

Exactly how is this possible? What I know about Monad in programming is that they are equivalent to a monad on a ’type category’ which has ’data types’ as objects and ’pure functions’ as morphisms. Since data types can always be seen as a set of values, the type category is like a subcategory of Set. Actually an arbitrary subcategory because languages can support any types as they want.

I got to know that every monad in Set are strong monad, which has tensorial strength by definition. I tried to prove that they eventually form a monoidal functor, but I failed. I could make two different possible candidate for coherence maps from given tensorial strength and costrength, but couldn’t prove that they satisfy the commutation condition for the coherence maps.

The only thing I could find was that strong monads are monoidal monad (and thus monoidal functor) if they are commutative. However, monads are not commmutative in general even in Set. There are many monad which are not commutative in Set, including free monoid monad. (I think they are equivalent to List in programming.)

Just proving that every monad in Set are monoidal functor may not be that hard. I rather want to know more fundamental, or generalizable reason behind that (If exist).

If I’m not wrong, it seems that every monad in Set are indeed monoidal functor even when they are not commutative. What makes this behavior? What makes every monad or strong monad in certain category be always monoidal functor, even when they are not commutative?

I am not a math major and still new to this area. I just got curious about some fundamental things behind tools I have used. I apologize if I said something stupid here.

]]>This question on math.stackexchange piqued my interest. It asks what the monads on a given monoid are. That is, if we treat a monoid as a category with one object we can ask what the monads on that category are. I would have thought that this question would have had an elegant answer, because monads and monoids are both so fundamental. But in fact I can’t find a nice characterisation.

Writing down the definitions we find that a monad on a monoid $X$ is equivalent to “an endomorphism $\theta\colon X\to X$ together with two elements $m,h\in X$ such that:

$\forall x\in X$, $\theta(x)m = m\theta(\theta(x))$,

$\forall x\in X$, $\theta(x)h = hx$,

$m^2 = m\theta(m)$,

$m\theta(h) = mh = 1$.”

Now, in the nice cases when $X$ is a group or commutative, one can prove that $mh=hm=1$ and that $\theta$ is just the inner automorphism given by conjugation by $h$. But in the general case I’m not able to prove that $\theta$ can still only be an inner automorphism. So does anyone know what kind of structure this is?

]]>As far as I can tell, the difference between a monadic functor and a strictly monadic functor boils down to this: a strictly monadic functor $U : \mathcal{D} \to \mathcal{C}$ has the property that, for any object $D$ in $\mathcal{D}$ and any isomorphism $f : C \to U D$ in $\mathcal{C}$, there is a *unique* object $\tilde{C}$ and an (automatically unique) isomorphism $\tilde{f} : \tilde{C} \to D$ such that $U \tilde{f} = f$. Conversely, any monadic functor with this property is strictly monadic. This is very reminiscent of the definition of isofibration, but a monadic isofibration need not be strictly monadic. What’s a good phrase to describe functors like these for which isomorphisms lift uniquely?

- “Creates isomorphisms” on its own might be construed as “conservative”.
- “Isomorphisms lift uniquely” suggests something a little bit stronger than what I’m going for – the unique functor from a group to the terminal category admits unique solutions to the object part of the lifting problem (for obvious reasons) but not the isomorphism part.
- Maybe “strong/strict isofibration”…?

The Eilenberg–Moore construction is essentially a 2-functor from the “2-category of monads on locally small categories” to the “2-category of locally small categories”, modulo certain size issues. In the reverse direction, it is known that any functor $\Phi : \mathcal{C}^\mathbb{S} \to \mathcal{D}^\mathbb{T}$ such that $U^\mathbb{T} \Phi = F U^\mathbb{S}$ for some functor $F : \mathcal{C} \to \mathcal{D}$, where $U^\mathbb{S} : \mathcal{C}^\mathbb{S} \to \mathcal{C}$ and $U^\mathbb{T} : \mathcal{D}^\mathbb{T} \to \mathcal{D}$ are the respective forgetful functors, must come from a unique morphism of monads $\mathbb{S} \to \mathbb{T}$. (This is basically a stronger version of Theorem 6.3 in *Toposes, triples and theories*.) It is also not hard to come up with functors $\mathcal{C}^\mathbb{S} \to \mathcal{D}^\mathbb{T}$ that do *not* arise in this fashion.

But what about the 2-cells? Is every natural transformation between functors induced from a morphism of monads also induced by a 2-cell between the monad morphisms? Clearly, the answer is no – any natural transformation that doesn’t factor through the forgetful functor $U^\mathbb{S}$ can’t be induced by a 2-cell between monad morphisms. But I haven’t been able to come up with a proof or counterexample when I assume that the natural transformation *does* factor through $U^\mathbb{S}$.