Re: Grothendieck toposes

["Joyal, André" <joyal.andre@uqam.ca>]

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