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: theory: category theory

Topic: Binoidal categories and the principle of equivalence

Jacques Carette (May 16 2024 at 17:43):

The definition of binoidal category as given at [[premonoidal category]] seems overly strict and, in fact, seems to not respect the [[principle of equivalence]]. So this gives it an air of a not-particular-categorical concept. All the papers that I've seen that define binoidal category give a similar definition that mentions equality on objects.

Is this inevitable?

Kenji Maillard (May 16 2024 at 17:52):

Example 13.4 page 111 of The Univalence Principle by Benedikt Ahrens, Paige Randall North, Michael Shulman, and Dimitris Tsementzis does tackle the case of premonoidal categories.

Jacques Carette (May 16 2024 at 18:44):

Ah, thanks, yes, that does seem better. (Minor point: it is example 13.4 but that's on p.117; I was confused as there's an example 12.4 on p.111 !)

Jacques Carette (May 16 2024 at 19:00):

And I was able to formalize that in Agda in no time, and it looks like it's going to be smooth sailing to work with that.

Philip Saville (May 16 2024 at 21:03):

I would push back a bit on this idea that definitions which don't respect the principle of equivalence should be viewed as "not particularly categorical". My feeling is that we shouldn't get into the habit of automatically making all our definitions weaker just so the principle of equivalence holds, because in some cases it adds work without clarifying the theory. (Though I accept that when it comes to formalisation things might well be the opposite!)

For example, I think people would agree Gray-monoids or Gray-categories (see e.g. Day and Street) are "categorical", but their definition involves a similar equality to binoidal categories. And this arises very naturally from the enriched category theory. (I strongly suspect similar properties are in play in the binoidal case.)

