There is on the [nLab page "Grothendieck topos"][1] 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.


  [1]: http://ncatlab.org/nlab/show/Grothendieck+topos#in_weak_foundations