3
$\begingroup$

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 $$

$\endgroup$
5
$\begingroup$

$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$.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Isn't the nullary operation a member of $L(0, 1)$ ? $\endgroup$ – Bartosz Milewski 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$ – David Roberts 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$ – Bartosz Milewski Aug 13 '17 at 17:50
2
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.