My original problem was what to do about the absolutely ghastly argument I complained about, showing that membership could be figured out in Set. I now have a solution, only a couple of whose 70 lines are needed to describe membership. The rest explicitly, arithmetically, and (except for infinite products) completely describes all the adjunctions of (a lightweight version of) the bicomplete topos Set. For starters, you need to accept Mike Barr's intuition that "the elements don't matter." If it bothers you that {2,4,17} is not "in" my version of Set, you aren't looking at it from Mike's perspective. It's tempting to make Set even lighter weight than I do here by constructing it as Skel(Set). But while this is technically feasible, it makes the definition of limits and colimits on infinite sets obscure, and also loses a property I'll mention below in connection with a nice observation of John Isbell. Instead I retrace what I imagine is a familiar path for set theorists, but from the categorical perspective. I take the objects to be simply the ordinals, each defined as the set of ordinals less than it, and the maps to be all functions (in the usual sense) between ordinals. (So for all cardinals alpha, this Set has only alpha many sets of cardinality less than alpha, which is what I mean by lightweight.) This may well have been already proposed before, since it is so simple and solves my problem so directly. But if so then why didn't someone bring it up as an answer to my question? The ordinals being a transitive class, membership i \in j coincides with (global) strict inclusion i \subset j, which as will be seen below is definable as the left "local" inclusion of i into i+(j-i). This is ten times shorter than the method I complained about (Goldblatt 12.4) for calculating membership in Set! Here are some features of this version of Set. I'll abbreviate \omega to \w, \eta to \i, \epsilon to \e. * The full subcategory consisting of the finite sets is skeletal. * Since every set is well-ordered, by definition, Choice holds. * Since i+j=k is uniquely solvable in j for i<=k (this can be seen informally by deleting the first i elements of k and taking j to be the order type of the residue), it follows that monus (nonnegative minus) can be defined, denoted k-i. (Note that i+j=k is not uniquely solvable in i, witness i+\w=\w which has all finite ordinals as solutions while i+\w=\w+1 has no solutions.) We also have ordinal ("integer") division i/j and remainder i%j, see below. * The *global* inclusion (assumed proper) of i into j is definable, namely as the "local" inclusion of i into i+(j-i) (meaning the first half of the unit of the adjunction defining +, at (i,j-i)), just when this is not the identity on i. (For j <= i, j-i = 0, making the local inclusion the identity.) The global inclusions make Set an irreflexive poset, identical to membership except that we do not normally speak of membership of x in y as a map, only as the truth of the binary relation of membership at the object pair (x,y). If for some crazy reason we want to represent the membership relation by maps in Set, the global inclusion maps are the obvious choice. * The isomorphism 1=>x = x is the identity 1_x, and similarly for the isos \rho: x*1 = x, \lambda: 1*x = x, and \alpha: (x*y)*z = x*(y*z) making Set a strict cartesian closed category. I wrote = rather than tilde to avoid a repeat of yesterday's screwup with caret, but in fact these are equalities in the strongest sense: they make \rho, \lambda, and \alpha all identity natural transformations. Isbell's argument in CTWM VII.1 shows that we can't *always* make \lambda,\rho,\alpha identities, even in a CCC like Skel(Set). In the present context Isbell's argument yields more, namely that any construction we use to further reduce Set from the ordinals to a skeletal category *must* weaken these identities to isos. What saves the day for ordinals is that when x,y,z are countably infinite, x*y and (x*y)*z get to be different infinite ordinals. Isbell's argument gives really nice insight into why set theorists find ordinals work better than cardinals: as cardinals, countable x*y and (x*y)*z have to be the *same* countable cardinal, ordinals create useful elbow room. (Without this category perspective, I don't know how to make a convincing case for ordinal arithmetic over cardinal, anyone know a noncategorical way?) * The inclusion of the rationals into the reals (as Dedekind cuts) is definable, but only as a local inclusion, not a global one, nor a monotone one with respect to the well-ordering of the reals. Set well orders the reals "randomly," and we get to probe around in the resulting well-ordering after the "big coin toss" and sniff out some (all?) aspects of its crazy choices. (Use the global inclusion of 1 into the reals to locate the "least" real "0", which can now be compared with the "real" additive identity of the reals, 0.0.) But because it depends on the coin toss it is not mathematics, just unrepeatable noise. * But this isn't to say that every uncountable ordinal looks random. The least uncountable ordinal \w_1 *is* ordered predictably and repeatably, and that order *is* genuinely mathematical (to believers in \w_1 anyway). There's presumably a lot more to say about Set defined this way, but this is way overlength already, so let me push on to describe the category Set itself. The description talks about 0 and successor early on; these can be understood either externally starting from an already constructed Set (less demanding pedagogically) or internally as a purely categorical definition of Set (in terms of constants 0,1,+ denoting initial and final objects and a coproduct), which will inevitably seem circular just like ZF seems circular. ====================Light Set---V.R. Pratt--3/13/96=========== I'll start from the class of von Neumann ordinals, each the set of all ordinals less than it (sorry, Mike), and define all small sums and products, (co)equalizers, and the classified subobjects. I'll follow the standard ordinal conventions for binary sum and product, which make 1+\w = \w < \w+1 and 2*\w = \w < \w*2. We need some auxiliary operations on ordinals. i/j = the least k satisfying i < j*(k+1) i%j = i - j*(i/j) (i modulo j) Exercises. i <= j*(i/j), i%j < j. Binary sums (for illustration). To form i+j, form j' by adding i to the *elements* of j (recursively), and take i+j to be i union j', with the evident inclusions. (This is not commutative in general, as noted earlier.) This generalizes to all small sums as follows. Given a family n_i of ordinals indexed by i<I (I=2 for binary sums), take their sum to be the least ordinal s such that there exists a family f_i of monotone injections f_i:n_i->s such that i<j<I, h<n_i, k<n_j -> f_i(h)<f_j(k). For the rest of the adjunction defining this sum, take the unit \i_<n_i> to be <f_i> and the counit \e_k to be \n.n%k (*not* \n.n%I). Binary products (for illustration). Form i*j as the sum of j copies of i, with the evident projections. (Not commutative in general.) Infinite products are a well-known problem for ordinal arithmetic, starting with \w copies of 2. The problem is to well-order the continuum. Choice says only that a well-ordering exists, we can't determine one by the constructive methods that work on everything else in this note. We just do our best. Given a family n_i of ordinals indexed by i<I, take their product to be the least ordinal p such that there exists a jointly monic family f_i of monotone surjections f_i:p->n_i (the projections) such that for all x<y<p, if there exists a largest j such that f_j(x) != f_j(y), then f_j(x) < f_j(y). The projections form the counit while the unit is the linear function \n.an where a=1+sum(n_i,i+1<I) (the brick's diagonal). The incompleteness of this specification arises when such a largest j does not exist. Note that care is taken not to contradict the definition for finite products, which *does* completely specify the adjunction for product. Exponential ij. Defined as the product of j copies of i (inheriting the infinite product problem when j is infinite). The unit of the defining adjunction (-j right adjoint to j*-, not -*j) has for its morphisms linear (!) functions an+b where a = sum((ji)k,0<=k<j), b = sum(ki(ji)k,0<=k<j). The counit (evaluation map) at i is the function \n.((n/j)/i(n%j))%i. This works by (i) projecting out the function part of n as n/j and the argument part as n%j (ii) evaluating by "shifting" and "masking" to pick out "digit" n%j in radix i. Theorem: this function is the evaluation map. (So this weird-looking function is not an "implementation hack" at all, it's the unique function for the job.) Subobject classifier: Given f:i->2, the associated subobject is the least j such that there exists a monotone injection g:j->i such that fg = 1!. Theorem: such a g:j->i exists and is unique, and is the pullback of 1:1->2 along f. The equalizer of f:i->j and g:i->j is the subobject of i corresponding to the predicate on i "f(x)=g(x)". Theorem: this exists and is unique. The coequalizer object k of f:i->j and g:i->j is the subobject of j whose characteristic function p:j->2 is the predicate "is the least representative in its block". The coequalizer h:j->k maps each element of j to the least representative of its block. Theorem: h exists and is unique. Vaughan Pratt