Dear Thomas, What I'm curious to understand is how inevitable is a certain practical behaviour of universes. In many situations we know they are foundationally necessary, but we still seek ways to disregard them in everyday mathematics. If we try to use generalized spaces as our prime notion of collection, instead of sets, it begins to look different. We still have universes of a kind. For example the object classifier is a universe whose elements are sets (discrete spaces). But one would not make the mistake of thinking it is a set itself, as it has a non-discrete topology - it even has non-identity specialization morphisms in functions between sets. There are various other universes for various other kinds of spaces, such as the Boolean algebra classifier for Stone spaces. The different universes represent qualitative distinctions, not just one of "size". As you know, I'm trying to do something along those lines but based on arithmetic universes instead of Grothendieck toposes. All the best, Steve.

On 4 Jan 2018, at 11:00, streicher@mathematik.tu-darmstadt.de wrote:

Dear Steve at al.

I think in one or the other form universes are inevitable be they type or set theoretical. Of course, you can do category over fairly general bases like finite limit categories (as Benabou developed some time ago). But then you are bound to work externally since one can speak about a fibration in the internal language of its base in an only very restricted way.

Thomas

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]