2-Toposes
Posted by David Corfield
As 2-toposes seem to be cropping up a bit, here and here, let’s see if we can attract some experts to teach us about them.
On p. 36 of Mark Weber’s Strict 2-toposes, a 2-topos is defined as a finitely complete cartesian closed 2-category equipped with a duality involution and a classifying discrete opfibration. Cat is a good example of a 2-topos. Are there other familiar ones?
A 1-topos is a kind of 1-category. The 1-category of sets is a paradigmatic example, in which (the set of truth values) is the classifier.
A 2-topos is a kind of 2-category. The 2-category of categories is a paradigmatic example, in which Pointed Set Set is the classifier.
Hmmm, so what’s a 0-topos? It ought to be a kind of 0-category or set. The set of truth values should be a paradigmatic example. What kind of set should it be?
If in Set we have , and in Cat we have , is there a 0-Yoneda?
If it is possible to extract an internal language from a topos, what results from a similar process applied to a 2-topos? Do we find that it supports a higher order categorified logic?
Re: 2-toposes
David asked:
Let me make some guesses, to get the ball rolling.
Trivially, finite categories must be an example. Then, since sheaves on a site give an important class of 1-toposes, surely stacks (of categories) on a site give an important class of 2-toposes.
I think Urs asked somewhere whether the 2-category of toposes is a 2-topos. I would have thought not, since Mark requires a duality involution. In the case of this must be , but this isn’t going to work for toposes: the opposite of a topos isn’t a topos.
I don’t think I know any examples of toposes except for sheaves on a site, finite sheaves on a site, and trivial variants thereof. I think it’s the case that the effective topos, and probably other realizability toposes, provide further examples. Also, one has the classifying topos for any geometric theory; I don’t know if that’s always a topos of sheaves. Maybe there are analogues of these things for 2-toposes. And maybe there are 2-toposes that are not the analogue of anything in the 1-dimensional world!
My guess: a 0-topos is just a set. Agreed: the set should be a paradigmatic example.
Well, a -category is a truth value in the classical sense (i.e. or ), and there’s meant to be just one -category, somehow corresponding to the truth value . (I suppose I mean “corresponding” in the same way that the -categories and correspond to the -categories and , and that a -category corresponds to the discrete -category on it.) Also, the exponentiation of truth values is surely implication: means . So I think the -Yoneda embedding is the statement where . How come that’s an equality? Well, both and are elements of , which is a -category, so they’re either equal or not — there’s no chance of mapping between them.
Now I have a question of my own. Cantor’s theorem says that , for sets . I spent a little while trying to imitate this for categories, to show that for categories (small if you like). But I couldn’t, the sticking point being that ‘op’. Can anyone (dis)prove this?