When defining a functor (between categories), I am usually told that it assigns to each object of the source category an object of the target category. I do not find this very satisfactory since we are dealing with proper classes here. Judging by the definition, it must be possible to have the concept of a "map" between proper classes. I would like to know what exactly that is and how it is defined.

I have attempted to read some books on set theory in search for an answer, but they all treat classes very briefly and never mention the possibility of having anything like a map between two of them. I would be just as happy if you could point me to a book where this is explained.

This is becoming a very much non-research question. I think perhaps we can close the question. On the other hands, foundational questions on MO seem to be generally below research level and have mostly educational value, which would be a reason to keep this one.
–
Andrej BauerApr 28 '11 at 8:35

A class is given by a formula (which it defines). If $C,D$ are classes, then a map $C \to D$ is simply a class $f$ which defines a "map" $C \to D$ in the obvious sense: For all $x \in C$, i.e. all elements satisfying the formula defining $C$, there is exactly one $y \in D$, i.e. an element satisfying the formula defining $D$, such that $y = f(x)$, i.e. $(x,y)$ satisfies the formula defining $f$. As an exercise, prove that $V \to V, x \mapsto x + 1 := x \cup \{x\}$ is a map, where $V$ is the universe.
–
Martin BrandenburgApr 28 '11 at 8:46

1

My problem was that I simply did not know you could easily define ordered pairs of classes.
–
Jesko HüttenhainApr 28 '11 at 8:51

So, I am guessing, this is only possible if I use Morse-Kelley and not with ZFC alone? My problem was that I thought $C\times D$ was not really defined if $C$ and $D$ were proper classes.
–
Jesko HüttenhainApr 28 '11 at 8:18

It's possible with ZFC as well. Of couse $C \times D$ is defined for classes, just use the same definition as for sets.
–
Andrej BauerApr 28 '11 at 8:34

Well, now, that helped clarify a lot. Thank you both a lot, that trivial little miscomprehension caused me years of agony. I would really like to accept both answers, but apparently you can't do that.
–
Jesko HüttenhainApr 28 '11 at 8:37

Your question sounds like your preferred foundation is set theory, so let me speak in terms of set theory. A map $f : A \to B$ between sets is a functional relation, i.e., a subset $f \subseteq A \times B$ satisfying:

The same definition applies to classes. A map $F : C \to B$ between classes $C$ and $D$ is a subclass of $C \times D$ which is total and single-valued.

Exercise (allowed since this is not a research question): the domain and codomain of a function $F : C \to D$ cannot be recovered from the functional relation $F$. (If $C$ and $F$ are empty, how do we recover $D$?) Therefore, the object part of a functor must be a triple $(C,D,F)$ rather than just $F$. But how can we form ordered triples of classes?

Wait, can't the domain be recovered from the relation by Totality? I mean, if this really works for classes the same way it does for sets. Then, a functor would only have to be a pair $(F,D)$ and I just learned that that's easily possible.
–
Jesko HüttenhainApr 28 '11 at 8:43

Yes, you can record just $D$, but why would you do such an ugly thing?
–
Andrej BauerApr 28 '11 at 8:44

Well then, beauty it is! If you can have ordered pairs of classes, however, it should not be a problem to have any finite ordered tuple of classes, right? (So in particular, triples)
–
Jesko HüttenhainApr 28 '11 at 8:49

Right, but please don't confused the product $C \times D$ of two classes with an ordered pair $(C,D)$ of classes. That's what the exercise was for.
–
Andrej BauerApr 28 '11 at 9:19

ARC supposedly proves the existence of the $n$-th power-class of the set universe V for any $n \in \mathbb{N}$, and all so-called "good" classes provably exist, good classes being the class of all sets and "the powerclass and the union-class of a good class, and the union-class, the intersectionclass, the complement-class, the pair-class, the ordered pair-class, and the Cartesian product-class of any finite number of members of one good class".

According to the cited paper, ARC is consistent relative to ZFC plus a strongly inaccessible cardinal axiom.
I think that this set theory looks quite nice, so I'm wondering why it didn't take off at all.
The formal proofs should be in Muller's PhD thesis, which I don't have access to.