# Grothendieck toposes in (very) weak foundation

There is on the nLab page "Grothendieck topos" a part about the theory of Grothendieck toposes in weak foundation.

It claims that the equivalence for a category between the Giraud's axioms and being a category of sheaves over a site can be proved under very weak foundation: predicative (even without small set of functions), finitarist, constructive.

I am especially concern by the absence of sets of functions: without them Grothendieck toposes shouldn't be expected to be locally small, hence it does not seem possible to associate a sheave to an object $X$ being given a set of generators (because the sheave should be $Hom( \_ , X)$ which might not be a set). Maybe the theorem still holds by constructing a localization functor from a presheaves category to the "category of sheaves" but without a right adjoint, hence sheaves should not be set valued functors.

Also, it is not clear what a Grothendieck topology should be (more precisely what should be small ? this might explains the fact that sheafication don't preserve smallness )

I would also be interested in knowing if it is possible to weaken even further the foundations, for example by getting ride of quotient sets and still have a result of this kind.

• The section "Weak Foundations" first appears in Revision number 27, written by Toby Bartels. I may drop him a note about your post. – Todd Trimble Aug 13 '15 at 20:42
• Simon, you may be interested to know that there are (non-Grothendieck) boolean toposes that are not locally small: as such they have internal homs, which are the 'correct' 'set' of functions (working in the internal logic). These correspond to certain class-forcing models. Regarding a Grothendieck topology, one could replace it by a Lawvere-Tierney topology/local operator and see what one gets. – David Roberts Aug 14 '15 at 0:20
• That is indeed interesting. But Under weak fundation Grothendieck toposes are not going to be elementary topos, they are not expected to be cartesian closed if "sets" is not, and they are not going to have power objects if there is no power objects in "sets", so I'm sure one can use locale operators here either. – Simon Henry Aug 14 '15 at 7:59
• We can think about universal closure operators instead of local operators. – Zhen Lin Aug 14 '15 at 9:35
• Indeed we can, but as I mentioned it is not clear that sheaves should be a subcategory of small presheaves (the situation might be similar to what happen when you have a large site: the sheafification of a small presheaves might not be a small presheaf and what we want to consider is the category sheaves which are sheafication of small presheaves), in which case the closure operation is not a solution either... – Simon Henry Aug 14 '15 at 10:02

More speculatively, the classical proof that Giraud's axioms imply local smallness might have a strongly predicative variation proving, say, that there is a small generating set (possibly smaller than the original one) $G$ such that $\hom(G,X)$ is small for each $X$. That solves your problem of getting a Set-valued sheaf from an object, and it's trivial (but impredicative) to prove that a category with such a generating set must be locally small. But I'm not sure that it's actually correct!