Timeline for Elementary theory of the category of groupoids?
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 3, 2021 at 20:34 | comment | added | Tim Campion | In the (Grothendieck) $\infty$-topos case, Lurie formally uses universes in the metatheory. That's not really relevant to the issue of thinking about size inside an $\infty$-topos, where he ends up with $\kappa$-object classifiers for every regular cardinal $\kappa$ or something. (I'm trying to say that your $\kappa$-small sets need not technically form a "universe" but just some sort of "weak universe"...) Anyway, the existing stuff outside of type theory is foundationally complicated. But type theorists do think carefully about these sorts of things. | |
| Feb 3, 2021 at 20:29 | comment | added | Tim Campion | Yes. I believe in Weber's theory of 2-topoi, two universes are used. Size issues are important to think about here, and potentially very delicate. This is especially so if one is trying to work foundationally, because a lot of the ways we're used to thinking about size are potentially quite tied up with the details of the metatheory, which is usually ZFC (but if we're trying to build a foundational theory, we're probably trying to avoid using something like ZFC in any kind of metatheory). As Noah Snyder indicates, thinking about this from a type-theoretic perspective would at least mean no ZFC | |
| Feb 3, 2021 at 20:26 | comment | added | user173426 | However, the notion of the groupoid of sets in a category of groupoids has size issues, similar to the case in infinity topos theory, so it probably would make more sense to talk about internal groupoid of $\kappa$-small sets. | |
| Feb 3, 2021 at 20:17 | comment | added | Tim Campion | Yes. I should also mention that there has been work on 2-topoi (i.e. (2,2)-topoi in the terminology from above. In this terminology, what is normally called an $\infty$-topos should be called an $(\infty,1)$-topos, and what is normally called a topos or 1-topos should be called a (1,1)-topos).Just as the canonical 1-topos is $Set$, and the canonical $(2,1)$-topos is $Gpd$, the canonical $(2,2)$-topos is $Cat$.The "subobject classifier" of the 2-topos$Cat$ is $Set$. The "subobject classifier" of the (2,1)-topos of groupoids, would be the groupoid of sets | |
| Feb 3, 2021 at 20:11 | comment | added | user173426 | Since a subobject classifier is simply an object that classifies $-1$-morphisms; i.e. internal trith values; I would think that the corresponding classifier would be something that could classify $0$-morphisms, or the discrete objects of the groupoid. This might be some internal notion of a groupoid of sets. | |
| Feb 3, 2021 at 19:06 | history | edited | Tim Campion | CC BY-SA 4.0 |
edited body
|
| Feb 3, 2021 at 18:58 | history | answered | Tim Campion | CC BY-SA 4.0 |