Why does the CwF definition require a set of types under a context rather than a class of types?

Question

In "Syntax and Semantics of Dependent Types" at the top of page 24, Martin Hoffman describes $\mathit{Ty}_{\mathcal C}(\Gamma)$ as the collection of semantic types under context $\Gamma$.

It makes sense that he used the word collection rather than set, because in the set-theoretic CwF he describes, the types under a context $\Gamma$ are $\Gamma$-indexed families of sets. It is well known that this is a proper class.

However, on page 26 he provides a more abstract definition where a CwF is a Fam-valued presheaf. Such a presheaf maps an object $\Gamma$ of the context category onto a pair (Ty($\Gamma$), $\mathit{Tm}(\Gamma,\sigma)_{\sigma \in \mathit{Ty}(X)}$). The left component of an object of Fam is an index set, so this contradicts the earlier definition and seems incorrect. Most literature on CwF's takes the same approach. Would it be more appropriate to use the category of class-indexed families of sets as the codomain category for these presheaves?

Answer 1

There is nothing special about types with respect to sizing, compared to what we already have in ordinary categories. A small category has a set of objects, and for each pair of objects, a set of morphisms between them; so morphisms are an indexed family of sets. We can immediately extend this definition to small CwFs, where for each context we have a set of types.

All that happens, compared to categories, is that we have four underlying set families (objects, morphisms, types, terms) instead of just objects and morphisms, so we have more degree of freedom when choosing the sizes involved. E.g. we have locally small categories where the set of objects is large (in some sense) and the sets of morphisms are small, and we're likewise free to pick relative sizes of all involved sets in CwFs.