Dear Steve, When an elementary (base) topos S is specified, I use "S-bounded topos" to mean the pair (E, e), with E an elementary topos and e: E--> S a (bounded) geometric morphism. When S = Set (a model of ZFC) and E an arbitrary elementary topos, then there is a most one geometric morphism e:E---> Set, so in that case the latter need not be specified. I therefore use "E is a Grothendieck topos" to mean "E is an elementary topos bounded over Sets". The latter has been shown to be equivalent to what Grothendieck meant by it. Best regards, Marta ************************************************ Marta Bunge Professor Emerita Dept of Mathematics and Statistics McGill University Montreal, QC, Canada H3A 2K6 Home: (514) 935-3618 marta.bunge@mcgill.ca http://www.math.mcgill.ca/people/bunge ************************************************ ________________________________ From: Steve Vickers <s.j.vickers@cs.bham.ac.uk> Sent: October 27, 2016 7:07:52 AM To: Categories Subject: categories: Grothendieck toposes For some years now, I have been using the phrase "Grothendieck topos" - category of sheaves over a site - to allow the site to be in an arbitrary base elementary topos S (often assumed to have nno). Hence "Grothendieck topos" means "bounded S-topos". The whole study of Grothendieck toposes, as of geometric logic, is parametrized by choice of S. That's presumably not how Grothendieck understood it, and I know some of his results assumed S = Set, some classical category of sets. Moreover, the Elephant defines "Grothendieck topos" that way. On the other hand, if a topos is a generalized space, with a classifying topos being the space of models of a geometric theory, then that surely meant Grothendieck topos; and there are various reasons for wanting to vary S. For example, using Sh(X) as S gives us a generalized topology of bundles, fibrewise over X. I'm coming to suspect my usage may confuse. How do people actually understand the phase "Grothendieck topos"? Do they hear potential for varying an implicit base S, or do they hear a firm implication that S is classical? Steve Vickers. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]