Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I thought it was silly to have indexed functor without indexed category, so I remedied the situation.
In view of our discussion about people not using ’indexed’ or ’fibered’ in ’parametrized higher category theory’, I went looking to see what we have at the nLab. Let us say it’s far from optimal.
There is Grothendieck fibration which is a redirect for ’fibered category’. This entry speaks of -indexed categories without a link to indexed category. The latter knows that indexed categories are equivalent to fibered categories.
Then there’s also indexed monoidal category. There seems no indication so far of a -version.
In places ’cartesian fibration’ is used as a synonym for ’Grothendieck fibration’, but the page with that title Cartesian fibration (why the capital ’C’ when most such entries have lower case?) speaks directly of quasi-categories.
I see that out in the world people use ’fib(e)red monoidal category’ and ’monoidal fib(e)red category’ and ’monoidal fibration’.
We have monoidal fibration, which says they are a kind of Grothendieck fibration (Cartesian fibration) (so suggesting synonyms), but then says only if the base category is cartesian monoidal is it a case of an indexed monoidal category. Yet indexed monoidal category makes no such restriction of the base.
I guess our chaos is a reflection of the general state of affairs out there. Is it beyond repair?
Thanks for pointing these out!
I added a link from Grothendieck fibration to indexed category.
I’ve removed the use of "cartesian fibration" as a synonym for a 1-categorical Grothendieck fibration at monoidal fibration, which I agree doesn’t make sense given that our page Cartesian fibration is only about quasi-categories. If you notice other such usages please point them out. In a model-independent setting for -categories I’d probably speak simply of a "fibration"; only in a concrete case like quasi-categories do we need to distinguish it from other kinds of model-categorical fibrations. (As for why the capital "C", you’ll have to ask Jacob Lurie. Maybe he hadn’t gotten the memo that category theorists have honored Descartes in the same way that group theorists have honored Abel; unlike the latter, the former usage seems to be largely restricted to category-theorists.)
The statement at monoidal fibration is that if the base is cartesian, then a monoidal fibration is the same as an indexed monoidal category. It doesn’t claim that every indexed monoidal category has a cartesian base. Similarly, indexed monidal category describes how if the base has finite products then the Grothendieck construction of an indexed monoidal category is a monoidal fibration. I’d be happy to hear suggestions for making this relationship more clear.
These are all details, however, and I get the sense you’re seeing a more general problem. Is the entry indexed category not easily-enough noticeable from other entries, do you think? It would probably also benefit from some more explicit discussion of how indexed categories are "a category theory".
I’ll remove Cartesian fibration from Grothendieck fibration:
A Grothendieck fibration (also called a cartesian fibration or fibered category or just a fibration) is a functor such that…
I’m dimly aware that Benabou was exercised by some distinction between ’fibered’ and ’indexed’. Is it something we should reflect?
Is the entry indexed category not easily-enough noticeable from other entries, do you think? It would probably also benefit from some more explicit discussion of how indexed categories are "a category theory".
A couple of things,
Could we not have the wider perspective of ’enriched indexed categories’? There’s just an odd reference at the moment, e.g., at the end of indexed monoidal category. More generally, that idea of something “being a category theory” could be spelled out.
is it that -versions work so straightforwardly from the 1-versions that we could just have single pages, or do we want separate treatments? Is there anything to learn from Fibrations of ∞-categories?
In weak foundations fibred is more general than indexed. Bénabou’s paper on fibred categories and foundations has a big appendix setting out his objections, perhaps not all of which had mathematical origins.
Could we not have the wider perspective of ’enriched indexed categories’
Absolutely, I would love that! (-: But I don’t have time to add it myself.
is it that (∞,1)-versions work so straightforwardly from the 1-versions that we could just have single pages, or do we want separate treatments?
I’d incline towards separate treatments.
In weak foundations fibred is more general than indexed.
That’s a little debatable. I don’t think this is something we need to discuss on the lab. (Anyone who does feel it is important should feel free to add such a discussion, but not at the top, please.)
That’s a little debatable. I don’t think this is something we need to discuss on the lab.
sure. I guess that if the setup is correct, then things work out (eg using anafunctors rather than functors as the morphisms in ). I guess the usual protagonists would have stuck to the “constructively incorrect” , whereby not all fibrations can be cloven (there is a little mention of this already at cleavage).
Yes, anafunctors solve most of the problems. There is also I guess a “universes” issue in that to define an indexed category one needs “the category of categories” in some sense, whereas a fibration can be written down in first-order logic.
There is also I guess a “universes” issue in that to define an indexed category one needs “the category of categories” in some sense, whereas a fibration can be written down in first-order logic.
Good point. Do you know of a reference that discusses the theory of large categories relative to a more-or-less arbitrary base category (eg a pretopos), without polemics? Or is it kind of scattered through the literature? I’m asking because in thinking about class forcing (which at some point I need to return to) one wants to talk about indexing categories for large diagrams, and not necessarily accept the existence of a next higher universe (much like in set theory they are happy to talk classes, perhaps with a few more instances of Replacement for one given class, without using MK or GBC).
No, I don’t think so.
1 to 10 of 10