What does the universe mean?

Question

The articles about functional programming, a lot of them have mentioned about the universe. I am reading the book "Category Theory for Programmers" by Bartosz Milewski and he has also mentioned about universe a lot of times. The question is, what does the universe mean in context of functional programming and category theory?

Answer 1

In the context of category theory, universes were introduced in order to bypass the paradoxes of set theory. For instance, Set is the category of sets, so its objects correspond to sets. The set of all objects in this category would be the set of all sets. But there is no set of all sets! Grothendieck introduced the idea of universes to deal with that. Essentially the set of all sets in a given universe is not a set in that universe--it's a set in the next bigger universe.

In programming, we have to deal with polymorphic functions, which are functions defined for all types. But all types don't form a set. So languages like Agda let you work with types within a given universe. They call the lowest universe Set, but Set itself is a member of Set₁ and so on.