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.
Matteo Capucci (he/him) (Apr 12 2024 at 13:24):IMO, the tight direction in double cats is the one deputed for morphological comparison, including isomorphism checks
Nathanael Arkor (Apr 12 2024 at 13:56):Graham Manuell said:
I don't know if this is related or not, but I never know how to think of isomorphisms in double categories. Usually when two objects are isomorphic I think of them as the same thing, but what if they are, say, horizontally isomorphic, but not vertically isomorphic?
Surely there's nothing that can be said in general? In an arbitrary double category, isomorphism in one direction may look entirely different to isomorphism in the other direction, so it really depends on the double category in question.
Nathanael Arkor (Apr 12 2024 at 14:00):Graham Manuell said:
Relatedly there doesn't appear to be one accepted notion of equivalence of double categories?
There's a 2-category of double categories and pseudo double functors, and one can consider an equivalence in this 2-category. If someone told me two double categories were equivalent, this is what I'd assume they meant. For instance, this is the notion of equivalence used in Grandis and Paré's strictification theorem for pseudo double categories. What other notions of equivalence have you encountered?
Nathanael Arkor (Apr 12 2024 at 14:02):(Note that it really is appropriate to consider the 2-category of double categories and pseudo double functors, rather than lax or colax double functors, since any equivalence can be improved to an adjoint equivalence in both directions, from which you can deduce that both adjoints must be both lax and colax, hence pseudo.)
Graham Manuell (Apr 12 2024 at 15:16):Nathanael Arkor said:
Surely there's nothing that can be said in general? In an arbitrary double category, isomorphism in one direction may look entirely different to isomorphism in the other direction, so it really depends on the double category in question.
This is entirely possible, but where does this leave us? Are general double categories just bad?
Graham Manuell (Apr 12 2024 at 15:16):Nathanael Arkor said:
There's a 2-category of double categories and pseudo double functors, and one can consider an equivalence in this 2-category.
It's more like there is a double-categories-enriched-category of double categories, no? You can use either horizontal or vertical transformations. I can't say off the top of my head the different notions of equivalence I've seen, but at least there are several different model structures people have considered that have different notions of weak equivalence.
Nathanael Arkor (Apr 12 2024 at 15:19):This is entirely possible, but where does this leave us? Are general double categories just bad?
This seems an odd question. Certainly if you want isomorphism in both directions to be related, then you want something stronger than an arbitrary double category. But I don't see why it should be considered a weakness that isomorphism in both directions can behave differently.
Nathanael Arkor (Apr 12 2024 at 15:22):You can use either horizontal or vertical transformations.
You can, but this seems a bit like saying that there isn't one accepted notion of equivalence of categories, because you can consider both equivalence and Morita equivalence. Rather, they are two different but related concepts, and the notion that is appropriate depends on the context. Taking the tight transformations gives the strictest notion of equivalence, and it is my experience that this is usually the appropriate one. But I'm not familiar with the model structure literature.
Graham Manuell (Apr 12 2024 at 15:22):Well my original question was how to think about such things. It feels like there should be some way to know when two objects are actually the same.
Graham Manuell (Apr 12 2024 at 15:22):How do/would people deal with double categories in homotopy type theory?
Nathanael Arkor (Apr 12 2024 at 15:22):Perhaps you can give some examples of double categories you have in mind, and how isomorphism behaves unexpectedly in them?
Graham Manuell (Apr 12 2024 at 15:26):I don't really know any concrete examples that aren't proarrow equipments, unfortunately. Perhaps you are right that thinking about one would be a good start.
Graham Manuell (Apr 12 2024 at 15:28):Nathanael Arkor said:
Taking the tight transformations gives the strictest notion of equivalence, and it is my experience that this is usually the appropriate one. But I'm not familiar with the model structure literature.
Are you you restricting the class of double categories here? Otherwise I don't know why one direction would be stricter than the other?
Graham Manuell (Apr 12 2024 at 15:33):Hmm. Or perhaps "companion pairs of isomorphisms" are the 'right' strict notion of isomorphism in general?
Mike Shulman (Apr 12 2024 at 15:56):There is, in fact, a general notion of "isomorphism" that can be defined generically across all higher-dimensional structures. It specializes to ordinary isomorphism in categories, to ordinary equivalence in 2-categories, and so on. In double categories, it specializes to a companion pair of equivalences, a.k.a. a "gregarious equivalence". This is developed in the context of HoTT in the monograph The Univalence Principle by Ahrens, North, Tsementzis, and myself.
Mike Shulman (Apr 12 2024 at 15:59):The double categories in which tight isomorphisms, or tight equivalences, are the "right" notion of equivalence are usually those that are at least "isofibrant", so that every tight equivalence has a loose companion and therefore induces a gregarious equivalence. And conversely, of course, every gregarious equivalence has an underlying tight equivalence.
Notification Bot (Apr 12 2024 at 15:59):17 messages were moved here from #theory: category theory > Cat(Mon(Cat)) vs Mon(Cat(Cat)) by Mike Shulman.
Nathanael Arkor (Apr 12 2024 at 16:41):Graham Manuell said:
Nathanael Arkor said:
Taking the tight transformations gives the strictest notion of equivalence, and it is my experience that this is usually the appropriate one. But I'm not familiar with the model structure literature.
Are you you restricting the class of double categories here? Otherwise I don't know why one direction would be stricter than the other?
Ah, yes, I meant in the context of pseudo double categories, sorry.
Mike Shulman (Apr 12 2024 at 16:47):You also need the pseudo double categories to be at least "isofibrant" (loose companions for tight isomorphisms) if you want equivalence using tight transformations to be "strictly stricter" than other notions in the sense that it implies them.
Graham Manuell (Apr 12 2024 at 19:08):Mike Shulman said:
There is, in fact, a general notion of "isomorphism" that can be defined generically across all higher-dimensional structures. It specializes to ordinary isomorphism in categories, to ordinary equivalence in 2-categories, and so on. In double categories, it specializes to a companion pair of equivalences, a.k.a. a "gregarious equivalence". This is developed in the context of HoTT in the monograph The Univalence Principle by Ahrens, North, Tsementzis, and myself.
Thanks! This is exactly what I was looking for.
Oscar Cunningham (Apr 14 2024 at 10:32):Sometimes people think of an ordinary category as being the horizontal part of a double category with only identity morphisms vertically. In particular categories over your original category are displayed by lax morphisms from this double category into . But this way of viewing categories as double categories sends equivalent categories to inequivalent double categories. Is there a version of this story that respects equivalence?
Mike Shulman (Apr 14 2024 at 15:32):I don't think so, because lax functors also don't respect equivalence.