Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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)
Isn’t that function in the Keisli category a partial function? What was all that about restriction categories, Cockett and Lack’s work?
Isn’t that function in the Keisli category a partial function?
Yes, I have added that remark to maybe monad now.
What was all that about restriction categories, Cockett and Lack’s work?
Dunno, maybe you can tell me?
Since Steve Lack wrote three papers on them, there should be something important about them.
Thanks. Maybe I find the time to look at that later. For the moment I have put those pointers here
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.
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.
Thanks, Todd (and Mike)! Very nice.
(I just added some more hyperlinks)
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?
Added successor monad to “Related concepts”.
It seems strange to me that both this page and successor monad mention both the Kleisli category and EM category separately without mentioning that they’re equivalent. Is that because we need Excluded Middle to prove the equivalence (“every element is either equal or inequal to the point”)?
Added some information about the simplex category, based on the comment of JCMcKeown at successor monad.
(…)
Re #11: I don’t know about the EM category of the maybe monad, but I do know that intuitionistic logic can prove “every element is either equal or inequal to the point” for any (maybe X). (Unlike with arbitrary pointed types.)
Re #14, that’s exactly the point (npi) — the Kleisli category is (as for any monad) identified with the full subcategory of free algebras in the EM category, and in this case that consists of the pointed sets whose point is detachable.
But it should certainly be mentioned on the page that under classical logic the two coincide (and also that under intuitionistic logic the Kleisli category contains only the partial functions with detachable domain).
1 to 15 of 15