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.
Jacques Carette (Aug 20 2021 at 17:09):I'm going to be speaking about slice categories here, but I'm aware that they are a special case of comma categories. Any answer that covers either/both would be welcome.
Context: one of the (old) lessons of category theory is the groupoid idea, i.e. don't actually take quotients, just go up a dimension, so that you don't need to squish things down uncomfortably. One can somewhat extend this idea to not pairing together things that naturally live in different universes. This shows up awkwardly in 'set'-based category theory (small, locally small, large, huge, etc), but is rather elegant when universes have names and/or are polymorphic, such as in Martin-L$$\"{o}$$f type theory. So objects and homs can live in different 'universes', and things work swimmingly.
But slice categories 'break' that: they pair up objects and morphisms, thus mixing universes. So the temptation is to try to make things larger (bicategories? double categories? something else?) where all the data that make up slice categories is still there, but not all squished together.
This feels like something that's probably been done already, though perhaps the motivation might have been quite different.
If someone wants a precise question: is there a 'home' for the data of a slice category that ends up being equivalent when everything is 'small', but does not mix objects with arrows.
Morgan Rogers (he/him) (Aug 20 2021 at 17:19):Can you elaborate on how things 'break'? It seems to me that one could afford to just put aside the universe that the objects live in when constructing slices, since the objects of the new category are morphisms of the old one.
Nathanael Arkor (Aug 20 2021 at 17:20):I don't see how the slice category construction (or combining entities residing in different places) is analogous to quotienting. In the latter, you are throwing away information, but you aren't doing anything of the sort in the former.
Nathanael Arkor (Aug 20 2021 at 17:21):In addition, comma categories can be described as a kind of 2-limit, which is surely evidence that they're entirely natural when considered in their own right.
Jacques Carette (Aug 20 2021 at 17:31):Nothing 'breaks'. And it isn't necessarily analogous to quotienting, that's just the best I could come up with. It's a general malaise on my part, where I don't like mixing things from different universes. And for sure, comma categories are entirely natural! That's why I didn't dismiss my malaise, but dug in, to understand better.
The comma object, as a 2-limit, was helpful, thanks. It's definitely along the lines of what I was hoping for.
Nathanael Arkor (Aug 20 2021 at 17:58):Another observation that may be helpful is that slices arise as hom-categories in bicategories of spans: if you consider the 2-cells of Span(E), you'll see that they correspond to morphisms between slices.
Mike Shulman (Aug 20 2021 at 17:59):I would say the reason it's not a problem is that it only brings things "down" in level, rather than up. You can always consider a set to be a discrete category, or a category to be a locally discrete 2-category, etc. In this case, the objects of a slice/comma category involve both (1) objects of the original category, at the same level, and (2) morphisms of the original category, which are at a higher level — they form a set, which we can always consider to be a discrete category. Similarly, the morphisms of a slice category involve morphisms of the original category and equalities of morphisms in the original category, which again are at a higher level. What forces a construction to go up a categorical dimension is if you lift data to a higher level, e.g. spans, where the morphisms in the category of spans involve objects in the original category.
Jacques Carette (Aug 20 2021 at 18:42):So I'm working with unsaturated E-categories, so there really are 3 distinct levels, with no a priori relation on the sizes. My Homs are (unsaturated) Setoids. That's why I'm even able to see that there's mixing going on!
That is indeed why my doodling seems to indicate double categories might be an even better home than bicategories.
I also want to repeat: I am not claiming there is a problem. I know that many constructions in category theory have a lot of different ways to look at them, so I was looking for such for slice/comma.
Mike Shulman (Aug 20 2021 at 18:49):It's important to distinguish between size (in the sense of how big a universe is) and categorical dimension: they're really unrelated.
Jacques Carette (Aug 20 2021 at 18:49):You're right, and I know this, I was indeed a little sloppy there.
Mike Shulman (Aug 20 2021 at 18:50):I don't see why things would be any different with E-categories: just as a set can be regarded as a discrete category, a setoid can be regarded as an (essentially) discrete E-category.
Jacques Carette (Aug 20 2021 at 18:59):Things are not different in E-categories, and indeed the DiscreteSetoid functor in agda-categories works exactly as you say. The only thing I'm saying is that I can 'see' the 3 arbitrary universes involved getting intertwined in a slice category, and I was wondering if there was an equivalent construction that doesn't do that.
The same way the unit/counit construction of Adjoints is fully universe polymorphic, but the equivalence-of-Hom-Setoids version (which is classically equivalent) is not.
Nathanael Arkor (Aug 20 2021 at 19:10):Why are the two definitions of adjunction not equivalent constructively? They can be proven equivalent in any 2-category, which includes Setoid-enriched categories.
Mike Shulman (Aug 20 2021 at 19:16):Ah, finally I see what you're getting at by talking about universes and size. You're saying that the type of E-categories can be parametrized over three unrelated universes, for the types of objects, morphisms, and equalities respectively, and that the slice/comma construction doesn't act on such E-categories leaving all the universes fixed. So it could either be an endomorphism of (in Coq notation) ECat@{i j k} with extra constraints k <= j <= i, or it could take input in ECat@{i j k} and yield output in ECat@{max(i,j) max(j,k) k}.
Jacques Carette (Aug 20 2021 at 19:16):@Nathanael Arkor They are still equivalent. They just need some extra work, because the Hom-Setoids naturally live in different universes, so can't be linked via a natural isomorphism 'on the nose'. You first need to inject both into the same universe, then things go through. Gory details near the end of this file if you read Agda.
Jacques Carette (Aug 20 2021 at 19:17):@Mike Shulman Exactly!
Mike Shulman (Aug 20 2021 at 19:18):I suppose I would argue that one should always impose the constraint k <= j <= i.
Jacques Carette (Aug 20 2021 at 19:18):How could I have said this to make myself clearer? [I avoided Agda-specific lingo on purpose]
Mike Shulman (Aug 20 2021 at 19:21):Well, I probably would have understood more quickly if you'd said it the way I did (-:
...the type of E-categories can be parametrized over three unrelated universes, for the types of objects, morphisms, and equalities respectively, and that the slice/comma construction doesn't act on such E-categories leaving all the universes fixed. So it could either be an endomorphism of (in Coq notation)
ECat@{i j k}with extra constraintsk <= j <= i, or it could take input inECat@{i j k}and yield output inECat@{max(i,j) max(j,k) k}.
But I don't think you were deficient in clarity by not saying exactly this to start with. Different people naturally think and phrase things in different ways, and bridging those gaps is why we communicate. (-:
Jacques Carette (Aug 20 2021 at 19:21):Mike Shulman said:
I suppose I would argue that one should always impose the constraint
k <= j <= i.
There's certainly a solid case to be made there, yes. It's both 1) too bad that it's really hard to actually say/do that, and 2) fascinating that almost all of category doesn't actually 'need' that.
Mike Shulman (Aug 20 2021 at 19:22):Jacques Carette said:
too bad that it's really hard to actually say/do that
Maybe in Agda, but not I think in Coq, where constraints on universes are inferred automatically and carried through everything.
Jacques Carette (Aug 20 2021 at 19:25):Oh, Agda infers them just fine! You just can't say that you have those extra constraints, i.e. k <= j <= i. You'll get the Agda-equivalent of ECat@{max(i,j) max(j,k) k} automatically. Can you say k <= j <= i in Coq?
Kenji Maillard (Aug 20 2021 at 19:35):you can specify constraints between universe levels in Coq, e.g.
Record ECat@{ i j k | i <= j, j <= k } := { (*to be filled *) }.
I didn't know that! We used to have to create constraints with manual hacks like this.
Mike Shulman (Aug 20 2021 at 21:10):Jacques Carette said:
fascinating that almost all of category doesn't actually 'need' that.
Of course, there's a substantial part of category theory that requires a strict inequality j < i, namely the theory of small limits and colimits in locally small categories. Of course you can define limits and colimits of any size in a category of any size, but things get significantly nicer when you're talking about categories that have limits and colimits of a size that can be indexed by their hom-sets.
Mike Shulman (Aug 20 2021 at 21:11):I haven't thought about how that generalizes to E-categories, e.g. do you need k < j < i or is k <= j < i enough, or even just k < i, j < i separately.
Jacques Carette (Aug 20 2021 at 22:52):As far as agda is concerned, a limit (i.e. all the data, not just the object) lives in the largest universe you name, of the ones involved in the category and the indexing category. I need to open up Agda to see where the limit object itself wants to live.
Mike Shulman (Aug 20 2021 at 23:20):Right, but the point is that, for instance, to prove an adjoint functor theorem you need the categories involved to have limits of the size of their hom-sets, and in concrete examples this requires their type of objects to be one universe higher than that of their hom-sets.
Jacques Carette (Aug 21 2021 at 00:17):Jason did the AFT proof, and I'm having a difficult time reading the levels involved to know how to read off the right things. Interestingly, it all revolves around... comma categories.