I would tend to assume that a "Grothendieck topos" is one bounded over "Set", whatever the current meaning of "Set" is, and in particular whether or not "Set" is classical. Thus, when working in the internal language of an arbitrary topos S, I would say "Grothendieck topos" to mean what *externally* to S would be called a bounded S-topos. On Fri, Oct 28, 2016 at 12:08 PM, David Yetter <dyetter@ksu.edu> wrote:

I, for one, would assume the same meaning for the phrase "Grothendieck topos" as is used in the Elephant.

David Yetter

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

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

On 2016-11-01 17:16, Joyal wrote:

It is marvelous that the two notions should be so related. But it is be better to keep them appart before uniting them. Otherwise the miracle disappear in confusion.

The "miracle disappears in confusion" is an important observation, as is the need to "keep apart before uniting". Syntax and semantics is like that, or meta and object language. Foundations of mathematics without categorical consideration is basically then over Set, naively speaking. Logic is similar. Fons et origo logic from late 19th century and decades after is confused about being before set theory or after. Topos internalizes logic but is different from the Goguen-Meseguer approach to institutions and entailment systems. The apples and pears of logic should not be seen as a fruit salad. I've sometimes thought (and written some pieces about, e.g. to be found under www.glioc.com) what if G??del's Incompleteness Theorem wasn't a Theorem but a Paradox. After all, G??del basically transforms the Liar Paradox to a Liar Theorem, and logicians at that time (except maybe Hilbert, but he was too old to quarrel) found it to be very smart. However, if we use underlying categories and functors to start from signatures, then create terms, then sentences, then entailments, then models, then proof strategies, and so on, it means we close doors behind us, so that we disable ourselves to mix truth and provability as being "of the same kind or type", which G??del did. Categorically, terms come from monads, because they enable substitution, but sentences just from functors, because otherwise everything is 'term'. The functorial description and generality of entailment and model is of course more tricky, in particular if the underlying category is something more elaborate (like monoidal closed categories) than just Set. In this (heretic?) view, G??del's Theorem/Paradox is actually an example where that miracle appears because of the unintended (?) confusion, so this is why I sometimes think what if it was ween as a Paradox. Best, Patrik [For admin and other information see: http://www.mta.ca/~cat-dist/ ]