Can we insist on having a universal category (with ZFC and a hierarchy of classes)?

45 Views Asked by At

I'm curious whether there is any harm on insisting on the existence of a universal category. I'm also curious if we can make one in an extremely naive way by stapling a hierarchy of classes to $\mathrm{ZFC}$.

I'm also curious whether the category shown below has the property that I'm after, namely that every category has a full, faithful functor into $\mathrm{Universe}$.


First, let's start with $\mathrm{ZFC}$ as our set theory and add a hierarchy of types as in the simple theory of types.

For concreteness, we add an additional comprehension schema to ZFC of the following form:

$$ \varphi(x^n) \; \text{is a formula} \implies \{ x^n : \varphi(x^n)\}^{n+1} \; \text{is a set of type $n+1$} $$

We also insist that each of the ZFC axioms hold as originally stated when confined to fixed levels of the type hierarchy.

I will now attempt to construct a category $\mathrm{Universe}$.

First, I define an additional function symbol in my vocabulary $\mathrm{rank}$ that takes an object or a morphism in $\mathrm{Universe}$ and gives me its rank, the number of its type.

If $A^n$ is a set, then $\mathrm{rank}(A^n)$ is equal to $n$.

With that out of the way, every set of rank $n$ is an object of rank $n$ in $\mathrm{Universe}$.

Additionally, if $A^n$ and $B^n$ are sets and $f : A \to B$, then let $\{\cdots \{\{A_i\}^n, \{A_i, B_i\}^n\}^n \cdots \}^n$ be a function defined in the typical way as a collection of Kuratowski pairs. Because we constructed this set without using $\mathrm{TST}$'s comprehension scheme, the set representation of the function has type $n$, not $n+3$.

The rank of a morphism is the rank of its representation as set.

This completes the construction of $\mathrm{Universe}$. There are no arrows that cross levels of the type hierarchy.