Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.


Stream: community: discussion

Topic: monoidal products


view this post on Zulip Antonio Lorenzin (May 19 2025 at 10:55):

I wanted to raise a question that sparked from reading the discussion about the word evil (especially @Ryan Wisnesky @Jonas Frey and @Patrick Nicodemus's comments). I have the belief that sometimes, for example when we work with monoidal categories, we would like to fix ABCA \otimes B \otimes C — and perhaps we naively do so — and in general all finite-length monoidal products. I have seen this subtlety being overlooked many times, and I would like to know more about this issue and how people perceive it. For example, why is there not a clearly accepted definition of this concept?

Just to put a disclaimer for people who may jump up saying that there is the strictness theorem: this is, most of the time, insufficient to ensure that other definitions stemming from monoidal categories admit a strictification. In fact, strictification seems to be a statement that needs a proof each time we change the setting.

view this post on Zulip Morgan Rogers (he/him) (May 19 2025 at 11:19):

This is a consideration resolved either by convention (that ABCA \otimes B \otimes C is shorthand for (AB)C(A \otimes B) \otimes C, with bracketing always from the left or the right) or by using an unbiased definition of monoidal category which includes monoidal products of every finite arity, or by instead working with representable multicategories, so that these tensors are determined by their universal properties and the mediating isomorphisms can be left implicit because they too are determined by the universal properties.

view this post on Zulip Todd Trimble (May 19 2025 at 11:31):

I don't think it's a subtlety that people are missing so much, as it is a common and mild abuse of language. Writing parentheses produces clutter , and (adding to what Morgan just said) if the category of different choices and the associativity morphisms and whatnot mediating between them is contractible (meaning: exactly one morphism between any pair of objects), then it's considered okay to treat them as all "essentially the same", and thereby reduce the fuss and clutter by not bothering to disambiguate.

This is related to how the word "the" is used.

view this post on Zulip Antonio Lorenzin (May 19 2025 at 11:36):

I do see how the issue can be resolved, but it's weird to me that there is no precise definition. And granted that for categories this is easy to fix, when you look at functors this is more nuanced. Here's a situation I'm thinking about: let us consider a prop and a certain symmetric monoidal category. Then a choice of a (symmetric) strong monoidal functor is also a choice of parenthesis, which feels unnecessary, but there is no strict functor if the symmetric monoidal category isn't strict.

Also, the convention you mentioned is definitely one way to consider this irrelevant, which I tend to believe is for most applications, but it's not what we do even for sets.

view this post on Zulip Patrick Nicodemus (May 19 2025 at 17:11):

but it's not what we do even for sets.

Isn't it? If you asked me to formally define the product A×B×CA\times B \times C in set theory I would use iterated Kuratowski pairs instead of introducing a custom coding of "ordered triple" in ZFC.

view this post on Zulip Kevin Carlson (May 19 2025 at 17:15):

It's not quite clear what you're claiming has no precise definition, but I'm pretty sure that when we dig into it you'll learn there is a precise definition, along one of the lines Morgan suggested.

view this post on Zulip Paolo Perrone (May 19 2025 at 17:22):

Could we solve this by making cliques more of a standard structure? (And anafunctors, etc.)

view this post on Zulip Mike Shulman (May 19 2025 at 17:26):

Patrick Nicodemus said:

but it's not what we do even for sets.

Isn't it? If you asked me to formally define the product A×B×CA\times B \times C in set theory I would use iterated Kuratowski pairs instead of introducing a custom coding of "ordered triple" in ZFC.

However, if I had a uA×B×Cu \in A\times B\times C and you ask me what its "first component" is, the answer would be an element of AA, not an element of A×BA\times B, even if you formally defined A×B×CA\times B\times C to be (A×B)×C(A\times B)\times C. So although we might take that as the formal definition, we immediately hide it behind an abstraction barrier and never use anything about it except that it's a product of A, B, and C in Set.

view this post on Zulip Patrick Nicodemus (May 19 2025 at 17:38):

@Paolo Perrone Off topic, but I don't know what an anafunctor is. I skimmed the definition on nlab and I got 'it's similar to a representable profunctor, but not exactly.' Can you or someone else explain anafunctors in terms of representable profunctors?

view this post on Zulip Paolo Perrone (May 19 2025 at 18:17):

@Patrick Nicodemus I'm not an expert at all (please anyone correct me if needed!), here's how I view the two things:
1) An anafunctor is "something like a functor mapping objects to cliques". A canonical example on the nose is the pseudoinverse of a given functor.
2) A representable profunctor is "something like a functor mapping objects to the representatives of a presheaf". A canonical example on the nose is a right-adjoint (representing the presheaf C(L-,Y): D^op -> Set for a given functor L: D->C), and another one is a pointwise Kan extension.

