This question is primarily a reference request. It arose from a personal coding/formalization project.
I am using a particular form of a definition of a category in ZFC. According to this definition, the sets $V_{\alpha}$ for limit ordinals $\alpha$ such that $\omega < \alpha$ replace the Grothendieck universes in the more conventional setting for the definition of a category. This approach is similar to what was originally proposed in Set-Theoretical Foundations of Category Theory [A] and later promoted in Set Theory for Category Theory [B] and other articles (e.g. [C, D]).
The primary problem associated with this definition is related to the lack of the Axiom of Replacement "closed in $V_{\alpha}$". However, various tricks were developed in the aforementioned articles to avoid this problem. Unfortunately, some of the theory behind these tricks seemed to be quite challenging to formalize using the technology that I was using (not impossible, but quite unwieldy and labor-intensive).
I have done some experiments in an attempt to avoid some of the aforementioned difficulties, and I found that the following condition is quite natural for the definition of an "$\alpha$-locally-small category" in this setting (and I hardly need anything larger than locally small for what I am doing): \begin{equation} \forall A \subseteq \mathcal{C}_{Obj}. \forall B \subseteq \mathcal{C}_{Obj}. (A \in V_{\alpha} \wedge B \in V_{\alpha}) \longrightarrow \bigcup_{a \in A} \bigcup_{b \in B} \text{Hom}_{\mathcal{C}} (a, b) \in V_{\alpha} \end{equation} Of course, it is also assumed that $\mathcal{C}_{Obj} \subseteq V_{\alpha}$. This condition also implies that the Hom-sets are $\alpha$-small. However, this condition still has to be combined with some of the simpler tricks described in [B] (e.g., to quote, "the correct definition of complete is 'having limits for all small functors'"), and I had to invent a few further tricks of my own to make the theory work. One important aspect of this condition (what I believe makes it work well) is that it provides closure with respect to taking the functor categories. That is, $\mathcal{C}^{\mathcal{J}}$ is $\alpha$-locally small provided that $\mathcal{C}$ is $\alpha$-locally small and $\mathcal{J}$ is $\alpha$-small ($\mathcal{J} \in V_\alpha$). Again, of course, this holds only in the augmented theory where $\mathcal{C}^{\mathcal{J}}$ is determined by the $\alpha$-small functors (see [B]).
My access to research literature is very limited at the moment and I have little social connection with the fields of foundations/pure mathematics. Therefore, I am not certain whether the aforementioned definition is already available in the research literature somewhere or, perhaps, it is part of the "folklore" already. Thus, my primary question is whether anyone had seen the aforementioned condition before in the context of a definition of a locally-small category in ZFC.
The secondary question is whether anyone can suggest any important theorem that holds in the conventional setting with the reference to locally small 1-categories but will fail when using the proposed condition. Thus far, I was able to find a way around such problems by strengthening the conditions for a given theorem to hold slightly (e.g., I coded Yoneda and the Freyd General Adjoint Functor Theorem).
References
- [A] Feferman S, Kreisel G. Set-Theoretical Foundations of Category Theory. In: Barr M, Berthiaume P, Day BJ, Duskin J, Feferman S, Kelly GM, et al., editors. Reports of the Midwest Category Seminar III. Heidelberg: Springer; 1969. p. 201–47. (Lecture Notes in Mathematics).
- [B] Shulman MA. Set Theory for Category Theory. arXiv:08101279 [math] [Internet]. 2008; Available from: http://arxiv.org/abs/0810.1279.
- [C] Blass A. The interaction between category theory and set theory. In: Gray JW, editor. Mathematical Applications of Category Theory. American Mathematical Society; 1984. (Contemporary Mathematics; vol. 30).
- [D] Rao VK. On Doing Category Theory within Set Theoretic Foundations. In: Sica G, editor. What is Category Theory? Polimetrica s.a.s.; 2006.
