Original problem
A few days ago I asked the following question on Stackexchange. Essentially, I was asking how to verify via one of the adjoint functor theorems that the forgetful functor from $\mathbf{Mon}$, the category of small monoidal categories with monoidal functors, to $\mathbf{Cat}$, the category of small categories, has a left adjoint. I have received a nice answer by Vladimir Sotirov.
My proposed solution
After reading his answer, I have been trying to understand what assumptions enter in the proof, and came up with the following "alternative" construction of the solution set.
Let $Y$ be a small category. Let $\kappa_Y$ be the least infinite cardinal that bounds the cardinality of the morphism set of $Y$. Define the proper class $Z$ as those monoidal categories that have a morphism set bounded by $\kappa_Y$.
Define an equivalence relation on this class $Z$ by letting two monoidal categories be equivalent if there exists a monoidal equivalence between them. By Scott's trick we obtain a class $\mathbf{X}$ of equivalence classes (i.e. for all $z \in Z$ there exists a unique $X \in \mathbf{X}$ such that there exists a $x\in X$with $x \sim z$), where any equivalence class $X \in \mathbf{X}$ is a set. Since given a category $C$ the class of monoidal categories $X$ with $U(C)=X$ is a set, we know that the class $\mathbf{X}$ is a set. Using the axiom of choice we obtain a set of representatives $\overline{\mathbf{X}}$ (that is, a set such that for all $z \in Z$ there exists a unique $x \in \overline{\mathbf{X}}$ such that $z \sim x$). One verifies that $\overline{\mathbf{X}}$ is a solution set.
My questions
- When I say things like "Define the proper class $Z$ …" or "Define an equivalence relation on this class" I am not working within $\sf ZFC$, right? That is, classes cannot be defined in $\sf ZFC$.
- Can I construct the set (?) $S$ as I did above, and what assumptions do I need for that? That is, what is the realm of discourse here? How can I work with classes if they do not exist in my universe?
- Here is my attempt at answering the questions in the two bullet points above. Is it correct? Let $\phi(x)$ be the predicate "$x$ is a monoidal category with morphism set bounded by $\kappa_X$“ (More precisely, $\phi(x)$ is a formula with one free variable written in the language of $\sf ZFC$.) When I write "Define the proper class $Z$ of monoidal categories with morphism set bounded by $\kappa_X$", I am not actually saying $\exists Z(z \in Z \leftrightarrow \phi(z))$, but I only consider the formula $\phi(x)$ (or maybe an equivalence class of formulas, where two are equivalent if they can be proved from one-another in $\sf ZFC$). When I say "Define an equivalence relation on $C$…", I am actually considering the formula $\phi(x) \land \phi(y) \land \psi(x,y)$, where $\psi(x,y)$ is the formula in $\sf ZFC$ that encodes the equivalence relation from above. Now, defining equivalence classes of an equivalence relation on a class in the above sense is problematic. For sets, we can employ the power set axiom. For classes, a workaround is Scott's trick. We consider the class $Z$ (again actually a formula), and for a chosen (?) $x \in Z$ define the equivalence class of $x$ via a predicate that essentially says "y is equivalent to x". Now Scott's trick constructs a set from this equivalence class by using the axiom of foundation. Next we consider the class (again a formula with one free variable, say $\varphi(x)$) of all those sets so constructed. We somehow have to now prove that $\exists \overline{\mathbf{X}}(x \in \overline{\mathbf{X}} \leftrightarrow \varphi(x))$.