RE: Subobject Classifier Algorithm

["Paul Taylor" <pt11@PaulTaylor.EU>]

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