Lawvere theory and the Maybe monad

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$.
• Isn't the nullary operation a member of $L(0, 1)$ ? Aug 12 '17 at 21:16
• @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$. Aug 12 '17 at 23:45
• 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$. Aug 13 '17 at 17:50