an obstruction in NFU when using the Kuratowski pair: one defines as because of the type displacement of 2 between the pair and its projections, which implies a type displacement of two between a cartesian product and its factors. It is straightforward to prove that the product always exists (but requires attention because the inverse of T is not total). Defining the exponential operation on cardinals requires T in an essential way: if was defined as the collection of functions from A to B, this is three types higher than A or B, so it is reasonable to define as so that it is the same type as A or B ( replaces with type-level pairs). An effect of this is that the exponential operation is partial: for example, is undefined. In ZFC one defines as without difficulty. The exponential operation is total and behaves exactly as expected on cantorian cardinals, since T fixes such cardinals and it is easy to show that a function space between cantorian sets is cantorian (as are power sets, cartesian products, and other usual type constructors). This offers further encouragement to the view that the "standard" cardinalities in NFU are the cantorian (indeed, the strongly cantorian) cardinalities, just as the "standard" ordinals seem to be the strongly cantorian ordinals. Now the usual theorems of cardinal arithmetic with the axiom of choice can be proved, including . From the case the existence of a type level ordered pair can be derived: is equal to just in case , which would be witnessed by a one-to-one correspondence between Kuratowski pairs and double singletons : redefine as the c such that is associated with the Kuratowski : this is a type-level notion of ordered pair. The Axiom of Counting and subversion of stratification So there are two different implementations of the natural numbers in NFU (though they are the same in ZFC): finite ordinals and finite cardinals. Each of these supports a T operation in NFU (basically the same operation). It is easy to prove that is a natural number if n is a natural number in NFU + Infinity + Choice (and so and the first infinite ordinal are cantorian) but it is not possible to prove in this theory that . However, common sense indicates that this should be true, and so it can be adopted as an axiom: Rosser's Axiom of Counting: For each