Now "objects representing the same presheaf", i.e. "satisfying the same universal property", form exactly a clique, so 1) is a special case of 2).
Conversely, but more "indirectly", an anafunctor gives rise to a representable profunctor (either form spans, or, if you allow choice, take an object in the clique and its representable presheaf).
Therefore the two concepts are in some sense equivalent, but have a different flavor: for anafunctors, the focus is on the "up to isomorphism", while for representable profunctors, the focus is on the universal property.

A canonical situation where you see the slight difference, citing what the nLab says, is if you want a left-adjoint. Clearly it's a functor defined up to isomorphism, but this time the universal property is the other way around, we are representing a functor D(X,R-): C -> Set, not a presheaf.
So it's pretty clear how the same "up to isomorphism" game still holds, but finding specifically a presheaf that this should represent takes some more work.
Similar considerations can be made for pseudoinverses (what's the presheaf?), for the coherence of monoidal categories, and so on.

What I said in my post above could be either in favor of anafunctors or of representable profunctors.

view this post on Zulip Antonio Lorenzin (May 19 2025 at 18:25):

Let me try to express more precisely what I find unsatisfying about the standard notion from a functorial perspective.

Intuitively, I'd like to consider only strong functors between monoidal categories that allow for a strict version. More precisely, let CC and DD be two monoidal categories and consider their strictifications CstC_{st} and DstD_{st}. Then I'd like to consider strong functors CDC\to D giving rise to strict functors CstDstC_{st} \to D_{st}.

Note that this is not necessarily true; in fact, there exist strong functors that are not naturally isomorphic to strict functors even between strict monoidal categories (a simple example is obtained by considering Z/2Z\mathbb{Z}/2\mathbb{Z} as a monoidal category with one object, and then take the identity functor equipped with the natural transformation given by the nontrivial element).

To avoid this issue and considering only functors that are more properly "strict" in this sense, it seems natural to consider the case where all finite-length monoidal products are fixed to begin with. Is there any way to circumvent this issue?

view this post on Zulip Antonio Lorenzin (May 19 2025 at 18:33):

Kevin Carlson said:

It's not quite clear what you're claiming has no precise definition, but I'm pretty sure that when we dig into it you'll learn there is a precise definition, along one of the lines Morgan suggested.

I think there is an "obvious" precise definition (by fixing all finite-length monoidal products), but as far as I can tell it's not used in the literature. And my interest is mostly on the functors that come from such a description.

view this post on Zulip Antonio Lorenzin (May 19 2025 at 18:35):

Paolo Perrone said:

Could we solve this by making cliques more of a standard structure? (And anafunctors, etc.)

This seems a promising direction, although I can't see how to make it precise at the moment. Thank you for the input!

view this post on Zulip Tobias Fritz (May 19 2025 at 18:59):

Antonio Lorenzin said:

I think there is an "obvious" precise definition (by fixing all finite-length monoidal products), but as far as I can tell it's not used in the literature.

If I understand correctly, what you're suggesting here is the unbiased definition of monoidal category (as mentioned earlier in this thread). This is developed in some detail in Section 3.1 of @Tom Leinster's HIgher Operads, Higher Categories.

view this post on Zulip Tobias Fritz (May 19 2025 at 19:07):

Giving a fully unbiased definition of symmetric monoidal category is harder, because one needs to have a way to avoid distinguishing ABA \otimes B from ABA \otimes B without losing track of the braidings. One possibility appears in Tannakian categories by Deligne and Milne:
image.png
Their definition tacitly assumes the strict equality CI=jJCα1(j)\mathsf{C}^I = \prod_{j \in J} C^{\alpha^{-1}(j)} for any map of finite set α:IJ\alpha : I \to J, without which their coherence morphisms don't type check. I suppose that this can be fixed, but it seems pretty tedious to get this really right.

view this post on Zulip Tobias Fritz (May 19 2025 at 19:14):

What is arguably the most systematic is the definition used in (,1)(\infty,1)-category theory to define symmetric monoidal structures. This is based on a fibrational picture where the symmetric monoidal structure becomes something more like a property rather than a structure. See e.g. Section 3.1 of Harpaz's lecture notes:
image.png
Roughly, this encodes the symmetric monoidal structure as a property in a way that is similar to how the nerve of a category encodes composition as a property.

view this post on Zulip Mike Shulman (May 19 2025 at 19:15):

Antonio Lorenzin said:

let CC and DD be two monoidal categories and consider their strictifications CstC_{st} and DstD_{st}. Then I'd like to consider strong functors CDC\to D giving rise to strict functors CstDstC_{st} \to D_{st}.

Note that this is not necessarily true; in fact, there exist strong functors that are not naturally isomorphic to strict functors even between strict monoidal categories

I think you confused two similar but different things here. It's true that given two strict monoidal categories, there may be strong functors between them that are not isomorphic to any strict functor between those same monoidal categories. But it is nevertheless true that every strong monoidal functor between two monoidal categories is equivalent, in a suitable sense, to some strict monoidal functor between their strictifications.

view this post on Zulip Mike Shulman (May 19 2025 at 19:18):

At least, if you choose the strictifications appropriately. (In particular, of course, that means even if the starting monoidal categories are strict, you can't choose themselves as their "strictifications".)

view this post on Zulip Antonio Lorenzin (May 19 2025 at 19:19):

@Tobias Fritz yes, that is what I have in mind! Apparently this is more investigated than I previously believed. I also thought that this should be well-known to higher categorists (and the last \infty-category approach is more sensible to what a monoidal category should be to me). Thank you for the pointers!

view this post on Zulip Mike Shulman (May 19 2025 at 19:23):

Tobias Fritz said:

Giving a fully unbiased definition of symmetric monoidal category is harder

Well, I suppose it depends on what you think that should mean. Normally when I say an unbiased symmetric monoidal category I would think of having ordered n-ary tensor products, just like in an unbiased non-symmetric monoidal category, with isomorphisms between them given by all permutations.

view this post on Zulip Mike Shulman (May 19 2025 at 19:24):

I think that matches better what we do in practice, e.g. we write A×B×CA\times B\times C rather than parenthesizing it, but we still write them in an order.

view this post on Zulip Tobias Fritz (May 19 2025 at 19:25):

Right, I know that that's how the term 'unbiased' is usually used, but I don't think that this matches the practice of e.g. network theory: if you permute the terminals of an electrical network, then practictioners would still call it the same network!

view this post on Zulip Tobias Fritz (May 19 2025 at 19:28):

Also if we take the [[periodic table]] seriously, then string diagrams in SMCs really live in four dimensions, and the "spatial slices" that designate objects are more like unordered bunches of wires, no? So what I meant by 'fully unbiased' was a kind of definition of SMC which implements the idea that it should be possible to tensor a bunch of objects with ordering them.

And although this is perhaps counterintuitive because one might be afraid of losing track of the braidings, the definitions I've pointed to actually realize this idea.

view this post on Zulip Tobias Fritz (May 19 2025 at 19:29):

Mike Shulman said:

I think that matches better what we do in practice, e.g. we write A×B×CA\times B\times C rather than parenthesizing it, but we still write them in an order.

Not always, it's also common to write things like iIAi\prod_{i \in I} A_i, no? Although arguably less common when II is finite than when it's infinite.

view this post on Zulip Kevin Carlson (May 19 2025 at 20:01):

Tobias Fritz said:

Right, I know that that's how the term 'unbiased' is usually used, but I don't think that this matches the practice of e.g. network theory: if you permute the terminals of an electrical network, then practictioners would still call it the same network!

In at least some applications, the issue is that you really do want a commutative monoidal category instead of a symmetric one: this is famously the case with Petri nets, which generate CMCs in their traditional semantics and SMCs in their whole-grain formulation. But I guess you do need a braiding for electrical networks, what with the wires and all...

view this post on Zulip Antonio Lorenzin (May 19 2025 at 20:01):

Mike Shulman said:

Antonio Lorenzin said:

let CC and DD be two monoidal categories and consider their strictifications CstC_{st} and DstD_{st}. Then I'd like to consider strong functors CDC\to D giving rise to strict functors CstDstC_{st} \to D_{st}.

Note that this is not necessarily true; in fact, there exist strong functors that are not naturally isomorphic to strict functors even between strict monoidal categories

I think you confused two similar but different things here. It's true that given two strict monoidal categories, there may be strong functors between them that are not isomorphic to any strict functor between those same monoidal categories. But it is nevertheless true that every strong monoidal functor between two monoidal categories is equivalent, in a suitable sense, to some strict monoidal functor between their strictifications.

Thank you for pointing this out! What I wanted to express in my setting is that the strictifications are not really taken to necessarily be "universal", but instead they are fixed at the beginning. So, in particular, a strong functor that is not naturally isomorphic to a strict functor is something that I would like to disregard as "not good enough". Also, if there were two strict functors that are naturally isomorphic, then I'd still want to consider them as separate.
More intuitively, I'm looking for an identification of strong functors that only differ by a "choice of parenthesis".

To keep in mind why on earth I'd want that, consider a (colored strict) prop PP and a symmetric monoidal category CC. If I give you a good assignment of the generators of PP in CC (i.e., all the relations are satisfied), this should give you a class of strong functors that are "unique up to parentheses". In particular, when I consider C=PC=P, then the identity assignment should give you only the identity functor.
My instinct (and not more at the moment) tells me that this may be more easy to describe if I fix finite-length tensor products, for example.

view this post on Zulip Mike Shulman (May 19 2025 at 20:06):

Tobias Fritz said:

Mike Shulman said:

I think that matches better what we do in practice, e.g. we write A×B×CA\times B\times C rather than parenthesizing it, but we still write them in an order.

Not always, it's also common to write things like iIAi\prod_{i \in I} A_i, no? Although arguably less common when II is finite than when it's infinite.

I think it is quite rare to write that when II is an unordered finite set. And we are talking here about monoidal structures here, not arbitrary products, so there isn't really even a possibility of II being infinite in iIAi\bigotimes_{i\in I} A_i.

view this post on Zulip Tobias Fritz (May 20 2025 at 04:47):

Mike Shulman said:

I think it is quite rare to write that when II is an unordered finite set.

I'll grant that the rarity or frequency of that notation varies from subject to subject, so let me mention one context where this is used frequently, namely the theory of Bayesian networks. There, one has a directed graph (V,E)(V,E) and a Markov kernel p(xvxparents(v))p(x_v|x_{\mathrm{parents}(v)}) associated to each edge vertex vv. These kernels are composed to a joint distribution given by p(x)=vVp(xvxparents(v))p(x) = \prod_{v \in V} p(x_v|x_{\mathrm{parents}(v)}).

In the special case where the graph has no edges, this is simply a product of probability distributions indexed by VV, which is a monoidal product with finitely many factors in a Markov category. The fact that the standard or unbiased definition of SMC do not support this kind of tensoring while VV is unordered is a frustrating issue for the semantics of Bayesian networks. (And it's even worse when the graph does have edges, because then one needs to evaluate a genuine string diagram in a Markov category, without having a planar embedding.)

So this kind of comsposition works and is used in the context of Bayesian networks, and therefore I think that category theorists should provide a definition of SMC that supports it natively.

view this post on Zulip Mike Shulman (May 20 2025 at 06:04):

Interesting, thanks for sharing. Is that a non-cartesian monoidal structure? (It sounds like you're saying it is; I ask because you wrote \prod rather than \bigotimes.)

view this post on Zulip Mike Shulman (May 20 2025 at 06:09):

Tobias Fritz said:

I think that category theorists should provide a definition of SMC that supports it natively

I know you didn't mean it this way, but that phrase sounds a little offensive to my ears, as if category theorists existed only to serve the needs of other mathematicians. Even though I generally agree that category theory is improved by looking at what structures arise naturally in other areas of mathematics and trying to model them.

view this post on Zulip Mike Shulman (May 20 2025 at 06:11):

Anyway, you're probably aware that Leinster wrote down a definition of symmetric multicategory along these lines in one of his appendices, under the name "fat symmetric multicategory". So perhaps to avoid confusion with existing notions of "unbiased", this could be called a "fat symmetric monoidal category".

view this post on Zulip Nathanael Arkor (May 20 2025 at 06:37):

Pisani also studies "fat" (symmetric) monoidal categories in Unbiased multicategory theory.

view this post on Zulip Tobias Fritz (May 20 2025 at 07:00):

Mike Shulman said:

Interesting, thanks for sharing. Is that a non-cartesian monoidal structure? (It sounds like you're saying it is; I ask because you wrote \prod rather than \bigotimes.)

Yes, that's right! The formation of product distributions multiplies probabilities (so the product is a product of numbers), but it's a non-cartesian symmetric monoidal structure.

view this post on Zulip Tobias Fritz (May 20 2025 at 07:03):

Mike Shulman said:

as if category theorists existed only to serve the needs of other mathematicians.

Oh, I certainly didn't mean that with an "only". But I'd hope for that to be one purpose among others for some category theorists!

view this post on Zulip Tobias Fritz (May 20 2025 at 07:23):

Thanks for the pointers to fat symmetric multicategories! I didn't know about the Pisani paper. It's nice that this even gives an apparently well-behaved notion of infinitary SMC.

view this post on Zulip Jonas Frey (May 20 2025 at 07:36):

Since I don't see it mentioned yet (sorry if I missed it): unbiased symmetric monoidal categories can be defined as algebras for a 2-monad on Cat with a fairly easy definition: SC is the category whose objects are lists of objects in C, and morpisms between lists of the same length are given by pairs of a permutation and an n-tuple of maps in C.

view this post on Zulip Jonas Frey (May 20 2025 at 07:37):

This appears in the work on generalized species

view this post on Zulip Jonas Frey (May 20 2025 at 07:41):

Regarding the "fat" case: I think one can define a notion fat non-symmetric multicategory for each class J of linear orders which contains 1 and is closed under J-indexed ordinal sums.

I wonder if this has been studied, or if anyone has seen examples?

view this post on Zulip Sam Staton (May 20 2025 at 08:30):

Hi In programming, the components of a product are very often named (called "fields"). @Owen Lynch just uploaded a preprint connecting this with strict products, SMCs etc. (Sec 3). Perhaps this is relevant. [Sorry this is not an answer to Jonas's last question, though.]

view this post on Zulip John Baez (May 20 2025 at 11:41):

A data point from a mathematical physicist: I often use products and tensor products indexed by unordered sets. For example in my old work on quantum gravity I defined a connection on a graph to be an element of

eEG \prod_{e \in E} G

where EE is the set of edges of the graph and GG is some Lie group. Of course we could rewrite this as GEG^E. But I also introduced a Hilbert space of 'quantum connections' on the graph as

eGL2(G) \bigotimes_{e \in G} L^2(G)

where I'm taking an unordered tensor product of Hilbert spaces L2(G)L^2(G).

I've done this sort of thing forever, it seems, and only recently a referee of one paper raised a question of what these unordered products mean. I forget how I finessed it - some explanatory remark.

view this post on Zulip Antonio Lorenzin (May 20 2025 at 12:00):

I would like to know that explanatory remark if possible, because that tensor product seems inherently ordered to me.

Btw, another important thing to keep in mind when doing such unordered variants, is that somehow you'd like to be able to say what invariance under permutation is. I remember discussing this with @Tobias Fritz

view this post on Zulip John Baez (May 20 2025 at 12:14):

@Antonio Lorenzin - basically the explanatory remark amounted to "don't worry about it, there are lots of ways to formalize this, and it doesn't matter which you use". This thread has listed a bunch, and it's easy to make up more.

view this post on Zulip Antonio Lorenzin (May 20 2025 at 12:24):

@John Baez Just to better understand, this is not really different from choosing a wellorder, is it?

view this post on Zulip John Baez (May 20 2025 at 12:29):

It really depends on what "really" means.

view this post on Zulip John Baez (May 20 2025 at 12:32):

I would never bother to choose an order myself. I think it's quite possible to define the universal property of a tensor product of vector spaces like

xSVx \bigotimes_{x \in S} V_x

for some finite set SS without ever choosing an order on SS. The universal property specifies this tensor product up to canonical isomorphism. You are then free to construct something obeying this universal property using whatever method you like. The great thing about universal properties is that I don't need to know or care what method you've chosen: as long as it obeys the universal property you're okay.

view this post on Zulip Antonio Lorenzin (May 20 2025 at 12:43):

Yes, I think we are saying similar things from different perspectives. If we want to fix one tensor object, then order matters, but if we instead work up to unique iso, then such a choice becomes irrelevant.

view this post on Zulip John Baez (May 20 2025 at 13:09):

Okay. I don't think the order needs to matter even if you want to fix one tensor object... but I also don't care! I always want to work only up to unique isomorphism, because I'm trying to communicate with many mathematicians, who may have their own constructions of tensor products, and I want to let them use their own constructions.

If I were designing a software system to work with tensor products, or doing some foundational work on mathematics, or writing an algebra textbook, then I might need to choose some 'unique up to equality' definition of tensor products. (Or maybe I would avoid this.)

view this post on Zulip Antonio Lorenzin (May 20 2025 at 13:21):

I guess it depends on the category, but I do agree that this may be more annoying than important in many contexts --- I can imagine this being very important in higher categorical structures, but since I'm not familiar with them, let me just leave it at that.

view this post on Zulip Antonio Lorenzin (May 20 2025 at 13:23):

John Baez said:

If I were designing a software system to work with tensor products, or doing some foundational work on mathematics, or writing an algebra textbook, then I might need to choose some 'unique up to equality' definition of tensor products. (Or maybe I would avoid this.)

That is an interesting approach, because I feel it's more natural to work with strict monoidal categories so that everything is fixed, rather than reasoning up to natural iso.

view this post on Zulip John Baez (May 20 2025 at 13:39):

I'm not working in isolation: my work relies communicating with many people. The mathematicians I know have almost all learned the universal property definition of tensor product (of vector spaces, say), and that's what they consider fundamental. Since I want my theorems to be understandable and valid to all these mathematicians, I can't use rely on anything but the universal property.

I also talk to some physicists whose definition of tensor product is roughly: the tensor product of Cn\mathbb{C}^n and Cm\mathbb{C}^m is Cmn\mathbb{C}^{m n}. Or: the tensor product of a vector space VV with basis eie_i and a vector space WW with basis fjf_j is some vector space with basis consisting of symbols eifje_i \otimes f_j. Luckily I can write in a way that's at least roughly understandable to them too, since most the things I do with tensor products can be understood in these terms. Some may ask about the question you raise: how do we tensor an unordered set of vector spaces? Then, since I probably don't want a long conversation, I may tell them "choose an ordering".

view this post on Zulip Antonio Lorenzin (May 20 2025 at 13:54):

That makes total sense!

By the way, I apologize if I came across as harsh or disrespectful — that wasn’t my intention. I have a deep appreciation for your expertise, and I understand you're not working in isolation. In fact, between the two of us, I think I’m the one working in more isolation. When I said 'that’s an interesting approach,' it was meant as a genuine expression of surprise, because my (limited) experience had suggested otherwise. Again, sorry for the mishap.

view this post on Zulip John Baez (May 20 2025 at 14:04):

Don't worry, you didn't seem harsh or disrespectful at all! The fact that you think I might have thought that (oh-oh, now it's getting complicated) probably comes from me sounding a bit harsh. And that's simply because this sort of question reminds me of when I'm working on my Windows machine and all of a sudden it turns out that to do something I need to enter some code in DOS in the command line interface.... leaving the level of abstraction I'm comfortable with, and going down to some primitive realm.

view this post on Zulip Amar Hadzihasanovic (May 20 2025 at 14:49):

I believe the notion of nominal prop from this paper by Samuel Balco and @Alexander Kurz may be relevant to the discussion. I believe that this is essentially trying to formalise the idea of a node (or box) in a string diagram having named wires instead of ordered wires, and a connection being possible wrt any matching of named wires, rather than by "reordering" with the structural symmetric braidings.

view this post on Zulip Amar Hadzihasanovic (May 20 2025 at 14:51):

Things like John's "unordered tensor products" are very natural if one takes the nominal approach... such a tensor product would have a set of named wires which is like a dependent sum: one parameter for the index, and then one for each named wire of the indexed diagram...

view this post on Zulip Mike Shulman (May 20 2025 at 15:37):

John Baez said:

I often use products and tensor products indexed by unordered sets.

Cool! Thanks to you and Tobias, today I have learned that something I thought was fairly esoteric is actually useful.

Maybe fat symmetric monoidal categories would be a nice subject for a TAC Expositions paper.