Grothendieck Topos

Question

If,

1. A Grothendieck Topos is equivalent to the Category of sheaves on some site (C,J).
2. 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).
3. 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?

Answer 1

Giraud's axioms do explicitly refer to the category of sets, through every use of the term "small". E.g. taking the formulation at ncatlab, the category of sets is explicitly referred to by the requirement that $E$ be locally small, and that $E$ have all small coproducts.

I don't know nearly as much about it as I like, but I understand you can replicate broad swaths of the theory of Grothendieck toposes starting from any base topos $S$: you can talk about internal sites, internal presheaves, and internal sheaves, and then the toposes $E$ that comes with a bounded geometric morphism $E \to S$ are precisely those toposes that are equivalent to a categories of internal sheaves over an internal site. e.g. see base topos and bounded geometric morphism from ncatlab.

I don't know what the relative version of Giraud's axioms are, but I imagine they would look quite similar.

Answer 2

You don't necessarily have to see $Set$ as classical set theory axiomatized by e.g. $ZFC$, $NBG$ or the like. Instead you can think of $Set$ as being characterized as an abstract category without any reference to classical set theory (i.e. without reference to membership relation).

See Lawvere, An elementary theory of the category of sets (pdf)

---

See also Category theory without sets (stack exchange article)