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: (∞, ∞)

sarahzrf (Jun 02 2020 at 00:18):

Is there a such thing as an (∞, ∞)-category?

And if so, how on earth do you define what an equivalence in one is? Some kind of coinduction?

Nathanael Arkor (Jun 02 2020 at 00:22):

Yes. Some people call these $\omega$-categories, to distinguish them from $(∞, 1)$-categories.

Dan Doel (Jun 02 2020 at 00:23):

Aren't such things the goal of the 'type theory for $\infty$-categories' stuff? Like, every type has a directed path type, and if there is no iteration of the path type that automatically has inverses, then it's an $(\infty,\infty)$-category?

Nathanael Arkor (Jun 02 2020 at 00:24):

I think there are both inductive and coinductive variants, though there's not yet one agreed-upon notion, as I understand it.

Dan Doel (Jun 02 2020 at 00:24):

Similar to how some types can fail to be n-truncated for any n?

Dan Doel (Jun 02 2020 at 00:26):

I don't know what equivalence looks like in that setting, though.

Dan Doel (Jun 02 2020 at 00:30):

Also, I think ω-category originally refers to strict $\infty$-categories, which is why that page is talking about weak ω-categories. And for some reason, the name $\infty$ was popularized as the primary name for the weak version.

Nathanael Arkor (Jun 02 2020 at 00:31):

Unfortunately, $\infty$-category has also been popularised as a shorthand for $(\infty, 1)$-categories.

Dan Doel (Jun 02 2020 at 00:38):

Hmm.

Soichiro Fujii (Jun 02 2020 at 02:34):

Equivalences in $(\infty,\infty)$-categories (= weak $\omega$-categories) can be defined coinductively.

There are several definitions of weak $\omega$-categories, but in many cases at least the following conditions are satisfied (this is certainly true for Batanin’s and Leinster’s definitions, and presumably for many other algebraic definitions):

• Any weak $\omega$-category $\mathcal{A}$ has an underlying globular set $|\mathcal{A}|$. For any $n\geq 1$ and any $n$-cell $a$ in $|\mathcal{A}|$, write $a\colon x\to y$ if $x$ (resp. $y$) is the $(n-1)$-dimensional source (resp. target) of $a$.
• For any $n\geq 1$ and $(n-1)$-cell $x$ (in $|\mathcal{A}|$), there is a specified $n$-cell $i_x\colon x\to x$ (“identity on $x$”).
• For any $n\geq 1$ and two $n$-cells $a\colon x\to y$ and $b\colon y\to z$, there is a specified $n$-cell $b\circ a\colon x\to z$ (“composite”).

As Cheng observed, one can define equivalences in $\mathcal{A}$ (coindutively) from just these structures. That is: for $n\geq 1$, an $n$-cell $a\colon x\to y$ is an equivalence $n$-cell if there exist an $n$-cell $b\colon y\to x$ and equivalence $(n+1)$-cells $\eta\colon i_x\to b\circ a$ and $\varepsilon \colon a\circ b\to i_y$.

By the nature of coinductive definition, in order to verify that an $n$-cell is an equivalence, it suffices to find a set $W$ of cells (of various dimensions) containing that $n$-cell, such that for all $k\geq 1$, whenever a $k$-cell $a\colon x\to y$ is in $W$, there are some $k$-cell $b\colon y\to x$ and $(k+1)$-cells $\eta\colon i_x\to b\circ a$ and $\varepsilon \colon a\circ b\to i_y$ in $W$. (Cheng calls such a $W$ a set of witnesses.)

John Baez (Jun 02 2020 at 05:51):

Understanding weak $\omega$-categories is, in my opinion, one of the main goals of higher category theory.

John Baez (Jun 02 2020 at 05:52):

The Batanin-Leinster approach is good for people who like globe-shaped cells.

Rune Haugseng (Jun 02 2020 at 08:04):

Nowadays it is easy to define (∞, ∞)-categories within the world of ∞-categories (i.e. (∞,1)-categories): if Cat(∞,n) is the ∞-category of (∞,n)-categories then there is a "forgetful" functor Cat(∞,n) -> Cat(∞,n-1) that forgets the non-invertible n-morphisms (this is the right adjoint to the inclusion of (∞,n-1)-categories into (∞,n)-categories). Then we can simply define the ∞-category Cat(∞,∞) of (∞,∞)-categories as the limit of Cat(∞,n) (in the ∞-category of (large) ∞-categories).

Rune Haugseng (Jun 02 2020 at 08:07):

If we use Rezk's definition of (∞,n)-categories as presheaves on a category $\Theta_{n}$ valued in the ∞-category of spaces (∞-groupoids) satisfying Segal and completeness conditions, then we can describe Cat(∞,∞) similarly as presheaves of spaces on the colimit $\Theta_{\infty}$ of the categories $\Theta_{n}$ along certain inclusions, again with Segal and completeness conditions.

