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.
Alexander Gietelink Oldenziel (Jan 03 2022 at 13:31):It is my understanding that HoTT corresponds to the internal language of the initial elementary -topos. While the Giraud-Rezk-Lurie axioms axxiomatize Grothendieck -topoi, i.e. these correspond somehow to the internal language of the initial Grothendieck -topos .
My understanding might be confused. I suppose that one is not able to prove all Giraud-Rezk-Lurie axioms from just plain HoTT. Do we know which parts of these axioms are not derivable from HoTT?
I.e. what is the gap between Grothendieck and elementary -topoi?
I am particularly interested what parts of Urs Schreiber-Nikolaus-Stevenson [https://arxiv.org/abs/1207.0248], which derives G-principal bundle theory from just the Giraud-Rezk-Lurie axioms, could potentially fail.
Morgan Rogers (he/him) (Jan 03 2022 at 14:10):Initial toposes..? What morphisms are you implicitly talking about?
Morgan Rogers (he/him) (Jan 03 2022 at 14:12):The initial 1-topos, employing geometric morphisms, is degenerate, and I believe the same is true for infinity toposes because the conventions are lifted from 1-topos theory, so I suspect the initial toposes in this sense are probably not the ones you're interested in
Nathanael Arkor (Jan 03 2022 at 14:43):What morphisms are you implicitly talking about?
Presumably a notion of logical functor.
Ulrik Buchholtz (Jan 03 2022 at 14:48):Alexander Gietelink Oldenziel said:
I am particularly interested what parts of Urs Schreiber-Nikolaus-Stevenson arXiv:1207.0248, which derives G-principal bundle theory from just the Giraud-Rezk-Lurie axioms, could potentially fail.
You can do a lot of that in HoTT, by working with -groups as pointed, connected types (see here for some details). What you can't do is define -monoids (and carve out -groups from those) as types with coherently unital-associative composition operations. But that's often not needed.
Morgan Rogers (he/him) (Jan 03 2022 at 15:23):What morphisms are you implicitly talking about?
Presumably a notion of logical functor.
It must be something fairly precise to make infinity groupoids initial amongst Grothendieck infinity-toposes, no?
Nathanael Arkor (Jan 03 2022 at 15:30):Oh, sorry, you were of course referring to the Grothendieck toposes. In that case, then presumably Alexander is thinking about the dual setting (i.e. logoses rather than toposes), and means the terminal Grothendieck (infinity, 1)-topos with respect to geometric morphisms.
Mike Shulman (Jan 03 2022 at 15:57):Ulrik Buchholtz said:
What you can't do is define -monoids (and carve out -groups from those) as types with coherently unital-associative composition operations. But that's often not needed.
To be more precise, we don't currently know how to do this in HoTT, but no one has proven it impossible yet either. It's true that it's not often needed when setting up the abstract theory, but I think when constructing actual examples it's more annoying to live without.
Mike Shulman (Jan 03 2022 at 16:06):Alexander Gietelink Oldenziel said:
Do we know which parts of these axioms are not derivable from HoTT?
I.e. what is the gap between Grothendieck and elementary -topoi?
Just as in the case of 1-toposes, the elementary part can only speak about finitary structure. Thus it can talk about disjoint and stable finite coproducts, but not infinite ones. The main difference from the 1-categorical case is that effective quotients of equivalence relations in a 1-category are finitary, while effective quotients of groupoid objects in an -category are not.
However, in both 1-toposes and -toposes, one can use a natural numbers object to speak in a finitary way about infinitary structure. In this way one can say internally that infinite coproducts are disjoint and stable as well (although in the elementary case this doesn't actually imply that externally-infinite coproducts exist). The open question Ulrik referred to is whether tricks like this can be used to talk internally in an elementary -topos about effective quotients of groupoid objects.