More formally, define m+n for m and n in N as (But note that this style of definition is feasible for the ZFC numerals as well, but more circuitous: the form of the NFU definition facilitates set manipulations while the form of the ZFC definition facilitates recursive definitions, but either theory supports either style of definition). The two implementations are quite different. In ZFC, choose a representative of each finite cardinality (the equivalence classes themselves are too large to be sets); in NFU the equivalence classes themselves are sets, and are thus an obvious choice for objects to stand in for the cardinalities. However, the arithmetic of the two theories is identical: the same abstraction is implemented by these two superficially different approaches. Equivalence relations and partitions A general technique for implementing abstractions in set theory is the use of equivalence classes. If an equivalence relation R tells us that elements of its field A are alike in some particular respect, then for any set x, regard the set as representing an abstraction from the set x respecting just those features (identify elements of A up to R). For any set A, a set is a partition of A if all elements of P are nonempty, any two distinct elements of P are disjoint, and . For every equivalence relation R with field A, is a partition of A. Moreover, each partition P of A determines an equivalence relation . This technique has limitations in both ZFC and NFU. In ZFC, since the universe is not a set, it seems possible to abstract features only from elements of small domains. This can be circumvented using a trick due to Dana Scott: if R is an equivalence relation on the universe, define as the set of all y such that and the rank of y is less than or equal to the rank of any . This works because the ranks are sets. Of course, there still may be a proper class of 's. In NFU, the main difficulty is that is one type higher than x, so for example the "map" is not in general a (set) function (though is a set). This can be circumvented by the use of the Axiom of Choice to select a representative from each equivalence class to replace , which will be at the same type as x, or by choosing a canonical representative