Date: Fri, 30 Apr 1999 15:20:45 -0600
From: holmes@catseye.idbsu.edu
Subject: FOM: category theory in NF (or NFU)

In NF (or in NFU where we have a model theory so we can see what is
going on!) it is the case that one can have a category Sets whose
objects are all the sets and whose morphisms are all the functions
that there are.

The difficulty which arises is that the category of all sets and
functions (like all other universal categories of this kind in this
context) turns out to have unsatisfactory properties.  In particular,
it is not cartesian closed.

The intuition behind cartesian closedness is that any function from C
\times A to B is supposed to correspond to a function from C to
B^A.  But this correspondence doesn't work in NF, because it isn't
compatible with stratification.  Try it in type theory (with a
type-level ordered pair for simplicity):  for there to be functions
from (C \times A) to B, C, A, and B must be at the same type level, while
if there are to be functions from C to B^A, C must be at the same
type level as B^A, which is one type higher than either A or B.

Thus the usual method of showing that Set is cartesian closed will not
work in NF (or NFU).

Similar considerations show that Set cannot be shown to be Cartesian
closed using some nonstandard approach.  If Set were Cartesian closed,
there would be a one-to-one correspondence between arrows from V to V
(functions from the universe into the universe) and arrows from 1 to
V^V (functions with domain a fixed singleton and range the exponential
object).  But it is straightforward to show that the set of arrows
from 1 to A (functions from a fixed one-element domain to a set A) is
smaller than the set of arrows from V to V no matter what the set A is
taken to be.  The cardinality of the set of arrows 1 -> A is less than
or equal to the cardinality of the set of all singletons, which is
less than the cardinality of the set of all sets, which is equal to
the cardinality of the set of arrows from V to V.

For those who know what it is, the category of "strongly Cantorian"
sets and functions is cartesian closed and generally much more like
Set in a standard treatment -- but it is a proper class!

And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes
the gates of Cantor's paradise, that the       | Boise State U. (disavows all) 
slow-witted and the deliberately obtuse might | holmes@math.idbsu.edu
not glimpse the wonders therein. | http://math.idbsu.edu/~holmes