Dear Steve, I do understand your intentions. But I think one cannot mess with foundations and in particular not with Russell's insight that there is not a set of all sets. Most mathematicians either don't care and consider these kind of things as a nuisance. In type theory one definitely doesn't try to work with a type of all types. Universes have to be taken seriously but one want's to keep them in the background (i.e. avoid "universe cycles" as was done in LEGO as implemented by Randy Pollack). I personally think that all mathematics needs a foundation. ZFC set theory with the axiom that all sets are elements of some Grothendieck universe is a formidable foundation of mathematics. Set theory allows one to formulate irrelevant (i.e. not iso-invariant) questions one may want to stick to some type theory where they can't even be formulated. But even there cannot exist a top most (all inclusive) universe. Happy New Year, Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]