I cannot work out whether the message that Bill Lawvere originally sent in HTML was turned into plain text by him or by Bob Rosebrugh. Either way, I take exception to having the quotation of my message reduced in a way that suggests that I believe that the statements
(1) a topos is a cartesian closed category with (2) an internal Heyting algebra Omega,
are sufficient to characterise a topos. My objective was to move the discussion ON from quoting 1970s lemmas. If someone has indeed programmed these lemmas in Maple then it would be interesting to hear about that. (Maybe David Rydeheard's work on "electronic category theory" counts.) Otherwise "lemma" remains the appropriate word for them, not "algorithm". By the way, I consider it no disgrace to call something a lemma: see page 192 of my book. The point of the characterisation that I gave for a topos is that the difference between set theory (= a topos) on the one hand and topology and computation on the other is that quantification over arbitrary sets is allowed, but only over compact or overt spaces. This restriction brings us a little closer to what most people would call an algorithm. Paul Taylor [For admin and other information see: http://www.mta.ca/~cat-dist/ ]