Skip to main content
Source Link
Simon Henry
  • 42.4k
  • 5
  • 107
  • 205

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.