Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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?

    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?

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeFeb 12th 2014
    • 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 H\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 H\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 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.

    (I just added some more hyperlinks)

    • 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?

    • CommentRowNumber10.
    • CommentAuthoratmacen
    • CommentTimeSep 1st 2019

    Added successor monad to “Related concepts”.

    diff, v8, current

  1. 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”)?

  2. Added some information about the simplex category, based on the comment of JCMcKeown at successor monad.

    diff, v9, current

    • CommentRowNumber13.
    • CommentAuthorOscar_Cunningham
    • CommentTimeSep 1st 2019
    • (edited Sep 1st 2019)

    (…)

    • CommentRowNumber14.
    • CommentAuthoratmacen
    • CommentTimeSep 1st 2019

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

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeSep 1st 2019

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