The Maybe
monad is based on the endofunctor $ + 1$ (coproduct with the singleton set). Its Lawvere theory $L$ is supposed to be generated by one nullary operation (see Plotkin and Power), raise
. How do I show that the Maybe
monad is generated from this Lawvere theory using the coend formula:
$$
T a = \int^n L(n, 1)\times a^n
$$
$L(n,1)$ consists of the $n$ projection operations $p_i$ and the additional nullary operation $c$. So a typical element of $L(n,1)\times a^n$ has one of the two forms $(p_i;x_1,\dots,x_n)$ or $(c;x_1,\dots,x_n)$. Th coend consists of the disjoint union of all these sets (over all $n$) modulo some identifications. When you work out those identifications, you should find that $(p_i;x_1,\dots,x_n)$ gets identified with $(p_j;y_1,\dots,y_n)$ when $x_i=y_j$, and that $(c;x_1,\dots,x_n)$ gets identified with $(c;y_1,\dots,y_n)$ regardless of the $x$'s and $y$'s. So elements of the coend arising from $(p_i;x_1,\dots,x_n)$ can be regarded as just the corresponding elements $x_i$ of $a$, while those arising from $(c;x_1,\dots,x_n)$ can be regarded as one extra element. In other words, you get $a+1$.

$\begingroup$ Isn't the nullary operation a member of $L(0, 1)$ ? $\endgroup$ Aug 12 '17 at 21:16

$\begingroup$ @BartoszMilewski yes, but you need all compositions with the nullary operation, so in general you have have maps $a^n \to a^m$ such that some of the components $a^n\to a$ factor as $a^n \to a^0 \stackrel{c}{\to} a$. $\endgroup$ Aug 12 '17 at 23:45

$\begingroup$ So, after all identifications, we are left with a bunch of disjoint subsets of $a$, which sum up to $a$, and one singleton set. This makes sense. An even simpler case is the identity monad, in which case we only have the disjoint subsets summing up to $a$. $\endgroup$ Aug 13 '17 at 17:50
That follows from the general construction that associates a monad to a Lawvere theory.
If memory serves well you can find the details of this construction on this paper by Hyland and Power.
Hope this helps.