Dear All, The distance between the notion of elementary "topos" and the notion of space is particularly striking with Hyland's effective "topos". The effective "topos" is inspired by constructive set theory (Kleene recursive realizability) and it is among the important constructions in the theory of elementary "toposes". But it has no effect on topology! (ask your favorite topologist). We should probably stop saying that the theory of elementary "topos" (generalised) is topology! It appears to be more a branch of higher order logic formulated in the language of category theory. We can hope that the theory of elementary "toposes" will eventually find applications to topology (something recognised by topologist). The fact that a (Grothendieck) topos E over a base (Grothendieck) topos S can be regarded as a (Grothendieck) topos internal to the set theory defined by S could play a role. Homotopy type theory is a new avenue for the applications of higher order logic to topology. But the notion of elementary higher "topos" has not yet been formalised precisely. Best regards, André ________________________________________ From: Eduardo Julio Dubuc [edubuc@dm.uba.ar] Sent: Thursday, November 03, 2016 12:45 AM To: categories@mta.ca Subject: categories: Re: Grothendieck toposes The very notion of Grothendieck topos involves in fact two topos (sheaves over a site on the base). That is, it is a notion of geometric morphism, it does not make sense as a single category. The notion of elementary topos is a completely different notion which involves a single topos, it does perfect sense as a single category. This observation was made to me by Jacques Penon about 36 years ago. I agree with Joyal that the two notions should be kept apart. Not doing so has created a lot of confusion. best e.d. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]