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: learning: questions

Topic: Strict univalent foundations

Sridhar Ramesh (Dec 07 2024 at 18:22):

In homotopy type theory/univalent foundations, all types(/spaces/whatever you want to call them) have the structure of (weak) infinity-groupoids.

What happens if we further add the axiom that each of these infinity-groupoids is equivalent to a strict infinity-category? (Thus, for example, making all their braidings symmetric, among other consequences). Is this consistent or inconsistent with the univalence axiom? (If consistent, does this have any other interesting or bothersome consequences?)

Sridhar Ramesh (Dec 07 2024 at 18:24):

(Not sure if this belongs in "learning: questions". Always tricky for me to decide where posts belong exactly; feel free to move this if it would be better categorized elsewhere.)

Josselin Poiret (Dec 09 2024 at 10:13):

is this even possible to formalize internally such a statement?

Madeleine Birchfield (Dec 09 2024 at 13:53):

Probably the first thing to do is to prove that the model structure on strict $\infty$-groupoids presents a full sub-$(\infty,1)$-category of the $(\infty,1)$-topos of $\infty$-groupoids. The nLab merely claims the statement in [[strict infinity-groupoid]] but does not provide a proof or a reference to a proof.

Madeleine Birchfield (Dec 09 2024 at 13:56):

Then, if such a full sub-$(\infty, 1)$-category exists, one should try to find internally valid synthetic axioms that distinguish amongst all the $\infty$-groupoids the ones in the full sub-$(\infty, 1)$-category; i.e. presented by the model structure on strict $\infty$-groupoids. The end goal is to create a dependent type theory which is the internal logic of the full sub-$(\infty, 1)$-category.

Madeleine Birchfield (Dec 09 2024 at 14:18):

If one is just interested in the 1-category of strict $\infty$-groupoids, those are just crossed complexes, and one would be trying to find synthetic axioms for the internal logic of the category of crossed complexes and structure-preserving maps.

Amar Hadzihasanovic (Dec 09 2024 at 15:18):

One fact that holds in the world of strict $\infty$-groupoids is that the suspension of an $n$-groupoid is an $(n+1)$-groupoid, which in a dependent type theory with [[suspension type]] s $\mathrm{S}$ and an [[n-truncation modality]] $[-]_n$, one could try to formalise by making $\mathrm{S}[X]_n = [\mathrm{S}X]_{n+1}$ inhabited for all types $X$ in some universe. Perhaps considering whether this is compatible with univalence would already go a certain distance.

Amar Hadzihasanovic (Dec 09 2024 at 15:21):

At the semantic level I think this would correspond to localising at the universal maps from the $n$-spheres to their $n$-truncations, that is, “making the $n$-sphere $n$-truncated for all $n$”.

Sridhar Ramesh (Dec 09 2024 at 15:23):

Separate from the question of how to synthetically axiomatize strictness, I am curious as to whether there are models of univalence using just those infinity-groupoids which are equivalent to strict infinity-categories (I phrase this in terms of "strict infinity-categories" instead of "strict infinity-groupoids" to allow for the inverses to not be strict inverses, though this may make no difference).

Amar Hadzihasanovic (Dec 09 2024 at 15:26):

Yeah, I understand; I was thinking of synthetic axioms just in case one of them turned out to be inconsistent with univalence, thereby preventing the existence of a semantics in strict $\infty$-groupoids

Amar Hadzihasanovic (Dec 09 2024 at 15:33):

(Although I have been for a long time skeptical about strict $\infty$-groupoids being a “natural” class of homotopy types, so I am inclined to believe that the answer to this question would be shared with some super-class that contains it -- which is why I would focus on necessary but not sufficient axioms)

Mike Shulman (Dec 09 2024 at 16:09):

