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.
Madeleine Birchfield (Mar 31 2024 at 15:16):Do presheaf categories still have subobject classifiers if Set does not have a subobject classifier because one is a constructive predicativist?
Morgan Rogers (he/him) (Mar 31 2024 at 15:23):Did you already see the nLab page [[predicative topos]]?
Morgan Rogers (he/him) (Apr 01 2024 at 13:16):This got moved to another stream for some reason...
Graham Manuell (Apr 01 2024 at 15:18):Well, Set itself is a presheaf category. Or are you asking if there exists some other presheaf category that does have a subobject classifier? In case, the answer is positive, since the trivial topos 1 will always work.
Peva Blanchard (Apr 01 2024 at 16:26):I think the question refers to a specific model of Set theory (constructive predicativism). I understand from the question that, in this model, the category of Set-presheaves over a category does not have a sub-object classifier in general.
Mike Shulman (Apr 01 2024 at 17:52):Graham Manuell said:
Or are you asking if there exists some other presheaf category that does have a subobject classifier? In case, the answer is positive, since the trivial topos 1 will always work.
I suspect that is the only possibility. If is a nonempty category, then the geometric morphism is surjective (as its inverse image functor, which takes constant diagrams, is conservative since is nonempty). In ordinary topos theory this implies that the adjunction is comonadic, and the category of algebras for a left exact comonad inherits a subobject classifier. If that is also true predicatively (I haven't checked the proof), it would imply that if any nontrivial presheaf category has a subobject classifer, so does Set.