The universal set, defined as the least Grothendieck universe that contains the natural numbers, see the least_univ operation. Basically this means, it behaves almost exactly like UnivCl, but it is a set rather than a proper class. Theorem Univ_is_univ shows that it is well-defined, the proof depends on the axiom of universes.