From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/3871 Path: news.gmane.org!not-for-mail From: Jeff Egger Newsgroups: gmane.science.mathematics.categories Subject: Re: Teaching Category Theory Date: Thu, 30 Aug 2007 13:50:38 -0400 (EDT) Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1241019572 10654 80.91.229.2 (29 Apr 2009 15:39:32 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:39:32 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Thu Aug 30 17:00:15 2007 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 30 Aug 2007 17:00:15 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1IQq1m-0005jw-LH for categories-list@mta.ca; Thu, 30 Aug 2007 16:50:06 -0300 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 22 Original-Lines: 93 Xref: news.gmane.org gmane.science.mathematics.categories:3871 Archived-At: --- Jeff Egger wrote: > Date: Thu, 30 Aug 2007 13:48:36 -0400 (EDT) > From: Jeff Egger > Subject: Re: categories: Teaching Category Theory > To: Tom Leinster >=20 > Dear Tom, >=20 > I find that the set/class distinction is much less compelling than the=20 > 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=20 > pedagogically sound fashion. =20 >=20 > [Googling "naive type theory" yields some interesting-looking articles,= =20 > but I haven't really had time to look at any of them in anything > approaching a serious fashion.] >=20 > The central tenet of NTT should be the intuition that one can't compare= =20 > apples and oranges. In particular, you can't ask whether two things=20 > are equal unless they were already "of the same type", which is to=20 > say that they were chosen from the same set to begin with. =20 >=20 > [Interestingly, there exist better motivating examples than "apples=20 > and oranges". Does the speed of light equal the charge of a positron,=20 > for example? Of course one could say that the answer is yes if we=20 > measure the speeds in light-seconds per second and charges in=20 > elementary charges, or we could say that the answer is no if we use=20 > more conventional units such as km/h and coulombs. But if we try to > conceptualise physical quantities as real entities independent of a=20 > choice of unit of measurement, then we recognise the question itself > as flawed.] >=20 > Of course, elementhood should also not be a global predicate, for=20 > otherwise we could subvert the non-existence of a global equality=20 > predicate by asserting two things to be equal if they are equal=20 > in every type to which they both belong. =20 >=20 > The non-existence of a global elementhood predicate renders the=20 > extensionality axiom of conventional set theory meaningless.=20 > This, in turn, calls into question whether equality of types is a=20 > meaningful predicate. But the existence of a type of types would=20 > entail the existence of such a predicate, and thus we are led to=20 > a situation where the non-existence of a type of all types can be=20 > regarded as a feature, not as a bug. =20 >=20 > You see what I really have in mind is not so much topos theory=20 > (which you might have suspected at first), but FOLDS. [But NTT=20 > should be set up in such a way that elementary topos theory=20 > becomes a (or even, the) natural result of attempting to formalise=20 > one's naive intuitions about types. For example, one can talk about=20 > (product- and power-)type constructors in a naive way...I think. =20 > Ideally, I would hope that naturality could be adequately described=20 > in terms of polymorphic lambda-calculus---but even I wouldn't suggest=20 > springing that on an unsuspecting first-term graduate student.] =20 >=20 > Here is another helpful intuition for students: a set/class/type/ > collection should not be thought of as a "glass box", but rather=20 > as a black box with a button: when you push the button it gives=20 > you, not an element of the set, but a little receipt bearing the=20 > name of an element of the set. [Riders of the Montreal metro=20 > system may recognise the boxes from which one obtains bus transfers,=20 > which held a strange fascination over me when I was a child.] > For arbitrary collections, it is possible that an element have more=20 > than one name---and hence, when you ask for two elements, you may=20 > in fact receive two names of the same element, _and_ be left none=20 > the wiser for it. A type is (naively) a collection for which every=20 > element has a unique name. =20 >=20 > Now using NTT/FOLDS as a basis for category theory does restrict one=20 > to dealing with locally small categories (if, one regards types as=20 > necessarily "smaller" than arbitrary collections---which is not as=20 > easily justifiable as it might seem), but I would argue that's not=20 > such a great loss. [In my experience, non-category-theorists, when=20 > asked to provide a definition of category, almost uniformly supply=20 > (what amounts to) the definition of an enriched category, in the case > V=3DSet---which I find quite intriguing.] It also destroys the notion=20 > of skeletal category, which is probably a good thing too. >=20 > I hope this helps---I was originally planning to write a lot more > (and might still do so). >=20 > Cheers, > Jeff. >=20 >=20 >=20