Shouldn’t you be able to define a “strong monad” on a pseudomonoid in any monoidal 2-category?

]]>I presumed that the undefined $J$ designates the identity-on-objects functor so I stuck it in.

]]>Thanks, I put a remark at Freyd category to this effect, which also makes a link to the work of Jacobs-Heunen-Hasuo and Asada which is all about profunctors and Freyd categories. What always bothered me about this is that there I don’t know a very nice familiar way to describe the strength of the monad from the profunctor perspective. I mean, a strong cocontinuous monad on a presheaf category is a (what?) monad in Prof. (Not to say you can’t do it, and people have, but just that it is unfamiliar.)

]]>Nice, thanks! (Link for other readers: Freyd category.)

Of course, a colimit-preserving monad on a presheaf category is the same as a monad in Prof, which is the same as a bijective-on-objects functor. So I guess the point is that the monad is strong iff the functor is a Freyd category?

]]>Thanks, I have had a go at Freyd categories for now. I think wikipedia is also different because it serves a different purpose, perhaps as an introduction for the lay person, which means that wikipedia should probably follow the prevailing point of view even if that is arguably not the best route for the future (I had plenty of trouble with this a long time ago!)

]]>As you know, I find that ’personal agenda’ aspect very interesting for its not being so readily settled whether one POV supersedes/complements/runs contrary to another. But this is made more interesting as it takes place against a backdrop of ready agreement as to correctness of proof.

]]>That’s very true. Although even mathematicians have personal agendas about plenty of things just below the level of truth – but there we have the nPOV to guide us.

]]>Right. I suppose a small size of a community of contributors means that problematic contributors can be dealt with jointly in a case-by-case basis by informal community action. As we have done a handful of times in the past.

But another aspect that helps us is that, large or small, we are a community in the culture of modern mathematics.

It is hard to over-estimate the immense cultural accomplishment in mathematics, that people have a means to agree on the truth and to appreciate the truth seen by others. Just make a small step out of mathematics into other disciplines, and this ability vanishes rapidly.

This is a key reason why places like Wikipedia don’t allow contrinbutors to contribute their personal insights. In mathematics personal insight is universal, elsewhere personal insight can’t safely be distinguished from personal agenda.

]]>Urs is right; except that I wouldn’t say it has anything to do with the community size, it’s just that the nLab has a different purpose than WP. (Admittedly it might be harder to maintain quality this way with a larger community, but I don’t think if the community got larger we would change our purpose.)

]]>I could add these sorts of thing to the wiki but I am cautious about adding things which relate directly to my own papers.

We are small enough of a community that we can afford not to adopt the “neutral point of view” of Wikipedia and instead make good use of available expertise of members of our small community. If you know what you are doing and have something relevant and useful to add to an $n$Lab entry then, by all means, please do add it!

]]>Hello, Sorry to come late, just to add a couple of points in case it is helpful.

First: I think the original definitions of Freyd category by Power and Thielecke were in terms of premonoidal categories (they are almost just a premonoidal category with a given centre).

Second: as monoidal categories are to multicategories, so premonoidal categories are to “non-commutative” multicategories. By this I mean, when you formulate “multicategory” as Lambek using the circle-i formulation, you have associativity, identity and commutativity laws – drop the commutativity ones. Paul Levy and I called these “premulticategories” in our paper “Universal properties for impure programming languages” (it may have already been known or blindingly obvious).

I could add these sorts of thing to the wiki but I am cautious about adding things which relate directly to my own papers.

]]>#12 looks pretty promising to me. IIUC, the $\mathcal{M}$-funny tensor product of $C, D$ should be given by the pushout of $C \times D_t \leftarrow C_t \times D_t \rightarrow C_t \times D$, similar to the ordinary funny tensor, where $C_t$ is the $\mathcal{M}$-cat that has $C$’s tight morphisms as loose morphisms and tight morphisms.

This seems like a good level of generality to understand presentations of call-by-value languages that explicitly separate values and expressions as the internal language of the sort of generalized multicategory given by the “free cartesian-premonoidal $\mathcal{M}$-category” monad on some virtual equipment of $\mathcal{M}$-cats, where cartesian-premonoidal means the you have a premonoidal structure on loose morphisms that restricts to cartesian on tight morphisms.

Playing with that a bit it looks like this would axiomatize the 2 different kinds of composition for call-by-value expressions: let-binding which explicitly sequentializes terms (because the premonoidal structure is only functorial in each argument) and substitution of values into expressions. The inclusion of the tight morphisms into loose morphisms relates the 2 and in particular gives you the basic computation rule `let x = ret v in t == t[v/x]`