Rune Haugseng (Jun 02 2020 at 08:13):

Since limits of ∞-categories are easy to describe, we can also say: an (∞, ∞)-category is a sequence $(C_n)_{n \in \mathbb{N}}$ where $C_n$ is an (∞,n)-category, and $C_{n-1}$ is obtained by forgetting the non-invertible n-morphisms in $C_n$. A morphism is similarly a sequence of functors of (∞,n)-categories, and it will be an equivalence of (∞,∞)-categories precisely when each functor in the sequence is an equivalence of (∞,n)-categories.

Rune Haugseng (Jun 02 2020 at 08:21):

In particular, the equivalences here will not be the coinductive ones, though one could presumably just localize to invert them. I don't know the original motivation for that definition, but note that it has some bizarre (and to my mind undesirable) consequences: an (∞, ∞)-category where every i-morphism has adjoints for all i is coinductively equivalent to an ∞-groupoid (because using the adjoints at all levels you can enhance every i-morphism to a coinductive equivalence) - this means that if you invert coinductive equivalences there is no longer a forgetful functor taking (∞,∞)-categories to their underlying (∞,n)-categories, since it won't preserve equivalences!

Amar Hadzihasanovic (Jun 02 2020 at 09:08):

I think that for someone who accepts the coinductive definition of equivalences, an $(\infty,\infty)$-category where all morphisms have adjoints is an $\infty$-groupoid.

I believe there's a bit of a cultural divide here: I bet that anyone who approaches higher categories from a broadly “logic/CS” viewpoint will find it easier to understand the coinductive definition. The reason I believe that, eventually, higher (in the $(\infty,\infty)$ sense) categories will conquer theoretical CS is that they provide ways to deal with algebraic structures in an “equation-free”/“quotient-free” way, and for a CS theorist equations lead to word problems lead to undecidability. The coinductive model of equivalences comes precisely as the limit of a process of eliminating the equations of 'invertibility' by replacing them with generators in a higher dimension, in order to have “equation-free invertibility”.

On the other hand, I imagine that this concern is quite remote for a homotopy theorist/algebraic geometer whose bread and butter is localisation. :)

Oscar Cunningham (Jun 02 2020 at 10:35):

Amar Hadzihasanovic said:

I think that for someone who accepts the coinductive definition of equivalences, an $(\infty,\infty)$-category where all morphisms have adjoints is an $\infty$-groupoid.

Does that mean that the inductive and coinductive definition give genuinely different definitions of what an $(\infty,\infty)$-category is?

Oscar Cunningham (Jun 02 2020 at 10:35):

Also does it tell us something about cobordisms, via the cobordism hypothesis?

Dan Doel (Jun 02 2020 at 14:48):

