Re: Teaching Category Theory

[Jeff Egger <jeffegger@yahoo.ca>]

--- 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.
> 
> 
>