Description: A Grothendieck universe contains all functions on its elements. (Contributed by Mario Carneiro, 10-Jun-2013)