If,
- A Grothendieck Topos is equivalent to the Category of sheaves on some site (C,J).
- A presheaf (on site (C,J)) is a contravariant functor P, from category C to the category of sets. A sheaf is a pre-sheaf equipped with a matching families map, from the sieves of J(B) to elements of PB (for any object B of category C).
- A Grothendieck Topos is also an Elementary Topos which obeys Giraud's axioms.
Then,
The main definition of a Grothendieck Topos in 1 and 2, explicitly refers to the category of sets. Sets can be formalized several different ways: PA, ZF(C), NBG. I presume this choice would impact in turn the definition of Grothendieck Topos.
The alternative definition in 3 of Grothendieck Topos, through Elementary Topoi, does not explicitly refer to sets or the category of sets. What formalization of sets is assumed in this definition? Else, what have I overlooked?