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 would really like to know if there is some references about this or if someone has thought about it and could explain some details about this that seems a bit obscure to me.
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.
 A: (Toby Bartels wrote back, explaining that he was having some trouble logging in to his account here, but asking if I could post some comments he had. I'm going to post them under my name as Community Wiki, and invite him to edit this answer further once he's back, if he'd like -- or he can post separately of course.) 
I believe that local smallness follows (in conventionally strong foundations) from the other axioms (this is what the Elephant seems to say in C.2.2.8.vii), so the right thing to do should just be to remove it from the list of axioms, which I have now done at the nLab.  However, it would be good to have the argument written out in a clearly predicative way, to be certain.  I no longer have access to my copy of the Elephant (I had to check the wording of C.2.2.8 in Google Books), which I believe was my guide the last time that I was thinking through this, but hopefully I can find it in the library and extract an explicitly predicative and constructive argument from its proofs.
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! 
