Dear All,

The difference between a Grothendieck topos and an elementary topos
is like the difference between a "frame"(= a locale) and a Heyting algebra.

A Grothendieck topos should be called a "topos",
whereas an elementary topos could be called a "logical topos".

Best regards,
André

________________________________________
From: Michael Shulman [shulman@sandiego.edu]
Sent: Saturday, October 29, 2016 11:06 PM
To: David Yetter
Cc: categories@mta.ca
Subject: categories: Re: Grothendieck toposes

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