# Are there any type theories in which proper classes are presented?

I'm more of a computer scientist than a mathematician, now studying category theory. In CT, there are categories that are too big to be sets, e.g. the category of all sets/groups/small categories. As far as I know large categories can be constructed with proper classes. I wonder if there's something that roughly corresponds to classes in the sense of NBG set theory. Clearly, classes are not constructive, but maybe it could be added as axioms purely to do math without any computation meaning? How is there (not) such a type theory?

Let's say that the equality or the function arrow forms a (∞-)category, to model itself in the type theory, the set (or whatever you want to call that) of it would definitely be too big considering all of the types including universes. That's why I'm asking for a proper class.

There's nothing inherent in the notion of "class" that makes it non-constructive. Arguably, the non-reified notion of "class" that would be used in, e.g. ZF, is more constructive than that of a set. This notion of "class" more or less corresponds to a (unary) logical predicate. In some cases we may have a set $X$ such that for the predicate $\varphi$, $\varphi(x) \Leftrightarrow x \in X$ in which case we may say that $\varphi$ "is a set". Now why do I say that this may be more constructive than a set? Well, in this notion as "class" is essentially a formula, i.e. a finite collection of symbols in the formal system within which we're working. For example, the "class" of all sets is the formula $\varphi(x) \equiv \top$. On the other hand, I can easily postulate the "existence" of all kinds of sets for which there is no (finite) formula corresponding to them. For example, simply combine the axiom of infinity with the powerset axiom; most elements of $\mathcal{P}(\mathbb{N})$ cannot be described by any (finite) formula $\psi$. That is, there can be (and are in the "standard" model) elements $X \in \mathcal{P}(\mathbb{N})$ for which there is no formula $\psi$, not containing $X$, such that $\psi(x) \Leftrightarrow x \in X$. The constant reference to "size" is a bit of a red herring. A (very) similar situation happens with computability. For most (Turing-complete) programming languages I can (relatively) easily, possibly even trivially, make a computable function that picks out which bitstrings correspond to programs. I can't, however, make a computable function that picks out which bitstrings correspond to halting programs, even though it's surely the case that a halting program is a program. Returning to constructivity, with this notion of "class" the "constructiveness" of a "class" depends on the constructiveness of the logic in which we're working, while the constructiveness of a set depends on the logic and the non-logical axioms which we assume.

In a system like NBG, a separate notion of "class", i.e. a specific sort, is formulated. At this point we can axiomatically declare the existence of classes just like we do with sets. Whether this is constructive will depend on our logic and the non-logical axioms we assume just as it did for sets in the ZF-like scenario.

Turning to type theory, the first thing to note is that a type theory isn't a theory in FOL (or some other logic) like set theory is; it's a different logical framework entirely. Cartesian products of sets or function spaces are constructions in set theory which is itself axiomatized in first-order logic. Product types and function types, on the other hand, are logical connectives of type theory.

Structurally, a "class" in the ZF-like sense, corresponds to a type. More tightly, if $S$ is the type of "sets", then a natural interpretation of a class would be a subset type $\{s \in S\mid \phi(s)\}$ which more or less corresponds to the dependent sum type where $\phi(s)$ is propositionally truncated, i.e. $\Sigma s:S.||\phi(s)||$. The "class" of all "sets" would then essentially be $S$ itself. In a NBG approach, there'd actually be a separate type $C$ of "classes". However, both of these correspond to what would happen if you axiomatized ZF/NBG set theory in a (dependent) type theory, i.e. a "set" would be an inhabitant of $S$ in this case.

What is typically done, though, is view types as the analogue of sets. Then the analogue of the problem of the "set" of all sets is a "type" of all types. The usual solution to this nowadays is a universe. Adding a universe type to a type theory is the analogue of the NBG approach. There really isn't room for an analogue of ZF-like "classes". You could add judgements for "meta-types" and have a language of "meta-types" whose inhabitants are types. This would give you more flexibility (as the designer of the logic) than using a universe. You can do this even if you also have universes.

In practice variants on Martin-Löf type theory usually have not just a universe, but a whole infinite hierarchy of them as realized in e.g. Agda and Coq. This readily allows you to talk about small and large categories. If an infinite number of universes is still not enough for you, there are notions of superuniverses. The superuniverse (or a related notion) can then serve as your "proper class" if you want. Note, all of this is constructive.

• I guess what I expect is what you call "meta-types". I kind of doubt that a large category like the one presented in HoTT can be formalized because it talks about all types including universes. Does resorting to typical ambiguity or superuniverses deal with the problem properly? – 盛安安 Feb 2 '17 at 10:05
• By analogy to formulating the notion of a category of all types in MLTT with a single universe, my guess is that for MLTT with universe polymorphism (but not just typical ambiguity) you could show the universes satisfy the laws of an $\infty$-groupoid, say, but you couldn't make a type of $\infty$-groupoids such that the universe hierarchy inhabited it as a carrier. My impression is with a superuniverse, you would be able to make such a type, though it wouldn't apply to the superuniverse itself. – Derek Elkins Feb 2 '17 at 10:58