What are “maps” between proper classes?

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 Bauer Apr 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 Brandenburg Apr 28 '11 at 8:46
My problem was that I simply did not know you could easily define ordered pairs of classes. – Jesko Hüttenhain Apr 28 '11 at 8:51
-1. I agree with Andrej Bauer. – Sergei Tropanets Apr 30 '11 at 14:16

http://en.wikipedia.org/wiki/Ordered_pair#Morse_definition

Definition:
A relation $R$ is functional if and only if for all ordered pairs $\langle x,z\rangle$ and $\langle y,w\rangle$ in $R$, if $x=y$ then $z=w$.

Definition: If $R$ is a relation, $\operatorname{Range}(R) = \{y : (\exists x)(\langle x,y\rangle \in R)\}$.

Definition: A map is an ordered pair $\langle R,C\rangle$ such that $R$ is a functional relation and $\operatorname{Range}(R) \subseteq C$.

-
I suppose it wouldn't hurt to mention that all of what you've written applies to classes equally well as to sets. – Andrej Bauer Apr 28 '11 at 8:12
I suppose you're right. – Ricky Demer Apr 28 '11 at 8:15
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üttenhain Apr 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 Bauer Apr 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üttenhain Apr 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:

1. Totality: $\forall x \in A . \exists y \in B . (x,y) \in f$
2. Single-valuedness: $\forall x \in A . \forall y, z \in B . ((x,y) \in f \land (x,z) \in f \implies y = z)$.

We usually write $f(x) = y$ instead of $(x,y) \in f$.

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üttenhain Apr 28 '11 at 8:43
Yes, you can record just $D$, but why would you do such an ugly thing? – Andrej Bauer Apr 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üttenhain Apr 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 Bauer Apr 28 '11 at 9:19
I kan't sspell. – Andrej Bauer Apr 28 '11 at 9:20

Instead of MK set theory + Morse ordered pair definition, is ARC set theory (F.A.Muller, "Sets, Classes, and Categories", 2001, Bibliography PDF) with the usual Kuratowski ordered pair an option?

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.

-