Skip to main content
2 of 2
added 2 characters in body
David Roberts
  • 35.5k
  • 11
  • 124
  • 349

One thing that a universe $U$ gives you is that the sets and function in it form an internal full subcategory $USet$ of your ambient category $Set$ of sets . The idea is that the collection of objects forms a set, hence an object of $Set$. Then the collection of functions in $U$ from $X$ to $Y$, say, forms a set $USet(X,Y)$. However, the 'fullness' condition is that we can consider $X$ and $Y$ themselves as objects of $Set$, by considering the sets of their elements, $\underline{X} := USet(1,X)$ and $\underline{Y} := USet(1,Y)$ respectively, and then the set of functions $Set(\underline{X},\underline{Y})$ is the same as the set of functions $USet(X,Y)$ (isomorphic, not equal, generally). This is what Zhen refers to when he mentions hom-sets are preserved.

Notice here that $X$ and $Y$ are not sets, rather they are functions $1 \to Obj(USet)$, and to see them as sets we have to externalise them (note that for a category theorist, functions aren't necessarily sets).

For category theorists: a universe gives you a logical, full sub-fibred-topos of the fibred topos $cod\colon Set^\mathbf{2} \to Set$, and this definition extends to any topos $E$ replacing $Set$. This is a much nicer (from a category-theoretical perspective), and purely category-theoretic definition of a universe, independent of how one defines the category of sets. To consider only a model of set theory, one would take a model of the geometric theory 'well-pointed topos with AC and NNO' in $Set$, or worse (:-P) an internal relation modelling $\in$ from ZFC. You would have no control on the hom-sets of such a thing, and there would be no relation between 'internal' truth and 'external' truth.

David Roberts
  • 35.5k
  • 11
  • 124
  • 349