MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).

2 added 176 characters in body

Here's

Since you don't seem to want to leave ZFC, here's a taste of the issues you might face if you try to work with a stratified universe. (Here I mean the ordinary English word stratified’, rather than a formally stratified logical system like Russell's type theory.) First, a warm-up:

Exercise. Develop the theory of finite categories and locally finite categories.

Now, let $\lambda$ be any infinite limit ordinal greater than $\omega$. The set $V_\lambda$ (!) of all sets of rank less than $\lambda$, together with the set (!) of all functions inside $V_\lambda$, forms a small category $\textbf{Set}_\lambda$ satisfying the axioms of ETCS (the elementary category of sets). As long as you don't try to invoke unbounded separation or replacement, ETCS is a reasonable foundation in which to do mathematics. Thus, we obtain an infinite ascending sequence of full subcategories $$\textbf{Set}_{\omega + \omega} \subset \textbf{Set}_{\omega + \omega + \omega} \subset \cdots \subset \textbf{Set}_{\infty}$$ where $\textbf{Set}_{\infty}$ denotes the (meta)category of all sets. Immediately we have some problems to resolve:

1. Since each $\textbf{Set}_\lambda$ is a priori a different category, there is no reason to believe that limits and colimits in $\textbf{Set}_\lambda$ will agree with limits and colimits in $\textbf{Set}_\kappa$, if $\lambda \lt \kappa$. Fortunately, it is a fact that if $\mathcal{D}$ is a full subcategory of $\mathcal{C}$, and the limit (resp. colimit) $X$ of a diagram in $\mathcal{D}$ exists in $\mathcal{C}$, then as long as $X$ is in $\mathcal{D}$, $X$ will be the limit (resp. colimit) of that diagram in $\mathcal{D}$. In more sophisticated words, the inclusion of a full subcategory always reflects limits and colimits. The trouble is that it may not preserve limits and colimits.

2. None of the categories $\textbf{Set}_\lambda$ have all small limits or colimits. This is due to an observation of Freyd: a small category with all small limits (or colimits) is a preorder category. However, it has all internally-indexed limits and colimits, in the following sense: if $\mathbb{C}$ is an internal category in $\textbf{Set}_\lambda$, meaning $\operatorname{ob} \mathbb{C}$ and $\operatorname{mor} \mathbb{C}$ are sets in $\textbf{Set}_\lambda$, and $A : \mathbb{C} \to \textbf{Set}_\lambda$ is an internal diagram (see [CWM, Ch. XII, § 1]), then $\varprojlim A$ and $\varinjlim A$ both exist in $\textbf{Set}_\lambda$ via the usual construction. In particular, every $\textbf{Set}_\lambda$ is closed under finite limits and colimits.

3. Though $\textbf{Set}_\lambda$ is a small category, it is not an internal category in $\textbf{Set}_\lambda$ itself! Instead, we must go up the hierarchy in order to realise $\textbf{Set}_\lambda$ as an internal category. This a priori seems to mean that we cannot talk about a genuine functor $\mathbb{C} \to \textbf{Set}_\lambda$, where $\mathbb{C}$ is an internal category in $\textbf{Set}_\lambda$, without leaving $\textbf{Set}_\lambda$, and once we leave $\textbf{Set}_\lambda$ we have to worry about whether the results obtained in a bigger category $\textbf{Set}_\kappa$ are still valid in our original category $\textbf{Set}_\lambda$, cf discussions about "change of universe" in SGA.

To be clear, this is a non-trivial problem. It is not so easy to replace a genuine functor $\mathbb{C} \to \textbf{Set}_\lambda$ with an internal diagram in $\textbf{Set}_\lambda$. For example, let $\omega \to \textbf{Set}_{\omega + \omega}$ be the functor $n \mapsto \omega + n$. The obvious way of turning this into an internal diagram uses the axiom of replacement and results in a set of rank at least $\omega + \omega$ – in other words, it is not internal to $\textbf{Set}_{\omega + \omega}$! Nonetheless, for cardinality reasons, it is true that every genuine functor $\mathbb{C} \to \textbf{Set}_\lambda$ is isomorphic to an internal diagram in $\textbf{Set}_\lambda$.

There are other subtleties to think about. A well-known result of Kan implies that the category of presheaves on a small category $\mathcal{C}$ has $\mathcal{C}$ as a colimit dense subcategory via the Yoneda embedding $\mathcal{C} \to [\mathcal{C}^\textrm{op}, \textbf{Set}_\infty]$, but if $\mathcal{C}$ is only a locally small category, then this is in general false: in other words, the relative sizes of $\mathcal{C}$ and $\textbf{Set}_\infty$ matter!

1

Here's a taste of the issues you might face if you try to work with a stratified universe. First, a warm-up:

Exercise. Develop the theory of finite categories and locally finite categories.

Now, let $\lambda$ be any infinite limit ordinal greater than $\omega$. The set $V_\lambda$ (!) of all sets of rank less than $\lambda$, together with the set (!) of all functions inside $V_\lambda$, forms a small category $\textbf{Set}_\lambda$ satisfying the axioms of ETCS (the elementary category of sets). As long as you don't try to invoke unbounded separation or replacement, ETCS is a reasonable foundation in which to do mathematics. Thus, we obtain an infinite ascending sequence of full subcategories $$\textbf{Set}_{\omega + \omega} \subset \textbf{Set}_{\omega + \omega + \omega} \subset \cdots \subset \textbf{Set}_{\infty}$$ where $\textbf{Set}_{\infty}$ denotes the (meta)category of all sets. Immediately we have some problems to resolve:

1. Since each $\textbf{Set}_\lambda$ is a priori a different category, there is no reason to believe that limits and colimits in $\textbf{Set}_\lambda$ will agree with limits and colimits in $\textbf{Set}_\kappa$, if $\lambda \lt \kappa$. Fortunately, it is a fact that if $\mathcal{D}$ is a full subcategory of $\mathcal{C}$, and the limit (resp. colimit) $X$ of a diagram in $\mathcal{D}$ exists in $\mathcal{C}$, then as long as $X$ is in $\mathcal{D}$, $X$ will be the limit (resp. colimit) of that diagram in $\mathcal{D}$. In more sophisticated words, the inclusion of a full subcategory always reflects limits and colimits. The trouble is that it may not preserve limits and colimits.

2. None of the categories $\textbf{Set}_\lambda$ have all small limits or colimits. This is due to an observation of Freyd: a small category with all small limits (or colimits) is a preorder category. However, it has all internally-indexed limits and colimits, in the following sense: if $\mathbb{C}$ is an internal category in $\textbf{Set}_\lambda$, meaning $\operatorname{ob} \mathbb{C}$ and $\operatorname{mor} \mathbb{C}$ are sets in $\textbf{Set}_\lambda$, and $A : \mathbb{C} \to \textbf{Set}_\lambda$ is an internal diagram (see [CWM, Ch. XII, § 1]), then $\varprojlim A$ and $\varinjlim A$ both exist in $\textbf{Set}_\lambda$ via the usual construction. In particular, every $\textbf{Set}_\lambda$ is closed under finite limits and colimits.

3. Though $\textbf{Set}_\lambda$ is a small category, it is not an internal category in $\textbf{Set}_\lambda$ itself! Instead, we must go up the hierarchy in order to realise $\textbf{Set}_\lambda$ as an internal category. This a priori seems to mean that we cannot talk about a genuine functor $\mathbb{C} \to \textbf{Set}_\lambda$, where $\mathbb{C}$ is an internal category in $\textbf{Set}_\lambda$, without leaving $\textbf{Set}_\lambda$, and once we leave $\textbf{Set}_\lambda$ we have to worry about whether the results obtained in a bigger category $\textbf{Set}_\kappa$ are still valid in our original category $\textbf{Set}_\lambda$, cf discussions about "change of universe" in SGA.

To be clear, this is a non-trivial problem. It is not so easy to replace a genuine functor $\mathbb{C} \to \textbf{Set}_\lambda$ with an internal diagram in $\textbf{Set}_\lambda$. For example, let $\omega \to \textbf{Set}_{\omega + \omega}$ be the functor $n \mapsto \omega + n$. The obvious way of turning this into an internal diagram uses the axiom of replacement and results in a set of rank at least $\omega + \omega$ – in other words, it is not internal to $\textbf{Set}_{\omega + \omega}$! Nonetheless, for cardinality reasons, it is true that every genuine functor $\mathbb{C} \to \textbf{Set}_\lambda$ is isomorphic to an internal diagram in $\textbf{Set}_\lambda$.

There are other subtleties to think about. A well-known result of Kan implies that the category of presheaves on a small category $\mathcal{C}$ has $\mathcal{C}$ as a colimit dense subcategory via the Yoneda embedding $\mathcal{C} \to [\mathcal{C}^\textrm{op}, \textbf{Set}_\infty]$, but if $\mathcal{C}$ is only a locally small category, then this is in general false: in other words, the relative sizes of $\mathcal{C}$ and $\textbf{Set}_\infty$ matter!