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: naming homotopified double categories

David Corfield (Mar 27 2025 at 09:03):

I began an nLab stub for [[double infinity-categories]] (additions very welcome). But the question arose as to the best name for them. At the moment the choices seem to be 'double $\infty$-category' or 'double $(\infty, 1)$-category'. But what's the logic behind the choice? Why not '$\infty$-double category'?

Jonas Frey (Mar 27 2025 at 09:50):

I like infty-double-category in analogy to infty-2-category, as Urs says on the nforum

James Deikun (Mar 27 2025 at 10:09):

I'm not even sure the definition of double $\infty$-category in the literature is "correct", it should really include vertical completeness, otherwise there's an unnecessary degree of freedom similar to the one in non-complete Segal spaces.

James Deikun (Mar 27 2025 at 10:14):

That being said, the construction seems to be better described by "double $(\infty,1)$-category since both directions are built like $(\infty,1)$-categories rather than building a definition of double category first and then homotopically weakening it.

Jonas Frey (Mar 27 2025 at 15:02):

The question of vertical/horizontal completeness of higher double categories was discussed by @Nima Rasekh last year at HoTT-UF in a talk on joint work with Niels Van Der Weide, Benedikt Ahrens and Paige Randall North

https://hott-uf.github.io/2024/slides/Rasekh.pdf

Jonas Frey (Mar 27 2025 at 15:08):

One point that came up that I wasn't aware of is that one can view non-completeness at least in one direction as a feature, eg for rings we have the notion of isomorphism and of Morita equivalence, and they can't both coincide with the internal type of identification in the type of objects

Nima Rasekh (Mar 27 2025 at 15:09):

James Deikun said:

I'm not even sure the definition of double $\infty$-category in the literature is "correct", it should really include vertical completeness, otherwise there's an unnecessary degree of freedom similar to the one in non-complete Segal spaces.

Thanks @Jonas Frey for the shout out!
@James Deikun I think the "correct" notion is somewhat tricky.

• If you generalize naively from strict to non-strict, then the intuition might be to do \infty-category objects internal to \infty-categories, which unwinds to double complete Segal spaces (i.e. complete in all directions). That has the flaw that the space of objects is over-determined: it is equivalent to the space of horizontal equivalences and vertical equivalences. In particular it will lack a key example like Prof.
• One solution is to weaken in one direction, which is particularly suitable for double categories that are naturally pseudo double categories (i.e that happen to be strict in one direction). But in general this definition of completeness is annoyingly non-symmetric.
• A better --symmetric-- analogue might be "gregarious completeness", in the sense we do in the paper. The actual \infty-version is WIP by some people (I think). Here is a talk about it: https://acmbl.github.io/greg_slides.pdf (note Prof is in fact gregarious complete so at least it would be an example)

James Deikun (Mar 27 2025 at 15:30):

It feels like both "vertically complete" and "gregarious complete" are kind of non-comparable in how "good" they are. Vertically complete seems more appropriate for cases where symmetry is not a concern while gregarious complete is better when it is. Fortunately they seem to coincide for equipments!

Nima Rasekh (Mar 27 2025 at 15:32):

Yeah, I think that's the suprising gist of it, unlike categories and bicategories, where there is a "most general" notion of completeness and corresponding equivalence, there isn't one for double categories.
But yes, for many relevant examples that's fine, and they happen to coincide as we prove in the paper.

Kevin Carlson (Mar 27 2025 at 15:46):

Nima, when you say "non-symmetric", do you mean under transposition? I'm sorry to ask before having actually looked into any of this (but I'm doing so anyway :upside_down: )

Mike Shulman (Mar 27 2025 at 16:29):

I don't find non-symmetry under transposition to be annoying. It seems to me that that's probably the $\infty$-analogue of the fact that so many important double 1-categories are strict in one direction but not the other, i.e. for "framed $\infty$-bicategories" or "$\infty$-equipments".

Although the gregarious-complete double $\infty$-categories would probably be the analogue both of double 1-categories that are strict in both directions (which are fairly common) and those that are weak in both directions (which are both rare and hard to define).

Nima Rasekh (Mar 27 2025 at 18:14):

Kevin Carlson said:

Nima, when you say "non-symmetric", do you mean under transposition? I'm sorry to ask before having actually looked into any of this (but I'm doing so anyway :upside_down: )

When I say non-symmetric I simply mean in that definition the completeness (or univalence) condition is only about one direction, meaning the space of object is equivalent to the space of horizontal equivalences. There is no connection between vertical equivalences and objects. This was motivated by the question which completeness condition is suitable when defining double oo-categories.

Kevin Carlson (Mar 27 2025 at 18:17):

Yeah, I see how the answer is sort-of-yes, but sort of that the frame shifts when thinking HoTTotopically.

Nima Rasekh (Mar 27 2025 at 18:17):

Mike Shulman said:

I don't find non-symmetry under transposition to be annoying. It seems to me that that's probably the $\infty$-analogue of the fact that so many important double 1-categories are strict in one direction but not the other, i.e. for "framed $\infty$-bicategories" or "$\infty$-equipments".

Although the gregarious-complete double $\infty$-categories would probably be the analogue both of double 1-categories that are strict in both directions (which are fairly common) and those that are weak in both directions (which are both rare and hard to define).

