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) (Feb 14 2023 at 13:21):In category theory often one has a sense of 'inevitability' of certain constructions, which are basically the only possible things one can do in a given context. And yet, very often I find myself having to prove lots of coherence and well-posedness conditions... and that seems a waste a time, because I know everything's gonna work out, because how else could it end?
Hence it seems to me there is some very general coherence result lurking in the background, telling us that if I don't do anything bizarre, whatever I do categorically is gonna yield well-defined (functorial, natural, you name it) constructions.
I know it's very vague, but does anyone have an idea about what this result might look like?
Matteo Capucci (he/him) (Feb 14 2023 at 13:28):One example above all, due to Leinster: Yoneda lemma. If you have a category and a presheaf, there's not much you can talk about. You have and the representables . You can ask about morphisms in and out of from this one. And if you look at morphisms , you get a presheaf again.
Matteo Capucci (he/him) (Feb 14 2023 at 13:33):Then one might speculate they are the same, and indeed one finds it's trivial to find maps between and , which are evidently inverse to each other. At this point we should be able to argue: we didn't do anything weird, so we can conclude the object we constructed (the iso ) is a bona fide natural transformation. Even more, we should be able to argue that such an isomorphism is itself picked out 'naturally', somehow (what do I mean here? idk)
Amar Hadzihasanovic (Feb 14 2023 at 14:45):My own experience of category theory is that it is full of “inevitable” things which turn out to be not inevitable at all and in fact wrong.
Amar Hadzihasanovic (Feb 14 2023 at 14:46):(A famous example is that distributive monoidal categories satisfy all equations of linearly distributive categories except one, which they can satisfy if and only if they are posetal.)
Nathanael Arkor (Feb 14 2023 at 16:28):@Matteo Capucci (he/him): two papers you might be interested in are Lack's Non-canonical isomorphisms and Nunes's later paper Pseudoalgebras and Non-canonical Isomorphisms.
John Baez (Feb 14 2023 at 16:43):While there probably isn't a universal theorem that puts category theorists out of business by saying "all commutative diagrams that deserve to commute, do", there are lots of super-general coherence theorems known and probably more waiting to be discovered. So I applaud Matteo's desire to find them!
Homotopy theorists are probably the best experts at proving theorems that let them avoid (infinite towers of) coherence laws.
Amar Hadzihasanovic (Feb 14 2023 at 16:43):Possibly also relevant: this paper by Shulman
Amar Hadzihasanovic (Feb 14 2023 at 16:46):(While the title states a negative, it also begins with a review of positives, conditions under which there is a general "coherence theorem".)
Matteo Capucci (he/him) (Feb 14 2023 at 16:51):Amar Hadzihasanovic said:
My own experience of category theory is that it is full of “inevitable” things which turn out to be not inevitable at all and in fact wrong.
Yeah maybe this is the most important fact. Can we have a list of 'forbidden spells' that break coherence?
Matteo Capucci (he/him) (Feb 14 2023 at 16:51):Nathanael Arkor said:
Matteo Capucci (he/him): one paper you might be interested in is Lack's Non-canonical isomorphisms and Nunes's later paper Pseudoalgebras and Non-canonical Isomorphisms.
Thanks Nathanael, you're always very helpful with literature :) I'll look into them
Fernando Yamauti (Feb 14 2023 at 17:59):Isn't Grothendieck's Homotopy Hypothesis something along these lines? It looks like inevitable at first (one simply adds the obvious coherences in a coherator). Maybe you can argue that there are too many non-canonical choices though.
More interesting examples would be isomorphisms of stuff induced by non-canonical morphisms. Something like the arrow in Beck-Chevalley, or Frobenius reciprocity, or in a commutativity of limits and colimits such that the domain and codomain are isomorphic but the canonical morphism fails to be so. Does anyone know explicit examples in those cases?
John Baez (Feb 14 2023 at 18:57):Isn't Grothendieck's Homotopy Hypothesis something along these lines?
Hmm. This hypothesis says that homotopy types are the same as -groupoids. If you believe it, you don't need to give an independent definition of "-groupoid". So in that sense it does absolve you from writing down lots of coherence laws that might appear in the definition of -groupoid: we can just define homotopy types using topological spaces or Kan complexes.
But notice that as soon as you start trying to work with homotopy types, the coherence issues reappear. For example an space is a homotopy that's a monoid "up to homotopy", where the homotopies obey the pentagon identity up to homotopy, where these homotopies make the 3d Stasheff polytope commute up to homotopy, etc.
Of course you can avoid all this mess by simply decreeing that an space is a space equipped with a (weak) homotopy equivalence to a topological monoid. But this only works if you are willing to believe (or prove) that all the coherence issues work fine. And so on.
John Baez (Feb 14 2023 at 18:59):This has been a long story within homotopy theory; I'm only talking about things that happened before 1972.
Fernando Yamauti (Feb 14 2023 at 20:57):John Baez said:
Isn't Grothendieck's Homotopy Hypothesis something along these lines?
Hmm. This hypothesis says that homotopy types are the same as -groupoids. If you believe it, you don't need to give an independent definition of "-groupoid". So in that sense it does absolve you from writing down lots of coherence laws that might appear in the definition of -groupoid: we can just define homotopy types using topological spaces or Kan complexes.
But notice that as soon as you start trying to work with homotopy types, the coherence issues reappear. For example an space is a homotopy that's a monoid "up to homotopy", where the homotopies obey the pentagon identity up to homotopy, where these homotopies make the 3d Stasheff polytope commute up to homotopy, etc.
Of course you can avoid all this mess by simply decreeing that an space is a space equipped with a (weak) homotopy equivalence to a topological monoid. But this only works if you are willing to believe (or prove) that all the coherence issues work fine. And so on.
In my comment, I was referring to Grothendieck's model for weak -groupoids. In a coherator, one iteratively forces all the possible obvious diagrams, that one would expect to commute, to commute up to higher cells. Still, it's not obvious if that's enough to codify all the coherences in a homotopy type. So my point was that, in this case, one only proceeds the construction doing "what's obvious", but, in the end, no one knows if it's going to work.
John Baez (Feb 14 2023 at 22:07):Okay, thanks. I was referring to the homotopy hypothesis in its more general meaning as "weak -groupoids (in some definition thereof) are equivalent (in some sense) to homotopy types".
John Baez (Feb 14 2023 at 22:08):By the way, who was the first one who actually wrote the phrase "homotopy hypothesis" with this meaning?
John Baez (Feb 14 2023 at 22:18):It might have been me, in my June 2004 talk called Why n-Categories? at the workshop -Categories: Foundations and Applications. On page 17 of my slides I state a version of the homotopy hypothesis.
Or it might have been someone much earlier! The idea clearly goes back at least to Grothendieck. I'm just wondering about the phrase "homotopy hypothesis". I have the feeling I made it up, but it seems hard to believe.
John Baez (Feb 14 2023 at 22:19):Later, in 2007, I gave a talk at the Fields Institute called The Homotopy Hypothesis.
Mike Shulman (Feb 15 2023 at 01:06):I do have the sense that the "inevitable facts that turn out to be wrong" are memorable because they're surprising, because we're used to diagrams commuting most of the time, as Matteo said. In addition to the answers already given, another possible answer is "parametricity" in the computer science sense: in some cases, if some operation can be defined constructively, then it is automatically functorial or natural.
Josselin Poiret (Feb 15 2023 at 09:21):An hypothetical "directed type theory" would help formalize this behavior: the terms that you would be able to construct using it would be automatically functorial/natural/etc. without explicitely having to prove it. This remains hypothetical for now though AFAIK.
Robin Piedeleu (Feb 15 2023 at 09:28):This discussion made me want to create a [[counterexamples in category theory]] page on the nlab. Turns out it already exists, but could be expanded with the counter-examples discussed here!
Matteo Capucci (he/him) (Feb 15 2023 at 11:50):Mike Shulman said:
I do have the sense that the "inevitable facts that turn out to be wrong" are memorable because they're surprising, because we're used to diagrams commuting most of the time, as Matteo said. In addition to the answers already given, another possible answer is "parametricity" in the computer science sense: in some cases, if some operation can be defined constructively, then it is automatically functorial or natural.
Parametricity is definitely a key word here. Constructively too. I believe that's because in most case this 'natural feel' of coherence arises from constructing things coherently using from other coherent things. The kind of coherence you need in the previous sentence is what defies me a bit. I know functorial/natural can do, but that's a bit too vague...
Mike Shulman (Feb 16 2023 at 15:44):"Constructing things coherently from other coherent things" is also part of what directed type theory should achieve, as Josselin said.
Matteo Capucci (he/him) (Feb 18 2023 at 13:14):Somehow I missed their message! Maybe it's obvious if I think enough about it, but how would that work? It's the same idea as stuff written in hott is automatically coherent once interpreted in any -categories?
Mike Shulman (Feb 18 2023 at 15:32):Yeah, basically.
Josselin Poiret (Feb 19 2023 at 13:59):Matteo Capucci (he/him) said:
Somehow I missed their message! Maybe it's obvious if I think enough about it, but how would that work? It's the same idea as stuff written in hott is automatically coherent once interpreted in any -categories?
Note that you can't interpret HoTT in any -category unfortunately, you need it to be an -(Grothendieck) topos
Josselin Poiret (Feb 19 2023 at 14:01):basically, the parallel between HoTT and DTT would be that HoTT lets you synthetically manipulate groupoids, whereas DTT lets you synthetically manipulate categories instead.
Mike Shulman (Feb 19 2023 at 16:06):(Although you can embed any -category in its presheaf -topos and interpret HoTT there.)
Josselin Poiret (Feb 20 2023 at 13:29):Is there a good synthetic way to talk about representable objects in MLTT? Something like a universe of representable types?
Mike Shulman (Feb 20 2023 at 16:59):Yes, you would postulate a particular universe that's closed under whatever constructions your original category theory has that are preserved by the Yoneda embedding, like -types and -types (if it has finite limits) and -types if it's LCCC.