Definition least_univ_eq
Definition.
least_univ_eq
least_univ A = ⋂{U | univ U ∧ A ∈ U}
The least
Grothendieck universe
that contains A.