--- Jeff Egger <jeffegger@yahoo.ca> wrote:
Date: Thu, 30 Aug 2007 13:48:36 -0400 (EDT) From: Jeff Egger <jeffegger@yahoo.ca> Subject: Re: categories: Teaching Category Theory To: Tom Leinster <t.leinster@maths.gla.ac.uk>
Dear Tom,
I find that the set/class distinction is much less compelling than the type/collection distinction, so my initial reaction is that one should develop a kind of "naive type theory" to replace "naive set theory" ---but I don't know to what extent it is possible to do this in a pedagogically sound fashion.
[Googling "naive type theory" yields some interesting-looking articles, but I haven't really had time to look at any of them in anything approaching a serious fashion.]
The central tenet of NTT should be the intuition that one can't compare apples and oranges. In particular, you can't ask whether two things are equal unless they were already "of the same type", which is to say that they were chosen from the same set to begin with.
[Interestingly, there exist better motivating examples than "apples and oranges". Does the speed of light equal the charge of a positron, for example? Of course one could say that the answer is yes if we measure the speeds in light-seconds per second and charges in elementary charges, or we could say that the answer is no if we use more conventional units such as km/h and coulombs. But if we try to conceptualise physical quantities as real entities independent of a choice of unit of measurement, then we recognise the question itself as flawed.]
Of course, elementhood should also not be a global predicate, for otherwise we could subvert the non-existence of a global equality predicate by asserting two things to be equal if they are equal in every type to which they both belong.
The non-existence of a global elementhood predicate renders the extensionality axiom of conventional set theory meaningless. This, in turn, calls into question whether equality of types is a meaningful predicate. But the existence of a type of types would entail the existence of such a predicate, and thus we are led to a situation where the non-existence of a type of all types can be regarded as a feature, not as a bug.
You see what I really have in mind is not so much topos theory (which you might have suspected at first), but FOLDS. [But NTT should be set up in such a way that elementary topos theory becomes a (or even, the) natural result of attempting to formalise one's naive intuitions about types. For example, one can talk about (product- and power-)type constructors in a naive way...I think. Ideally, I would hope that naturality could be adequately described in terms of polymorphic lambda-calculus---but even I wouldn't suggest springing that on an unsuspecting first-term graduate student.]
Here is another helpful intuition for students: a set/class/type/ collection should not be thought of as a "glass box", but rather as a black box with a button: when you push the button it gives you, not an element of the set, but a little receipt bearing the name of an element of the set. [Riders of the Montreal metro system may recognise the boxes from which one obtains bus transfers, which held a strange fascination over me when I was a child.] For arbitrary collections, it is possible that an element have more than one name---and hence, when you ask for two elements, you may in fact receive two names of the same element, _and_ be left none the wiser for it. A type is (naively) a collection for which every element has a unique name.
Now using NTT/FOLDS as a basis for category theory does restrict one to dealing with locally small categories (if, one regards types as necessarily "smaller" than arbitrary collections---which is not as easily justifiable as it might seem), but I would argue that's not such a great loss. [In my experience, non-category-theorists, when asked to provide a definition of category, almost uniformly supply (what amounts to) the definition of an enriched category, in the case V=Set---which I find quite intriguing.] It also destroys the notion of skeletal category, which is probably a good thing too.
I hope this helps---I was originally planning to write a lot more (and might still do so).
Cheers, Jeff.