(I'm no expert, but) it seems like the mismatch is that the inductive version is like an $\infty$ version of strict categories. Like, when you forget non-invertible morphisms, this is because you have pre-chosen which morphisms are 'really' invertible via the $\infty$-groupoid structure in common at all levels. So, the higher levels of arrows are not determining which things are invertible.

The coinductive version is the 'univalent' one, I think. There can be presentations where looking at any finite level will not tell you all the invertible arrows, because each higher level adds the mediating arrows. The point of the coinductive version would be that the arrows really determine what is invertible, not some prior groupoid structure.

Oscar Cunningham (Jun 02 2020 at 15:02):

Thanks, that helps.

Rune Haugseng (Jun 02 2020 at 16:09):

The inductive and coinductive approaches are definitely different. I guess the canonical example would be the cobordism (∞, ∞)-category: In the inductive version this combines all the cobordism (∞, n)-categories for all n, but since all n-morphisms have adjoints the coinductive version is just an ∞-groupoid, presumably the one you obtain by inverting everything in the cobordism (∞,n)-category and taking the colimit over n (which Schommer-Pries proved is the infinite loop space of a cobordism spectrum, if I'm not mixing things up). Note that you definitely can't recover the cobordism (∞,n)-category from the latter!

Rune Haugseng (Jun 02 2020 at 16:13):

I would say this means the coinductive definition doesn't match my intuition for what (∞, ∞)-categories should be, but to be fair I don't think I know of any real applications of (∞, ∞)-categories (as opposed to (∞, n)-categories for finite n). I would be very interested to know what the expected uses of such objects are in CS/logic! Are there any examples there that ought to form (∞, ∞)-categories in the coinductive sense?

Dan Doel (Jun 02 2020 at 17:26):

I don't know of applications of the directed versions, but it seems to be just applying the same methodology as for $\infty$-groupoids and HoTT. You don't get to 'forget' structure above a certain level to go back from an $\infty$-groupoid to an $n$-groupoid, because only things that are inverses up to on-the-nose equality really count at some point.

And there are clear applications for $\infty$-groupoids working that way. As mentioned, it makes things involving equations/quotients tractable in a way that they normally aren't, because the 'equality' proofs contain information that helps solve the normally intractable problems.

The normal example I use is exhibiting an inverse to a bijective function. Arguably the most faithful way to state that a function $f : A → B$ is surjective is as $\Vert Π y. Σ x. y = f x \Vert$, where the $\Vert$ is propositional truncation. The un-truncated type is sufficient to produce a function $B → A$, but in general it is not a proposition, hence the truncation. Previous approaches to this sort of 'squash' type are just to make it computationally irrelevant, which means that you are only at liberty to eliminate it into other distinguished irrelevant types.

However, the way you exhibit the inverse function is to show that $f$ being injective implies that its fibers are (homotopy) propositions, so we are at liberty to eliminate from the truncation into them. The fibers aren't computationally irrelevant, though, because we want to assemble them back into a computationally relevant function (that was the original goal). The way that this works is that the 'equality' proofs from propositional extensionality actually carry the information on how to exhibit witnesses of one proposition from witnesses of the other. So in this case, how to compute values of the fiber type.

Dan Doel (Jun 02 2020 at 17:35):

The old approach is limited because merely knowing that a potential inverse exists is not generally enough information to figure out what it is. It is important that the propositions actually carry computationally relevant information, and perhaps even information that isn't equal 'on the nose', but merely up to higher dimensional bits of information.

But then, there isn't really a reason that this information has to be invertible/symmetric, in principle, so you could instead do the $(\infty,\infty)$-category thing, where all these things are directed, and two things are equivalent only if there are pairs of bits of information that are equivalent up to pairs of bits of information, that are ....

Reid Barton (Jun 02 2020 at 17:35):

The inclusion of (∞,n-1)-categories into (∞,n)-categories also has a left adjoint, given by freely adjoining inverses to the n-morphisms. Is the "coinductive definition" what you get by taking the inverse limit of these left adjoints? (It's been a long time since I thought about this stuff too, but this sounds familiar.)

Amar Hadzihasanovic (Jun 02 2020 at 17:38):

Reid, yes, that's the one.
This MO answer by Chris Schommer-Pries recaps the situation.

Reid Barton (Jun 02 2020 at 17:39):

From a homotopy theory/higher category theory/whatever point of view, it's easier to justify taking the other limit, the one Rune described, but at least you can write down both

John Baez (Jun 02 2020 at 17:40):

Rune Haugseng said:

In particular, the equivalences here will not be the coinductive ones, though one could presumably just localize to invert them. I don't know the original motivation for that definition, but note that it has some bizarre (and to my mind undesirable) consequences: an (∞, ∞)-category where every i-morphism has adjoints for all i is coinductively equivalent to an ∞-groupoid (because using the adjoints at all levels you can enhance every i-morphism to a coinductive equivalence)

Yes, this used to annoy me a lot. I wanted an (∞, ∞)-category of framed cobordisms where every i-morphism has adjoints for all i, and I wanted an ∞-groupoid corresponding to $\Omega^\infty S^\infty$, and I wanted a map from the former to the latter given by the Thom-Pontryagin construction, which turned adjoints into equivalences... but I didn't want this map to be an equivalence. Then Eugenia Cheng wrote a paper about how (∞, ∞)-categorries where every i-morphism has adjoints for all i are automatically ∞-groupoids. That annoyed me because it went against my intuitions.

Around this time I stopped working on higher categories (for completely different reasons).

John Baez (Jun 02 2020 at 17:41):

So, I never really noticed the resolution of this sort of issue.

Tobias Fritz (Jun 02 2020 at 17:57):

Eugenia Cheng's result sounds intriguing! I don't really understand higher duals, so perhaps you can explain why this doesn't contradict the existence of monoidal categories with duals that aren't just 2-groups?

John Baez said:

So, I never really noticed the resolution of this sort of issue.

Is there a known resolution?

Oscar Cunningham (Jun 02 2020 at 17:59):

Tobias Fritz said:

Eugenia Cheng's result sounds intriguing! I don't really understand higher duals, so perhaps you can explain why this doesn't contradict the existence of monoidal categories with duals that aren't just 2-groups?

Oscar Cunningham (Jun 02 2020 at 17:59):

Because in a monoidal category with duals the morphisms don't have adjoints. Only the objects do. But if everything has adjoints then you get a groupoid. At least according to the coinductive definition, which I think the consensus is now turning against.

Tobias Fritz (Jun 02 2020 at 18:02):

D'oh, of course, thanks! Somehow I wasn't thinking properly, and under the impression that everything above stuff with duals was already invertible. So then a higher category of cobordisms has duals in all dimensions except one? Weird.

Rune Haugseng (Jun 02 2020 at 18:06):

Dan Doel said:

I don't know of applications of the directed versions, but it seems to be just applying the same methodology as for $\infty$-groupoids and HoTT. You don't get to 'forget' structure above a certain level to go back from an $\infty$-groupoid to an $n$-groupoid, because only things that are inverses up to on-the-nose equality really count at some point.

The inductive definition (at least as I stated it above) doesn't involve forgetting/truncating to some finite level though, it starts with $\infty$-groupoids and builds up from there. Taking, say, the underlying $\infty$-groupoid of an $(\infty,n)$-category is certainly a well-behaved, reasonable operation.

Rune Haugseng (Jun 02 2020 at 18:12):

Amar Hadzihasanovic said:

Reid, yes, that's the one.
This MO answer by Chris Schommer-Pries recaps the situation.

If I remember correctly I actually heard this conjecture was disproved by Thomas Nikolaus some years ago, but I don't think the proof was ever written up...

Reid Barton (Jun 02 2020 at 18:13):

What's the conjecture?

Rune Haugseng (Jun 02 2020 at 18:14):

That taking the limit of the right adjoints from (∞,n)-cat.s to (∞,n-1)-cat.s and then inverting the coinductive equivalences gives the limit along the left adjoints

Reid Barton (Jun 02 2020 at 18:15):

So, does that mean there are actually three (or more?) candidate definitions?

Dan Doel (Jun 02 2020 at 18:17):

Your response doesn't appear to address my comparison.

Rune Haugseng (Jun 02 2020 at 18:18):

I guess so, though if it's true that these two are different I'm not sure anybody wants to look at the limit along the left adjoints

Amar Hadzihasanovic (Jun 02 2020 at 18:20):

Rune Haugseng said:

That taking the limit of the right adjoints from (∞,n)-cat.s to (∞,n-1)-cat.s and then inverting the coinductive equivalences gives the limit along the left adjoints

Forgive the ignorance, but Schommer-Pries only says he believes the left-adjoint/coinductive one is “a localisation” of the right adjoint/inductive one -- is “inverting the coinductive equivalences” the only sensible possibility?

Oscar Cunningham (Jun 02 2020 at 18:25):

Tobias Fritz said:

So then a higher category of cobordisms has duals in all dimensions except one? Weird.

That makes sense to me. If two morphisms are dual then the unit and counit of the adjunction are one dimension higher. So if you kill everything above a given dimension then you'll also kill the adjunctions one level down.

Rune Haugseng (Jun 02 2020 at 18:26):

It's possible it is some other localization, I guess (I have never thought about this).

John Baez (Jun 02 2020 at 18:27):

Tobias Fritz said:

John Baez said:

So, I never really noticed the resolution of this sort of issue.

Is there a known resolution?

I thought that's what @Rune Haugseng just explained in the comment I was commenting on.

Rune Haugseng (Jun 02 2020 at 18:27):

But is there then any reason to think it's connected to the coinductive approach to (∞, ∞)-categories?

Amar Hadzihasanovic (Jun 02 2020 at 18:44):

I really don't know. My knowledge of the “homotopy theory of higher categories” is not deep enough.

Amar Hadzihasanovic (Jun 02 2020 at 18:46):

I have worked on the 'coinductive' version coming from a CS/higher-dimensional rewriting perspective, where, like Dan, I think it is quite a natural one.

Rune Haugseng (Jun 02 2020 at 19:18):

I guess the coinductive definition only produces "weird" results if you go all the way to (∞, ∞)-categories - if you restrict to (∞, n)-categories for any finite n it seems like it should agree with the usual notion of equivalence

Dan Doel (Jun 02 2020 at 19:19):

Here is, perhaps, a way of reformulating my comparison, although maybe I'm off base.

Taking the underlying set of an n-groupoid is 'certain a well-behaved, reasonable operation' if your mindset is set theory. But (correct me if I'm wrong), it is not correct to say that equivalence in an $\infty$-groupoid is the same as equivalence in every one of the n-groupoids you get by forgetting its higher structure. So, you are using the coinductive notion of equivalence for $\infty$-groupoids, not the inductive version where they're 'really' sets with extra structure.

So, why then would you not use the coinductive notion of equivalence in an $(\infty,\infty)$-category? Why coinductive for the undirected stuff and inductive for the directed stuff? Moreover, this seems to negate the description of $(\infty,n)$-categories as $\infty$-categories where all the arrows above level $n$ have inverses up to the next level, because only some of the 'arrows' count for determining inverses.

Reid Barton (Jun 02 2020 at 19:38):

I'm having trouble with the first paragraph (every morphism in an $\infty$-groupoid is an equivalence by definition), but assuming you mean $(\infty,1)$-category, then for anything that could be reasonably considered an "underlying $(2,1)$-category" of an $(\infty,1)$-category, a 1-morphism being an equivalence is the same as it being an equivalence already in the underlying $(2,1)$-category. So there is no difference between inductive or coinductive there, if I understand correctly.

Rune Haugseng (Jun 02 2020 at 19:41):

I also don't understand what you mean by defining an equivalence in an $\infty$-groupoid. Do you have some specific model of these in mind (that isn't Kan complexes)? (If you mean an equivalence between $\infty$-groupoids then you can detect these on underlying n-groupoids for all n, if we take underlying to mean the truncation to an n-groupoid, since that still gives you all the homotopy groups.)

Dan Doel (Jun 02 2020 at 19:47):

Truncation is freely adding things, not removing them, so to me that is just highlighting the fact that you're treating the category case differently. :slight_smile:

Rune Haugseng (Jun 02 2020 at 19:49):

The second point I think makes sense - I'd say there are two things we might expect for (∞, ∞)-categories: that an equivalence is a morphism that has inverses at all levels, and that if we have a sequence of $(\infty,n)$-categories $C_n$ such that $C_{n-1}$ is the underlying $(\infty,n-1)$-category of $C_n$, then we can make an $(\infty,\infty)$-category that has $C_n$ as its underlying $(\infty,n)$-category for all n. Unfortunately they can't both be true at once.

Rune Haugseng (Jun 02 2020 at 19:51):

Dan Doel said:

Truncation is freely adding things, not removing them, so to me that is just highlighting the fact that you're treating the category case differently. :slight_smile:

I don't understand this: in what sense is taking, say, $\pi_0$ of an $\infty$-groupoid "freely adding things"?

Dan Doel (Jun 02 2020 at 19:57):

I think what I mean in the first paragraph is when we consider two objects of an $\infty$-groupoid to be equivalent. The answer is if there is a map between them, which in an $\infty$-groupoid necessarily has all higher maps. But if you just remove structure above some point and only consider composition up to set equality at the highest level, you may have removed the structure that actually makes things at the highest level inverses.

Amar Hadzihasanovic (Jun 02 2020 at 19:59):

Let me try to rephrase what Dan is saying: I know this for the case of strict $n$-groupoids but I suppose it works for weak $n$-groupoids as well. The inclusion of $n\mathrm{Gpd}$ in $(n+1)\mathrm{Gpd}$ also has both a left and a right adjoint. I think Voevodsky calls them the truncation and the “stupid truncation”. Then an equivalence of $\infty$-groupoids is a morphism which induces equivalences on all the truncations (which explicitly corresponds to equivalences at all levels of a Postnikov tower), not one which induces equivalences on all the stupid truncations -- so in this sense $\infty\mathrm{Gpd}$ should be the limit along the left adjoints, what would correspond to the coinductive $(\infty,\infty)\mathrm{Cat}$ in the analogy.

Rune Haugseng (Jun 02 2020 at 20:01):

@Dan Doel Sure, but then you're doing something that's incompatible with equivalences between $\infty$-groupoids, so this only makes sense in terms of some model of $\infty$-groupoids

Dan Doel (Jun 02 2020 at 20:02):

Why can't I say exactly the same thing about your inductive $(\infty,\infty)$-categories?

Dan Doel (Jun 02 2020 at 20:04):

Here is set truncation defined in an appropriate type theory. $\mathsf{squash}_0$ is freely adding paths above a certain level (it looks like it's only adding them at a certain level, but it happens that that also adds them at all higher levels, too, for reasons I probably can't explain very well).

Dan Doel (Jun 02 2020 at 20:05):

$π_0$ is defined as set truncation of the loop path space on a point, I think.

Dan Doel (Jun 02 2020 at 20:06):

That's here, but it's a little hard to read.

Reid Barton (Jun 02 2020 at 20:08):

Dan Doel said:

Why can't I say exactly the same thing about your inductive $(\infty,\infty)$-categories?

I think this is the key question. But just being able to ask the question doesn't mean anything. I could take any old $\infty$-category $C$, and then decide I'm actually interested in some localization of it, and the objects of $C$ are just presentations of the objects of the localization, and whatever invariants I can define on objects of $C$ might not descend to the localization.

Rune Haugseng (Jun 02 2020 at 20:09):

@Amar Hadzihasanovic Thanks, I think I'm starting to understand where you're coming from with this analogy. One important difference though is that these right adjoint functors don't exist at the level of $\infty$-categories of n-groupoids, because they're not compatible with equivalences between n-groupoids. The inclusion of the $\infty$-category of $(\infty,n)$-categories into that of $(\infty,n+1)$-categories has both left and right adjoints (at the $\infty$-level)

Rune Haugseng (Jun 02 2020 at 20:13):

This is different from what happens if I look at n-categories (i.e. (n,n)-categories) - the inclusion of n-categories in (n+1)-categories does not have a right adjoint (of $\infty$-categories/compatibly with equivalences) - the well-behaved underlying object of an (n+1)-category would be an (n+1,n)-category, not an (n,n)-category.

Rune Haugseng (Jun 02 2020 at 20:15):

(I hope I'm not coming across as hostile, by the way - we're clearly coming at this from very different perspectives!)

Rune Haugseng (Jun 02 2020 at 20:17):

I think your "set truncation" must be the same as my "$\pi_0$" - but to underscore my previous comment, I'm unlikely to get much out of looking at an agda program :-)

Amar Hadzihasanovic (Jun 02 2020 at 20:23):

To me you don't come across as hostile at all! (but maybe your aside was directed to Dan). But yes, in my first post in this thread I said that I thought there was a bit of a cultural divide between logic/TCS and alggeo/HT, and I am really grateful for this discussion -- I am learning a lot about the “inductive” perspective.

Dan Doel (Jun 02 2020 at 20:27):

I'm not sure if they're actually the same. I'm probably not communicating well because I don't know that much about the mathematical angle of this.

Here's other jargon that might mean something. Set truncation freely adds paths to make the hom $\infty$-groupoids contractible (I think).

Amar Hadzihasanovic (Jun 02 2020 at 20:27):

I think that in your perspective $(\infty,n)$-categories are “homotopical $n$-categories” or $n$-categories that 'live' in the world of homotopical mathematics, if you allow me some philosophising. So the $\infty$-groupoids in whatever incarnation are there as a background, constraining all the constructions to be compatible with it. And then in this 'world' it seems that the inductive version of $\omega$-categories is the most useful.
Whereas to Dan and me, for various reasons, it comes more natural to build the higher categories and higher groupoids alongside each other -- the latter a special case of the first -- on a background which is “strict”.

Dan Doel (Jun 02 2020 at 20:30):

Yeah, I think I agree with that explanation.

Reid Barton (Jun 02 2020 at 20:31):

I totally agree with this. And it is for this reason that $\infty$-category makes sense as a name for $(\infty, 1)$-category, too. (I used to dislike this convention but recently came around to this point of view.)

Rune Haugseng (Jun 02 2020 at 20:37):

@Amar Hadzihasanovic Yes, I agree with that summary. Do you guys have an actual definition of $(\infty,\infty)$-categories in mind, or is that something people are currently working on?

Dan Doel (Jun 02 2020 at 20:38):

Another reference (which might not help) is that it seems like the inductive version is analogous to what the HoTT book calls a "pre-category", and the coinductive version is what they call a (univalent) category.

Dan Doel (Jun 02 2020 at 20:38):

Although maybe that's not correct, I don't know.

Dan Doel (Jun 02 2020 at 20:44):

I know of this, which is an attempt to produce a type theory where every type has an associated hom type (and so, hom types have hom types, etc.). I think it's still out of my league, though.

Rune Haugseng (Jun 02 2020 at 20:47):

Dan Doel said:

Here's other jargon that might mean something. Set truncation freely adds paths to make the hom $\infty$-groupoids contractible (I think).

Well, $\pi_0$ means the left adjoint to the inclusion of sets into $\infty$-groupoids. Classically this is the set of connected components in a topological space (or simplicial set), and it also restricts to taking the set of isomorphism classes of objects in a groupoid, which is why it sounds weird to me to say that it "freely adds" things.

Rune Haugseng (Jun 02 2020 at 20:50):

I think that paper only talks about $(\infty,1)$-categories (more precisely I believe they formalize "simplicial spaces" and then can define analogues of Segal spaces and complete Segal spaces - that's just based on my memory of a talk by Emily Riehl though).

John Baez (Jun 02 2020 at 20:55):

It sounds like Dan lives in the brave new world where the concept of "set" is just "$\infty$-groupoid with each component contractible". Then taking $\pi_0$ of an $\infty$-groupoid means freely adding enough paths, paths-of-paths etc. to make it into a "set".

It sounds like Rune and I live in something more like the old-fashioned world of ZFC, where set means something else entirely, and taking $\pi_0$ is just taking the set of connected components.

Dan Doel (Jun 02 2020 at 20:55):

Oh, for some reason I though $π_0$ was the group above that.

Anyhow, I don't really think about classical set theory. The analogue to that in HoTT is (I think)... There is no such thing as 'sets' except $\infty$-groupoids that are truncated/contractible above a certain level. So, you could include those into $\infty$-groupoids without that restriction, and the left adjoint freely adds paths to make the right levels contractible.

John Baez (Jun 02 2020 at 20:57):

Yes, as I suspected part of the communication problem was that Dan is living in the world of HoTT (or something like that) while Rune and I live in the world of classical set theory, where you have to painstakingly build the concept of $\infty$-groupoid in some manner.

Btw, I like both worlds, but I probably know about 5000-10000 times as many facts about math based on classical set theory, so that's easier for me to talk about.

Reid Barton (Jun 02 2020 at 20:58):

I think my objection would be if you want to form $\pi_0 X$ by "adjoining" stuff to $X$, that is occurring in a world where it can not happen in any other way than "freely".

Dan Doel (Jun 02 2020 at 20:59):

Possibly you could do it cofreely, too. Although that hasn't worked out too well in the examples I've seen.

Reid Barton (Jun 02 2020 at 21:00):

Well, "freely" to me means without imposing relations, but those relations are something you would just call generators in the next dimension (and all this is quite familiar in homotopy theory, too).

Dan Doel (Jun 02 2020 at 21:00):

Ah, okay.

Reid Barton (Jun 02 2020 at 21:01):

Classically we would call it "killing higher homotopy groups by attaching cells"

John Baez (Jun 02 2020 at 21:02):

:+1:

Dan Doel (Jun 02 2020 at 21:10):

Anyhow, 'the connected components,' is the sort of thing that doesn't work nicely on a computer. So 'attaching cells' gives you a way to represent the points of the truncation in (roughly) the same way as the original type, but there are more ways of proving that the higher things are 'the same'. This instead of having to figure out all the things that are connected (which is probably impossible) so that they are all represented by literally the same thing.

Reuben Stern (they/them) (Jun 02 2020 at 21:13):

Are there examples of things that [are/should be] (∞, ∞)-categories coming up "in nature"?

John Baez (Jun 02 2020 at 21:13):

The advantages for computers are very similar to the advantages for "pure" mathematics; classical set theory is old and familiar, but inefficient in many ways.

John Baez (Jun 02 2020 at 21:14):

Yes, there are lots of examples of (∞, ∞)-categories.

Dan Doel (Jun 02 2020 at 21:16):

Well, my main worry is that with HoTT-alike stuff you have to worry about efficiency of stuff that was previously irrelevant to efficiency. But at least it's not impossible. :slight_smile:

John Baez (Jun 02 2020 at 21:17):

When I use "efficiency" I mean it in some sense that has nothing to do with computers, just how efficiently you can hold things in mind.

Reuben Stern (they/them) (Jun 02 2020 at 21:18):

Where might I find some examples of (∞,∞)-cats? A quick google search is leaving me empty-handed

John Baez (Jun 02 2020 at 21:18):

First of all, none of my friends says "(∞,∞)-categories". They say $\omega$-categories or ∞-categories.

John Baez (Jun 02 2020 at 21:21):

You can find examples in my papers Higher-dimensional algebra and topological quantum field theory and Categorification .

John Baez (Jun 02 2020 at 21:23):

The main examples here are tangle $\infty$-categories and cobordism $\infty$-categories. There are many kinds of these, with a wonderful structure glimpsed in the generalized tangle hypothesis.

John Baez (Jun 02 2020 at 21:23):

But there also lots of other examples, like: sets, spans, spans of spans, spans of spans of spans...

Reuben Stern (they/them) (Jun 02 2020 at 21:23):

Thank you! I like the idea of just saying ∞-category; it goes along with the terminology I use where "n-category" means (∞,n)

John Baez (Jun 02 2020 at 21:24):

I think people have been slow to discuss the applications of true ∞-categories in math because the formalism required to work with them is just being built.

John Baez (Jun 02 2020 at 21:25):

So my impression is that a lot of the wisdom about them has not yet been written down.

John Baez (Jun 02 2020 at 21:26):

There are lots of fascinating ∞-categories lurking in proof theory and rewrite theory, which remain largely unexplored.

Rune Haugseng (Jun 02 2020 at 22:32):

John Baez said:

There are lots of fascinating ∞-categories lurking in proof theory and rewrite theory, which remain largely unexplored.

That sounds really interesting, do you know of any good introductions to this? (I suspect the answer will be that there are lots of references suitable for people who are familiar with computer science/logic but scared of (higher) categories, but not the other way around :slight_smile:)

Dan Doel (Jun 02 2020 at 22:41):

Incidentally, when I said stuff like, "why can't I ..." above, that's because I really don't know. I have little understanding of stuff like the topology end of this kind of thing.

My operating suspicion, though, was that answers like, 'X isn't compatible with equivalence of groupoids,' is equivalent to, 'we already decided that groupoids work coinductively, but haven't decided that for categories.' And you could choose a different notion of equivalence that was analogous in each case. But I don't know if that's actually true.

Dan Doel (Jun 02 2020 at 22:52):

So from my naive perspective, it seems like the reason there can be debate about inductive vs. coinductive criteria is that people haven't decided to call the coinductive one $\infty$-category, and the inductive one 'models of $\infty$-categories' or something. :slight_smile:

Dan Doel (Jun 02 2020 at 22:56):

That also doesn't really mean I don't think it's useful to be able to talk about the inductive on in an $\infty$-groupoid setting, or maybe about strict equality of pre-$\infty$-groupoids or something.

Reid Barton (Jun 02 2020 at 23:09):

I still don't understand what "coinductive" or "inductive" in the setting of $\infty$-groupoids is supposed to mean. What are you calling an $\infty$-groupoid?

Reid Barton (Jun 02 2020 at 23:12):

For a homotopy theorist it just means a space (like, a Kan complex or a topological space or something), and there's no choice involved in the concept

Dan Doel (Jun 02 2020 at 23:12):

Why can't I do the same sort of thing for groupoids? An n-groupoid is a set with n levels of structure above it. Then an inductive $\infty$-groupoid is a sequence of those where the nth one is the 'stupid truncation' of the (n+1)th?

Reid Barton (Jun 02 2020 at 23:13):

I don't know of any model of spaces that works this way, myself.

Rune Haugseng (Jun 02 2020 at 23:19):

So the only way I know to define the (presumably) correct $(\infty,1)$-category of coinductive $(\infty,\infty)$-categories is to form the limit of the $(\infty,1)$-categories Cat(∞,n) as above (and note the right adjoints here are perfectly nice functors of (∞,1)-categories, this doesn't depend on a model), and then force the coinductive equivalences to be invertible by localizing at the map from the "free coinductive equivalence" to the point (which equivalently amounts to restricting to the full subcategory of those objects where all the coinductive equivalences actually are equivalences). You are of course welcome to do that, but as we discussed earlier it has some bad consequences. If you can figure out a way to define this homotopy theory without passing through the inductive version that would certainly make the coinductive approach a lot more convincing :slight_smile:

Rune Haugseng (Jun 02 2020 at 23:21):

Dan Doel said:

Why can't I do the same sort of thing for groupoids? An n-groupoid is a set with n levels of structure above it. Then an inductive $\infty$-groupoid is a sequence of those where the nth one is the 'stupid truncation' of the (n+1)th?

The difference is that the "stupid truncation" is not homotopically meaningful (it doesn't preserve the equivalences), while the right adjoint from $(\infty,n)$-categories to $(\infty,n-1)$-categories is - it is a functor of $(\infty,1)$-categories.

Dan Doel (Jun 02 2020 at 23:25):

You mean it preserves the equivalences from the $\infty$-groupoid substrate you started with, not the 'inverse up to all higher (directed) arrows' structure you decided not to call an equivalence?

Reid Barton (Jun 02 2020 at 23:25):

It preserves the equivalences OF groupoids.

Rune Haugseng (Jun 02 2020 at 23:26):

If we're looking at $(\infty,n)$-categories for n finite there's no difference - a coinductive equivalence in an $(\infty,n)$-category is just an equivalence.

Rune Haugseng (Jun 02 2020 at 23:30):

I.e., a coinductive equivalence can only fail to be an equivalence in my sense if there are non-invertible i-morphisms for arbitrarily large i

John Baez (Jun 03 2020 at 03:23):

Rune Haugseng said:

John Baez said:

There are lots of fascinating ∞-categories lurking in proof theory and rewrite theory, which remain largely unexplored.

That sounds really interesting, do you know of any good introductions to this? (I suspect the answer will be that there are lots of references suitable for people who are familiar with computer science/logic but scared of (higher) categories, but not the other way around :slight_smile:)

There's not nearly as much written about this as there could be. Let's see, the introduction of this:

• Francois Metayer, Resolution by polygraphs

hints at some ideas.

John Baez (Jun 03 2020 at 03:24):

This work uses strict globular $\infty$-categories, by the way.

John Baez (Jun 03 2020 at 03:25):

The results of Squier, mentioned in this introduction, have been influential in this subject.

John Baez (Jun 03 2020 at 03:26):

These slides are perhaps more helpful at getting the basic ideas across:

• Francois Metayer, From word rewriting to higher categories.

John Baez (Jun 03 2020 at 03:31):

This may also be good:

• Samuel Mimran, Towards 3-dimensional rewriting theory.

I think the best days of this subject are yet to come; few people have the technical muscle to study rewriting using higher categories, but the higher structures are there waiting to be studied!

Mike Shulman (Jun 03 2020 at 09:00):

I could be wrong, but I don't think of the inductive/coinductive approaches to equivalences in $(\infty,\infty)$-categories as related to the precategory/univalent-category distinction. It seems to me that you could formulate both "pre" and univalent versions of both of them, simply by using different notions of "equivalence" to state the univalence condition.

Valery Isaev (Jun 03 2020 at 15:51):

Is it known whether Batanin's globular approach models one of the definitions of $(\infty,\infty)$-categories? If it does, it seems it could be only the coinductive definition, right?

Mike Shulman (Jun 03 2020 at 18:34):

Yes, Batanin's globular definition (and most of the other older definitions of $(\infty,\infty)$-category) uses a coinductive notion of equivalence. I don't think any of these definitions have been proven equivalent to those obtained as limits or colimits of $(\infty,n)$-categories.