Alternatively: Lawvere theories are typically defined using strict preservation of products, but I don't think this is ever an obstacle in developing their theory. In fact I suspect that making the definition weaker but invariant under equivalence would add complication without much gain. Another similar example would be the Kelly-Eilenberg definition of closed categories, which uses an identity of functors but -- so far as I remember -- that doesn't cause any issues with the proofs. (Again, I'm talking here about pen-and-paper mathematics rather than formalisation.)

For another, perhaps more provocative, example: functors strictly preserving some kind of structure are typically not closed under isomorphism (e.g. a strict product preserving functor can be naturally isomorphic to one that only preserves products up to iso) but it is sometimes very useful to work with strict functors because you can then talk about uniqueness on the nose, and so get (1-dimensional) adjunctions. This occurs quite often in even in categorical semantics but is especially obvious in higher category theory. For example, in his book Coherence in three-dimensional category theory Gurski often states free properties using strict pseudofunctors or similar. Taking the idea things ought to be invariant under equivalence completely seriously in this setting would require us to work up to equivalence of pseudofunctors, which would change the universal property from an adjunction to a biadjunction. So we'd have to do a lot more work only to get a property that's much less easy to work with. (And that's before we start on any tricategories!)

Mike Shulman (May 16 2024 at 21:14):

The only reason the definition on the nLab looks non-categorical is that we're used to a bundled definition of "functor" that includes the action on objects, so if you want to have two functors that act the same on objects you have to ask for an equality of objects. The solution is to view "a functor whose action on objects is F" as a perfectly good and categorical definition, given a function F on objects. This notion can't be defined categorically in terms of the definition of "functor", but rather the reverse: a functor is a function F on objects together with "a functor whose action on objects is F".

Mike Shulman (May 16 2024 at 21:14):

This is a totally different issue from things like the strictness of strict 2-categories and Gray-categories.

Jacques Carette (May 16 2024 at 22:44):

@Mike Shulman 's interpretation seems to me to be of the same flavour as "identity on objects functors" - it is a bunch of data that induces a functor, but not a special kind of functor. As an unbundled definition, IOO makes perfect sense.

I much prefer that view as also applied to Binoidal.

Philip Saville (May 17 2024 at 12:57):

Mike Shulman said:

The only reason the definition on the nLab looks non-categorical is that we're used to a bundled definition of "functor" that includes the action on objects, so if you want to have two functors that act the same on objects you have to ask for an equality of objects. The solution is to view "a functor whose action on objects is F" as a perfectly good and categorical definition, given a function F on objects

This is a neat point I've not appreciated before :)

My worry is that sometimes we give the impression that a definition involving identities should automatically be considered less 'nice' than definitions which are weak enough to be respected by equivalence. I imagine a student writing down the definition of binoidal category and then thinking to themselves it can't be right, so they throw it away and end up writing something much more complicated when they didn't need to.

So my point is that

1. Definitions that at first sight appear 'suspect' can actually arise for good reasons. For me, Mike's argument is a nice example of this: the binoidal definition looks 'off' but is actually quite natural from the right point of view. And I suggested Gray-monoids because they have a very similar equality between functors on objects, which also occurs very naturally because it falls out of the definition of the Gray tensor product on Cat.

2. Even if a definition does involve some equalities that are not preserved by equivalence, that doesn't necessarily make it less good. Perhaps one might have to occasionally take a bit more care but the net simplification in the theory can make this worthwhile. For me, Lawvere theories and closed categories sit in this bracket.

Jacques Carette (May 17 2024 at 13:26):

I don't think that definitions that are written using identities (on objects) are necessarily bad - but as software developers says, it is a "code smell". It's not that what you're trying to define (such as Binoidal categories, identity on objects functors, Lawvere theories, etc) are themselves bad, but that the means you've chosen to define them is suspect.

I think using a variety of different foundations is useful in this regard: certain settings (such as dependent type theory) let you more easily see that some definitions' exact phrasing is suspect. In some foundations (like ZFC), certain utterances are invisibly equivalent.

In many of the cases that I've encountered, the subtle difference is between is and induces -- a category, a functor, etc. It's a data-flow problem: what data is given a priori, and what data can be extracted a posteriori out of a bundle. Equalities on a posteriori information is problematic, equalities that are pre-witnessed on a priori information is perfectly fine. (This is quite clear IOO Functors, IMHO.)

Philip Saville (May 17 2024 at 14:26):

For me the word 'suspect' is too strong. By which I mean: I can't recall an instance where this 'suspect'ness has actually caused me a problem in a proof (e.g. when working with binoidal categories or Lawvere theories or whatever). In my mind it doesn't reduce the stock of examples but does simplify the theory so I'm happy. Of course, I might just be outing myself as someone who has never tried to persuade a theorem prover of every detail of their definitions, because I know then these issues can really bite!

Part of my motivation for being so pernickety is that a lot of people learn CT from Zulip nowadays, and I want to point out that -- while one can be very careful about making everything invariant -- you don't have to do that in order to do good category theory. And there are central concepts in the field where this happens (or at least appears to). We can debate which is better, but I do think both approaches are actually fine.

(I do agree with your point about different foundations being a useful way to make explicit coercions so we can ask ourselves whether or not we're really happy with them, and also that there's lots of interesting questions about whether one can tweak the phrasing of a definition to make it more invariant. But I think we probably disagree on the extent to which these questions trouble us in our day-to-day research!)

Mike Shulman (May 17 2024 at 15:30):

Gray-monoids do have an equality like binoidal/premonoidal categories that can be dealt with in the same way, but they also have strict associativity and unit laws which can't be removed similarly. The latter sort of strictness is of a different flavor, and also appears more simply in strict 2-categories. I would probably argue that Eilenberg-Kelly closed categories are also of that sort, since an EK closed structure is not transportable across an equivalence of categories (but every LaPlaza-Manzyuk closed category is isomorphic to an EK one with different hom-sets -- a sort of "strictification theorem" like "every bicategory is equivalent to a strict 2-category").

Mike Shulman (May 17 2024 at 15:32):

When working in [[set-level foundations]], I agree that definitions that are "too strict" aren't necessarily wrong, and can be very useful on occasion. When using them one incurs an extra obligation to verify that all the "important" constructions are equivalence-invariant (in addition to the "strictification" result that justifies their use in the first place), but sometimes that can be a worthwhile price to pay for the simplification that accrues from strictness. [[2-monad]] theory is one of my favorite examples of this.

Mike Shulman (May 17 2024 at 15:34):

But in [[higher-level foundations]], the "too strict" definitions usually aren't sufficiently general, e.g. it's no longer true that every bicategory is equivalent to a strict 2-category.

Max New (May 18 2024 at 13:44):

The original article is a bit sloppy, I should probably clean up the writing. A binoidal category is simply a category $C$ equipped with a "separately functorial bifunctor" $C,C \to C$ (would be nice to have simple terminology for separate vs jointly functorial bifunctors). Separately functorial bifunctors respect equivalence of categories so there's no issue with the principle of equivalence.

You seem to be complaining that the definition of separately functorial bifunctor (which is basically inlined on this page) says that it is two functors that agree on objects, and that in general imposing equality of functors on objects is not equivalence-respecting. But just because each intermediate step of a construction doesn't follow from a generally applicable equivalence-respecting principle doesn't mean that the final construction is not equivalence respecting.

Matteo Capucci (he/him) (May 19 2024 at 03:28):

It's indeed very sad that bifunctors are not separately functorial functors but jointly functorial functors

Matteo Capucci (he/him) (May 19 2024 at 03:29):

In fact I would push to reappropriate bifunctor for the latter since there is no reason to call bifunctors the first instead of just 'functors of 2 variables' or the suchlike

Mike Shulman (May 19 2024 at 03:51):

I think the word "bifunctor" is just unfortunate and should be retired completely. It could variously be interpreted as a joint functor of two variables, a separate functor of two variables, a functor between bicategories, or a functor that is also a cofunctor.

Matteo Capucci (he/him) (May 20 2024 at 15:39):

I forgot about the last two. Ugh.

Jacques Carette (May 21 2024 at 15:52):

Max New said:

The original article is a bit sloppy, I should probably clean up the writing. [...]
You seem to be complaining that the definition of separately functorial bifunctor (which is basically inlined on this page) says that it is two functors that agree on objects, and that in general imposing equality of functors on objects is not equivalence-respecting. But just because each intermediate step of a construction doesn't follow from a generally applicable equivalence-respecting principle doesn't mean that the final construction is not equivalence respecting.

You're probably correct that my main complaint is one of "sloppy writing".

There is definitely an issue of who is the audience: is the nLab purely reference material for people who are assumed to already know all of this intimately, or is it also meant as somewhat pedagogical material for people new to the less standard parts of category theory? I'd say the vast majority of readers belong to the latter class of people.

So yeah, "sloppy writing" will definitely confuse me. I am not at the level of understanding (yet) where I can tell that apart from 'the definition means what it says exactly'.

Mike Shulman (May 21 2024 at 18:40):

The nLab is whatever people make of it. There's lots of pedagogical material, but lots of articles don't have a pedagogical aspect just because no one has felt inspired to write it yet.

Jacques Carette (May 21 2024 at 18:46):

I don't know why I keep getting myself embroiled in these things. I don't care about binoidal categories... I was trying to help someone else. Next thing I knew, I was way way deep in a rabbit hole that I had no idea even existed, never mind being as this deep.

Reid Barton (May 22 2024 at 20:21):

Max New said:

Separately functorial bifunctors respect equivalence of categories so there's no issue with the principle of equivalence.

Maybe I'm misunderstanding some of the words in this sentence, but this surprises me.
Say $I$ is the "walking isomorphism". Isn't a "separately functorial bifunctor" $I, I \to C$ the same as giving a possibly non-commuting square of isomorphisms in $C$?
While a "separately functorial bifunctor" $1, 1 \to C$ is just an object of $C$; and these aren't equivalent. Unless the natural transformations are also not what I expect, maybe?

Reid Barton (May 22 2024 at 20:22):

(I'm also open to the possibility that "principle of equivalence" doesn't mean what I expect)

Mike Shulman (May 22 2024 at 20:48):

Yes, I think I agree. In fact, that's one of the important and subtle things about premonoidal categories and their ilk, that things in them are not invariant under arbitrary isomorphism, but only under central isomorphism. That's why they were an interesting example for the ANST paper.

Mike Shulman (May 22 2024 at 20:50):

So perhaps the definition is "non-categorical" in that sense. I was just thinking of the fact that it can be defined without reference to equality of objects.

John Baez (May 23 2024 at 15:32):

There's a tensor product of categories called the [[funny tensor product]] such that a separately functorial bifunctor from C,D to a category K is the same as a functor from the funny tensor product of C and D to K. The funny tensor product is a symmetric monoidal structure on the category Cat - in fact, one of the only two symmetric monoidal closed structures on the category Cat!

@Morgan Rogers (he/him) gave an example implying that the funny tensor product can't extend to a monoidal structure on the 2-category of categories, functors and natural transformations, because equivalent categories can have inequivalent funny tensor products.

John Baez (May 23 2024 at 15:37):

So, we can conclude that the other symmetric monoidal closed structure on Cat, namely the cartesian product, is the only one that extends to a monoidal structure on the 2-category of categories, functors and natural transformations!

Mike Shulman (May 23 2024 at 15:38):

I wonder if there are any other places in mathematics where the word "funny" has been given a precise meaning.

Morgan Rogers (he/him) (May 23 2024 at 15:46):

John Baez said:

Morgan Rogers (he/him) gave an example implying that the funny tensor product can't extend to a monoidal structure on the 2-category of categories, functors and natural transformations, because equivalent categories can have inequivalent funny tensor products.

I'd already forgotten that I did that... Someone could put that on the nLab page ;)

John Baez (May 23 2024 at 15:50):

Do it before you forget! :wink:

Valeria de Paiva (May 23 2024 at 16:12):

suggestion for a title: "A Tale of Two Tensors"

just kidding, but it would be nice to have it in the nLab.

Jules Hedges (May 23 2024 at 17:14):

John Baez said:

Morgan Rogers (he/him) gave an example implying that the funny tensor product can't extend to a monoidal structure on the 2-category of categories, functors and natural transformations, because equivalent categories can have inequivalent funny tensor products.

What is the consequence of this? That it's not possible to define "premonoidal natural transformations"?

Jules Hedges (May 23 2024 at 17:16):

Around here there's also [[sesquicategory]], which are to premonoidal categories as 2-categories are to monoidal categories, ie. it's like a 2-category but without the interchange law. Allegedly they are categories enriched in Cat with the funny tensor

Morgan Rogers (he/him) (May 23 2024 at 21:28):

John Baez said:

Do it before you forget! :wink:

Done. It's one of those cases where the simplest possible example of an equivalence gives a counterexample.

John Baez (May 24 2024 at 07:44):

Jules Hedges said:

Around here there's also [[sesquicategory]], which are to premonoidal categories as 2-categories are to monoidal categories, ie. it's like a 2-category but without the interchange law. Allegedly they are categories enriched in Cat with the funny tensor

Yes, the allegation is true. Relatedly, there are 3 important tensor products of 2-categories: the white tensor product (= funny tensor product, where you don't fill in the squares that get formed by pairs of morphisms), the Gray tensor product (where you fill them in, either with a 2-morphism or a 2-isomorphism), and the black tensor product (= cartesian product, where you fill them in with an equation, making the squares commute).

Mike Shulman (May 24 2024 at 07:52):

Although, as you alluded to in the corresponding parenthetical, there are actually 3 Gray tensor products, one where the morphism goes in each way and a third where it's invertible.

John Baez (May 24 2024 at 07:58):

Yes, so we've got a total of 5 tensor products of 2-categories here!

Martti Karvonen (May 24 2024 at 09:38):

Given that the funny tensor product doesn't extend to the 2-category Cat, I'd expect that some (at least the white tensor product) of these 5 tensor products fail to work for the 3-category of 2-categories (or perhaps issues come up already for 2-cells?). Is that the case?

Nathanael Arkor (May 24 2024 at 10:23):

A counterexample for even the 2-functoriality of the (lax/colax) Gray tensor product is given in this MathOverflow answer.

Mike Shulman (May 24 2024 at 15:11):

However, the lax Gray tensor product is a functor of "lax-Gray 3-categories" and dually, just by abstract enriched category theory.

Nathanael Arkor (May 24 2024 at 15:37):

To clarify, are you saying that, since the lax Gray tensor product forms a closed structure on the category 2-Cat, we can enrich in it, in which case 2-Cat becomes a (lax Gray)-enriched category, and the lax Gray tensor product is consequently also (lax Gray)-enriched?

Mike Shulman (May 24 2024 at 15:37):

Yes!

Mike Shulman (May 24 2024 at 15:37):

Although actually, I didn't check that that works in the usual way when the tensor product is non-symmetric, so it's possible I just lied.

Mike Shulman (May 24 2024 at 15:38):

Hmm, yes, I think I lied.

Mike Shulman (May 24 2024 at 15:39):

To make the tensor product an enriched functor on a closed monoidal category, you want $[A,B] \otimes [C,D] \to [A\otimes C, B\otimes D]$, which by adjunction is equivalent to $[A,B] \otimes [C,D] \otimes A \otimes C \to B\otimes D$, and the obvious thing to do is put together the evaluation maps $[A,B]\otimes A \to B$ and $[C,D]\otimes C \to D$, but it looks like to do that you have to permute $[C,D]$ past $A$.

Kevin Carlson (May 24 2024 at 18:29):

Martti Karvonen said:

Given that the funny tensor product doesn't extend to the 2-category Cat, I'd expect that some (at least the white tensor product) of these 5 tensor products fail to work for the 3-category of 2-categories (or perhaps issues come up already for 2-cells?). Is that the case?

Yeah, I'm also a little confused about how it can be that the white tensor product exists but the funny tensor product isn't 2-functorial on Cat, but haven't gotten a chance to actually try to work it out yet.

John Baez (May 24 2024 at 18:41):

@Kevin Carlson - When I said there's a white tensor product of 2-categories I didn't say this put a monoidal structure on the 2-category or 3-category 2Cat. My guess is that it only puts a monoidal structure on the 1-category 2Cat, just like the funny tensor product of 1-categories only puts a monoidal structure on the 1-category Cat, not the 2-category.

Mike Shulman (May 24 2024 at 18:42):

And just like the Gray tensor product is only on the 1-category 2Cat, as we just concluded.

John Baez (May 24 2024 at 18:45):

That breaks down already for the 2-category? For some reason I didn't see anyone concluding that.

Do you mean the "iso Gray tensor product" or the "lax Gray tensor product"?

Mike Shulman (May 24 2024 at 18:46):

Unless I misunderstood, Tim Campion's counterexample in the MO link works at the level of the 2-category. And he stated it only in the lax case, but I think it works in the iso case as well.

Kevin Carlson (May 24 2024 at 19:17):

Right, right, so as in Mike's Gray stuff, there's a closure on (the 1-category!) 2Cat whose exponential is the 2-category of 2-functors, unnatural transformations, and modifications (where I guess a modification between unnatural transformations is just a family of 2-morphisms satisfying no axioms), and if we set White to be 2-Cat with the white product, then the white product is a White-enriched functor but not a 2-functor. Something like that. Thanks John!

Mike Shulman (May 24 2024 at 19:18):

Right, because unlike Gray, White is symmetric.

Kevin Carlson (May 24 2024 at 19:18):

Luckily the white product is symmetric so that weird thing about the lax...yep!

Kevin Carlson (May 24 2024 at 19:19):

Pseudo-Gray is symmetric too, right, so that the pseudo-Gray product is a pseudo-Gray enriched functor?

Mike Shulman (May 24 2024 at 19:19):

Yes.

John Baez (May 24 2024 at 19:45):

Thanks for clarifying things, Mike and Kevin.

Right, right, so as in Mike's Gray stuff...

Do you mean John Gray? It would be great if there were three guys named Gray - Lax, Oplax and Pseudo - but I think there's just John.

Kevin Carlson (May 24 2024 at 19:46):

Haha, just meant the Gray-related comments Mike made, not crediting the Gray structure to Mike, pseudo-Mike, etc

John Baez (May 24 2024 at 19:49):

Oh wow, I misread that as "Mike Gray's stuff". :anguished:

John Onstead (May 24 2024 at 22:36):

I remember a discussion I had about this a while back. I was wondering if anyone had an answer to this...
Let's say nCat is the 1-category of n-categories and functors between them. What is the function f(n) that takes in n and outputs the number of tensor products on that category? For instance, f(1) = 2 (the funny and cartesian product), f(2) = 5 (the funny, cartesian, and the 3 Gray tensor products), etc. What is the general equation to calculate f(n) for a general n, and is this exponential, factorial, etc.? Or what is the OEIS sequence number?

John Baez (May 24 2024 at 23:13):

Since there are infinitely many symmetric monoidal structures on 0Cat, we'll only get a fun game if we restrict to symmetric monoidal closed structures. Then we get f(1) = 2 by a theorem of Foltz, Lair and Kenny, and it seems easy to show f(0) = 1 since such a tensor product distributes over colimits and every set is a coproduct of copies of the terminal set. I don't really know that f(2) = 5, just that f(2) $\ge$ 5, but it should be possible to compute the actual answer.