I think, particularly in a set theoretical setting, this is largely correct.

However, if one is in a univalent setting, then there are in fact natural "doubly weak" examples, such as Prof: the double category of univalent categories, functors and profunctors. In this case, both functors and profunctors are part of a bicategorical structure, but neither are part of a strict 2-category (as observed here https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.5).

Mike Shulman (Mar 27 2025 at 18:50):

Well, yes, in a univalent setting there aren't even any strict 2-categories to speak of. I was indeed thinking only of set-theoretic foundations.

Nima Rasekh (Mar 27 2025 at 18:55):

Mike Shulman said:

Well, yes, in a univalent setting there aren't even any strict 2-categories to speak of. I was indeed thinking only of set-theoretic foundations.

Well, if one takes setcategories, then they do form a univalent category, and so also a univalent 2-category (if one add natural transformations), meaning if one also adds profunctors one gets a pseudo double category (so functors compose strictly, pseudo functors weakly).

In the univalent setting I guess, it depends with what type of object one starts.

Mike Shulman (Mar 27 2025 at 18:56):

Okay, but there aren't really any set-categories to speak of, so that's not much of an example. (-:

Jonas Frey (Mar 27 2025 at 18:57):

What do you mean by set-categories?

Nima Rasekh (Mar 27 2025 at 18:58):

Jonas Frey said:

What do you mean by set-categories?

It's just a category in which the objects are a set.

Jonas Frey (Mar 27 2025 at 18:59):

Ok but are they also supposed to be univalent?

Nima Rasekh (Mar 27 2025 at 18:59):

Jonas Frey said:

Ok but are they also supposed to be univalent?

No, not necessarily.

Jonas Frey (Mar 27 2025 at 19:01):

Ok then I don't agree with Mike's statement that "there aren't really any", at least if we assume that all types admit covers by 0-types. But in any case they're artificial if we assume that Set is univalent.

Nima Rasekh (Mar 27 2025 at 19:02):

Mike Shulman said:

Okay, but there aren't really any set-categories to speak of, so that's not much of an example. (-:

Well the category of setcategories is defined indepedent of particular examples.
I guess your point is that most categories we would construct start with the universe of sets, in which case it would be univalent?

On the other hand, there are at least some examples even if we focus on univalent ones, namely univalent categories without automorphisms, so posets maybe or Delta.

Nima Rasekh (Mar 27 2025 at 19:04):

I mean the point of setcategories is that they are supposed to occur when we care about categories up to isomorphisms, instead of equivalences. I agree this is not what we usually do, but it does happen sometimes.

Mike Shulman (Mar 27 2025 at 19:29):

Jonas Frey said:

if we assume that all types admit covers by 0-types

Why would you assume that?

Jonas Frey (Mar 27 2025 at 19:32):

Well, I would say that's "classical" metatheory and in general I don't mind classical metatheory.

On the other hand, I also like the philosophical point of view that size and h-level grow in parallel.

Jonas Frey (Mar 27 2025 at 19:42):

The latter is probably not consistent with the existence of truncations, so probably not what you had in mind.

But anyways, even without assuming covers by 0-types we get interesting strict 1-categories, in terms of generators and relations

Mike Shulman (Mar 27 2025 at 20:11):

Jonas Frey said:

Well, I would say that's "classical" metatheory and in general I don't mind classical metatheory.

I don't agree that that's metatheory. It's an axiom of the theory.

Mike Shulman (Mar 27 2025 at 20:12):

There are $\infty$-topos models (constructed in a classical metatheory) in which it fails.

Mike Shulman (Mar 27 2025 at 20:14):

I admit it was an exaggeration to say there aren't any strict categories "to speak of". But my main point was that the notion of "strict 2-category" is not very important or useful in UF, because the primary 2-categories that 2-category theory is aimed at are not strict, and that's because the primary 1-categories that 1-category theory is aimed are not strict.

Jonas Frey (Mar 27 2025 at 20:24):

Which theory is meta is a matter of perspective, but I guess I'm promoting Voevodsky's viewpoint of an axiomatics of HoTT that is "as classical as possible". This is not supposed to capture the logic of an arbitrary infty-topos, but specifically the infty-topos of spaces (eg in classical set theoretic metatheory)

Jonas Frey (Mar 27 2025 at 20:31):

So I guess my answer to your question "why would you assume that?" is "because in my classical mental model I think it's true".

Jonas Frey (Mar 27 2025 at 20:42):

I agree that constructing strict $1$-cats via set-covers is artificial and not "what category theory is about"

Mike Shulman (Mar 27 2025 at 21:50):

I don't see any way that the theory in which we're doing mathematics (here, category theory) could be called meta.

But okay, if you want to be totally classical that's fine.

Jonas Frey (Mar 27 2025 at 22:05):

I agree with you that "meta theory" doesn't make sense without "object theory", and that I chose my words sub-optimally here. Maybe "foundation" makes more sense.

But since you're referring to category theory, I'll have to disagree and say hat this is the object theory, and the meta theory is type theory. (forget the last part, I misread your statement as saying that "category theory" is the foundation)

Mike Shulman (Mar 28 2025 at 01:14):

Ah, I did phrase that sloppily, sorry.