.

Has anyone considered putting the Kleisli construction in a purely premonoidal world?

I haven’t found anything like this.

]]>Note that the main example of Kleisli categories does come equipped with a specified class of central morphisms (those that factor through the unit of the monad).

Has anyone considered putting the Kleisli construction in a purely premonoidal world? That is, define what we mean by a strong monad on a *premonoidal* category and show that its Kleisli category (suitably defined) is again premonoidal? It seems like a natural thing to do when thinking about composites and transformers of monads. If so, I bet that could be expressed in terms of $\mathcal{M} Cat$ too.

Whether or not that is the natural definition of premonoidal functor given the definition using the funny tensor product I don’t know.

I don’t see how it could be. Preserving central morphisms is the sort of thing that never follows from preserving “algebraic structure”, since the universal quantifier in the notion of centrality in the codomain ranges over more things than in the domain.

However, that suggests to me another approach to defining premonoidal categories. Consider the 2-category $\mathcal{M}Cat$ of M-categories, whose morphisms are $\mathcal{M}$-functors (preserving tight and loose morphisms), and whose 2-cells are $\mathcal{M}$-natural transformations, i.e.\ transformations with tight components that are natural even with respect to loose morphisms. Now if $D$ and $E$ are $\mathcal{M}$-categories, there is an $\mathcal{M}$-category $[D,E]$ whose objects are functors $D\to E$, whose tight morphisms are $\mathcal{M}$-natural transformations, and whose loose morphisms are unnatural transformations with loose components that are natural with respect to tight morphisms. If $C$ is another $\mathcal{M}$-category, an $\mathcal{M}$-functor $C\to [D,E]$ consists of:

- for every object $x\in C$, an $\mathcal{M}$-functor $F(x,-) : D\to E$ (thus preserving both tight and loose morphisms)
- for every loose morphism $f:x\to y$ in $C$, an transformation $F(x,-) \to F(y,-)$ with loose components which is natural with respect to tight morphisms, and if $f$ is tight it has tight components and is natural with respect to loose morphisms,
- subject to compatibility and functoriality axioms.

The second and third data consist essentially of an extension of the function $F(-,-) : ob(C) \times ob(D) \to ob(E)$ to $\mathcal{M}$-functors $F(-,u) : C\to E$ for each $u\in D$, such that the bifunctoriality square for $f:x\to y$ in $C$ and $g:u\to v$ in $D$ commutes if either $f$ *or* $g$ is tight.

By general nonsense, there should now be a tensor product of $\mathcal{M}$-categories that is left adjoint to $[-,-]$, which I believe should make $\mathcal{M} Cat$ into a symmetric monoidal 2-category. And it seems, though I have not checked the details, that a pseudomonoid in this monoidal 2-category should be (almost?) the same as a non-strict premonoidal category equipped with a *specified* class of central morphisms (the tight morphisms) that contains the associators and unitors. (In particular, the above description of bimorphisms means that all the tight morphisms are central.)

I added a brief part about how Kleisli catgories of strong monads get premonoidal structure to the idea section (since it is the motivation for the entire concept).

Also, someone (Mike I think) had a remark that the center is maybe adjoint to the inclusion of monoidal categories into premonoidal categories, and this is true using the definition of premonoidal functor given in Power-Robsinson, because premonoidal functors there were required to preserve central morphisms. Whether or not that is the natural definition of premonoidal functor given the definition using the funny tensor product I don’t know.

]]>Ah, thanks *so* much, Sridhar! I get strangely obsessed with mysteries I can’t solve :-)

I remember the picture, but never recognised it.

]]>I’m pretty sure this Adam is the MO contributor that I interacted with here.

Totally off-topic, but his MO avatar used to be different: a picture of some mathematician or logician perhaps. Anyone remember that, and if so, who it was a picture of? Not knowing was driving me nuts (tried to ask him at MO, but he never replied).

]]>Okay, well then maybe I’ll remove it.

(Not that something written by Adam should be any less reliable, just that he seems unlikely to turn up here to explain what he was thinking of.)

]]>Whoever wrote that claim was Adam again.

]]>Hehe, yes, I did actually find that tiny mention.

Are you suggesting that maybe whoever wrote that claim at the page premonoidal category was thinking instead of promonoidal categories?

]]>One tiny mention here.

Is this a clue here

]]>“pro-monoidal” structures were originally called “pre-monoidal” ?

The page premonoidal category claims

There’s been a lot of discussion of this on the n-Category Café — someone find it and cite it!

But my google-fu is insufficient to find any such discussion. Can someone tell me where to look?

]]>