Michael Warren's thesis constructed models of homotopy type theory in strict $\infty$-groupoids, but he didn't consider univalence (which wasn't part of the general consciousness yet at the time in 2008).

Mike Shulman (Dec 09 2024 at 16:11):

Amar Hadzihasanovic said:

One fact that holds in the world of strict $\infty$-groupoids is that the suspension of an $n$-groupoid is an $(n+1)$-groupoid, which in a dependent type theory with [[suspension type]] s $\mathrm{S}$ and an [[n-truncation modality]] $[-]_n$, one could try to formalise by making $\mathrm{S}[X]_n = [\mathrm{S}X]_{n+1}$ inhabited for all types $X$ in some universe. Perhaps considering whether this is compatible with univalence would already go a certain distance.

This is not compatible with univalence, since the suspension of the 1-sphere is the 2-sphere, and with univalence you can prove that $\pi_3(S^2) = \mathbb{Z}$.

Amar Hadzihasanovic (Dec 09 2024 at 16:45):

On second thought, though, I think I am confident about my point about suspension only wrt strict $\infty$-groupoids with strict inverses, so the ones that are equivalent to crossed complexes; homotopy pushouts are more complicated in strict $\omega$-categories with weak inverses, so I would need to think carefully about what suspension is there.

Anyway, I do believe that Mike's comment should lead to incompatibility of univalence with semantics in strict $\infty$-groupoids with strict inverses.

Mike Shulman (Dec 09 2024 at 17:22):

I have a vague memory that this question was discussed at some point in the past, maybe on the HoTT mailing list, and a similar conclusion reached.

Amar Hadzihasanovic (Dec 09 2024 at 17:36):

In fact, thinking of it for a little bit, I do think that the "2-sphere", that is the twice-suspended pair of points, in the folk model structure for strict $\omega$-categories with weak inverses is the "walking weakly invertible 2-cell with degenerate boundaries", which is the example for which Simpson showed the vanishing of the generator of $\pi_3$.

John Baez (Dec 09 2024 at 17:56):

One question I have is: why should we care about strict infinity-groupoids, except for the fact that strictness is a powerful simplifying assumption?

One answer: I think there's a nice topological characterization of the spaces whose homotopy types are strict infinity-groupoids. I could be getting this wrong, but I think these are the spaces whose [[Postnikov invariants]] all vanish. Thus, any connected is the total space of a bundle where the fiber is a product of [[Eilenberg-Mac Lane spaces]] $K(\pi_n,n)$ for $n > 1$ and the base is a $K(\pi_1,1)$, where the only "twisting" arises from an action of $\pi_1$ on each higher $\pi_n$.

That sounds like a mouthful, but for a homotopy theorist this sounds like a pretty simple sort of space.

Sridhar Ramesh (Dec 09 2024 at 18:18):

A reason I thought I should care about strict n-categories (for finite n or n = infinity) is that strict (< n)-categories naturally comprise a strict n-category, thus inductively bringing me to care about strict infinity-categories.

But univalence being inconsistent with an interpretation into strict infinity-categories is challenging my intuitions here. I will have to sit and think and reconcile my intuitions, to decide whether I care about strict n-categories after all or not.

Amar Hadzihasanovic (Dec 09 2024 at 19:05):

@Sridhar Ramesh strict n-categories form a strict (n+1)-category only with boring higher morphisms—the ones with strictly commuting naturality squares—so I think that whether that's their "natural" ensemble is also unclear.

Sridhar Ramesh (Dec 09 2024 at 19:15):

Sure, but that's natural at least in the sense of arising from the cartesian closed structure on n-Cat, right? That is, if it is at least natural to consider strict n-functors (viewing strict n-categories as models of an ordinary algebraic theory), then it is natural to consider the 1-category these comprise, which turns out to be cartesian closed, thus enriched over itself in a very natural way to consider, from which we get the view of it as a strict (n + 1)-category.

This is not the limiting bounds of what is natural to think about but it seems at least one naturally arising thing to consider, even though it has as 2-cells the strictly natural transformations rather than pseudonatural transformations and so on.

Amar Hadzihasanovic (Dec 09 2024 at 19:51):

Yes, I agree that this sort of "fixed point of self-enrichment" story is a natural justification of strict $\omega$-categories, but it also seems quite unrelated to the homotopy-theoretic side; for example the cartesian closed structure which is used for self-enrichment is not compatible with the folk model structure.

Mike Shulman (Dec 09 2024 at 20:18):

By default, you should not care about strict higher categories. If you aren't sure whether or not you should care about them, you probably shouldn't.

David Michael Roberts (Dec 09 2024 at 20:46):

That's a bit strongly worded... :-)

David Michael Roberts (Dec 09 2024 at 20:46):

In the context of .... should one not care?

Mike Shulman (Dec 09 2024 at 20:47):

David Michael Roberts said:

In the context of .... should one not care?

I don't understand, what do you mean?

David Michael Roberts (Dec 09 2024 at 20:51):

Your statement seemed like a very broad one, that The Default Position on a class of objects is that no one should consider them worth of study. I'm pretty sure your position is more nuanced.

David Michael Roberts (Dec 09 2024 at 20:52):

But this (in the spirit of collegiality, and not enforcing one's priorities) could be put in a way that specifies what this is in contrast to, and/or in what particular focus of study.

David Michael Roberts (Dec 09 2024 at 20:53):

It's more a matter of wording than the fact of the statement.

Amar Hadzihasanovic (Dec 09 2024 at 20:55):

I read it in the same spirit as one would say "by default you shouldn't care about non-Hausdorff topological spaces" or "non-noetherian rings", in the sense that "you should only care about these if you have a specific reason why you need to".

Mike Shulman (Dec 09 2024 at 21:04):

Yes, what Amar said is what I meant by "by default".

Mike Shulman (Dec 09 2024 at 21:06):

I think someone who is just coming to the field of higher categories should start out assuming that they probably want the weak ones, since in most cases those are the more useful.

Mike Shulman (Dec 09 2024 at 21:12):

I didn't mean to denigrate the work of people who do care about strict higher categories for good reasons.

John Baez (Dec 09 2024 at 21:27):

Historically it was actually a huge step forward, not taken easily, to realize that by default it's the weak n-categories that matter most. It was a difficult step both because you can strictify any weak 2-category (leading to some false hopes that this would continue for higher n), and because weak n-categories are a lot more complicated to work with. I was there.

So, it's not so terrible to give the youngsters the benefit of history, and tell them that if they don't have a special reason to care about strict n-categories, they probably want to use the weak ones. But ultimately of course it's important to tell them the reasons why weak ones are more important (which I am not attempting to do here).

Amar Hadzihasanovic (Dec 09 2024 at 22:05):

Besides what John says, with which I agree even though “I was not there” :), I would just add that, while the notion that “weak higher categories are more important” is widely accepted, I believe that it is underappreciated how little evidence there is that strict higher categories are, at all, a “natural subclass” of weak higher categories; and that indeed the situation is quite different from the case of strict vs weak groupoids, where I believe John's suggested characterisation in terms of vanishing Postnikov invariants should hold (I am not sure to what degree it is proven)

Amar Hadzihasanovic (Dec 09 2024 at 22:11):

A proper subclass of $n$-categories, the gaunt ones which do not contain any (weakly) invertible cells at all except identities, play a role in the axiomatic framework for the homotopy theory of $(\infty, n)$-categories due to Barwick and Schommer-Pries, as being postulated to be generating under homotopy colimits. But in fact only a smaller set of gaunt $n$-categories is sufficient for the purpose.

Sridhar Ramesh (Dec 09 2024 at 22:15):

Whether or not I should care about whatever, what I have learnt from this thread is that it is possible to model type theory with identity types in strict infinity-groupoids (as in Michael Warren's thesis) without trivializing iterated identity types, but that such a model of type theory cannot be equipped with a univalent universe the way a model in weak infinity-groupoids can be.

It would be enlightening for me to understand directly what goes awry in trying to carry out in the former context the analog of the construction used in the latter model for a univalent universe.

Amar Hadzihasanovic (Dec 09 2024 at 22:25):

I do not know a precise answer but I imagine that the fact that the folk model structure on strict $\omega$-groupoids is not cartesian (e.g. the product of two cofibrants is almost never cofibrant) probably limits the applicability of most techniques used in the “weak” case.