Definition. Grothendieck universe [002q]