Re: V-included categories

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

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/ ]