# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeFeb 12th 2014

a stubby minimum at maybe monad

(we are talking about it in the other thread, but for completeness I suppose I should start a new thread for it here)

• CommentRowNumber2.
• CommentAuthorDavid_Corfield
• CommentTimeFeb 12th 2014

Isn’t that function in the Keisli category a partial function? What was all that about restriction categories, Cockett and Lack’s work?

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeFeb 12th 2014

Isn’t that function in the Keisli category a partial function?

What was all that about restriction categories, Cockett and Lack’s work?

Dunno, maybe you can tell me?

• CommentRowNumber4.
• CommentAuthorDavid_Corfield
• CommentTimeFeb 12th 2014

Since Steve Lack wrote three papers on them, there should be something important about them.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeFeb 12th 2014

Thanks. Maybe I find the time to look at that later. For the moment I have put those pointers here

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeFeb 12th 2014
• (edited Feb 12th 2014)

Over in the thread on partial functions I had wondered if and then Todd and Zhen Lin kindly confirmed and provided details for the neat little statement that the smash product on pointed objects is indeed the canonical tensor product induced by the monoidalness of the maybe monad on its category of algebras.

I have now added a brief mentioning of this fact to maybe monad – EM category and relation to pointed objects.

For the moment this is without any of the further details that we talked about. Maybe Todd or Zhen Lin feel inspired to add them in. Otherwise I’ll try to do so later.

I have also added a pointer to this statement to smash produc (search the entry for the words “general abstract” to find the new proposition).

Finally I have added a pointer to Seal’s arXiv:1205.0101 to the References-section at monoidal monad and commutative monad (and maybe elsewhere, too, I forget).

Not sure how you all feel about it, and not sure how useful this is technically, but conceptually this makes me very happy: start with a homotopy-type theory $\mathbf{H}$ and consider the maybe modality (and what could be simpler than that..). Its “modal types” (the algebras) canonically form a linear homotopy-type theory over $\mathbf{H}$. If we also add a reduction modality and consider specifically the orthogonals to the reduced maybe types, then this is an abstract formalization of parameterized formal moduli problems and hence of sheaves of $L_\infty$-algebra. Voila, quite beautiful, in its way.

• CommentRowNumber7.
• CommentAuthorTodd_Trimble
• CommentTimeFeb 13th 2014

Re #6: I added some details of various recent discussions (Mike also supplied pertinent points) to the sections on Kleisli category and EM-category at maybe monad.

• CommentRowNumber8.
• CommentAuthorUrs
• CommentTimeFeb 13th 2014

Thanks, Todd (and Mike)! Very nice.

• CommentRowNumber9.
• CommentAuthorRodMcGuire
• CommentTimeFeb 14th 2014
• (edited Feb 14th 2014)

What is the relation of the maybe monad to what might be called “multi-pointed sets”?

Let’s say a multi-pointed set consists of a set equipped wit a list of distinguished elements.

One with 0 points is equivalent to a plain set, with 1 point a pointed set, with 2 points a bi-pointed object, etc.

There are obvious morphisms such as $*+$ which adds a new point to the set and pushes it onto the list, with the 2 “inverses” : $*-$ which just “pops” the list of points (forgetting that that point was distinguished) and $*--$ that in addition to popping the point list also removes that point from the set.

I am guessing that full treatment of such morphisms involves a simplex category. Does all this automatically fall out of the maybe monad?