# What system was Grothendieck working in when he introduced universes?

I was reading that the universes which we now call "Grothendieck universes" were introduced by Grothendieck in order to avoid proper classes; from Grothendieck universe on Wikipedia:

The idea of universes is due to Alexander Grothendieck, who used them as a way of avoiding proper classes in algebraic geometry.

Now, the existence of such universes is axiomatized formally by Tarski's axiom in Tarski–Grothendieck set theory:

For every set $x$, there exists a set $y$ whose members include:

• $x$ itself;

• every subset of every member of $y$;

• the power set of every member of $y$;

• every subset of $y$ of cardinality less than that of $y$.

However, I was wondering, when Grothendieck initially introduced these universes:

• was he working in a formal theory, such as $\mathsf{ZFC}$, which he found insufficient and decided to augment with an axiom similar to Tarski's?
• or, was he working in naive set theory, which he nevertheless found to be insufficient for his purposes (perhaps thinking the existence of these sets was not guaranteed by intuition)?

I did some searching, but having not thoroughly combed the literature, I was not able to find the source(s) where he introduced universes; references are welcome.