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

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

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

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

sends $f$ to $i \mapsto f(p(i))(i)$.

I guess you can think of that by factoring $\prod_{i: I} X(i)$ as $\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 $\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 $E$ is finite, using crude monadicity: $\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 $E$.

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

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

Regarding #3, I don’t think $\prod_E$ reflects isos even for finite $E$. If I’m not mistaken, when $E=\{0,1\}$, then $\prod_E(X,k_0)=\prod_E(Y,k_0)=\emptyset$ for all $X$ and $Y$. Here $k_0$ is the constant $0$ 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 \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.

• 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 $\prod: NonEmptySet^2\to NonEmptySet$ is monadic. So perhaps, more generally, #3 can be rescued with some non-emptyness assumptions.