Not signed in (Sign In)

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

  • 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
    • CommentTimeApr 17th 2015
    • (edited Apr 17th 2015)

    created a minimum at function monad (aka “reader monad”, “environment monad”)

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 9th 2018
    • (edited Dec 9th 2018)

    What can be said about algebras for the function/reader monad, AA EA \mapsto A^E? I see Zhen Lin gives as an example a setting where for a function p:IEp: I \to E and dependent X(i)X(i), the product type i:IX(i)\prod_{i:I} X(i) is an algebra, where the action

    ( i:IX(i)) E i:IX(i) (\prod_{i:I} X(i))^E \to \prod_{i:I} X(i)

    sends ff to if(p(i))(i)i \mapsto f(p(i))(i).

    I guess you can think of that by factoring i:IX(i)\prod_{i: I} X(i) as e:E pX(i)\prod_{e: E} \cdot \prod_p X(i)?

    Is there anything to be said more generally about these algebras?

    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 9th 2018

    It’s possible that E:Set/ESet\prod_E: Set/E \to Set is monadic in general (the associated monad is this reader monad). I can check this at least in the case where EE is finite, using crude monadicity: E\prod_E preserves reflexive coequalizers since the latter are sifted colimits and these commute with finite products. It seems to be isomorphism-reflecting as well although a slick proof eludes me at the moment.

    I’m not going to have any time during the remainder of today to look into the situation for more general EE.

    • CommentRowNumber4.
    • CommentAuthorSam Staton
    • CommentTimeDec 9th 2018
    • (edited Dec 9th 2018)

    If I recall correctly, when E=2E=2 then the algebras are precisely the rectangular bands.

    Regarding #3, I don’t think E\prod_E reflects isos even for finite EE. If I’m not mistaken, when E={0,1}E=\{0,1\}, then E(X,k 0)= E(Y,k 0)=\prod_E(X,k_0)=\prod_E(Y,k_0)=\emptyset for all XX and YY. Here k 0k_0 is the constant 00 function. Maybe I misunderstood #3.

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 9th 2018
    • (edited Dec 9th 2018)

    Thanks, Sam. I see you’re talking about such things in Instances of computational effects:an algebraic perspective. I’d never heard of bands before. There’s then a ’rectangular bands monad’, as discussed here, which is id×idid \times id for the identity monad.

    A whole new world!

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 9th 2018

    Stupid me.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 9th 2018

    I’ve added something on algebras.

    diff, v14, current

    • CommentRowNumber8.
    • CommentAuthorSam Staton
    • CommentTimeDec 9th 2018

    Thanks. It was also discussed at the cafe back in 2015 (here). Out of that came the observation that :NonEmptySet 2NonEmptySet\prod: NonEmptySet^2\to NonEmptySet is monadic. So perhaps, more generally, #3 can be rescued with some non-emptyness assumptions.

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)