From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2982 Path: news.gmane.org!not-for-mail From: Paul Taylor Newsgroups: gmane.science.mathematics.categories Subject: prone and supine Date: Wed, 04 Jan 2006 19:09:12 +0000 Message-ID: NNTP-Posting-Host: main.gmane.org X-Trace: ger.gmane.org 1241019020 6738 80.91.229.2 (29 Apr 2009 15:30:20 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:30:20 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Wed Jan 4 20:04:51 2006 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 04 Jan 2006 20:04:51 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.52) id 1EuIbw-0004Ak-LV for categories-list@mta.ca; Wed, 04 Jan 2006 20:04:08 -0400 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 8 Original-Lines: 140 Xref: news.gmane.org gmane.science.mathematics.categories:2982 Archived-At: Several people have asked me to explain why I brought category theory into disrepute by introducing the words "prone" and "supine" 480 pages into my book. It's easy to understand why retired people of any generation would want to carve their works in tablets of stone. It's equally clear that they must never be allowed to do so - "Argument by Authority" is a principle of Theology, not of Science. It isn't even a principle of mathematical history: for example, I recently learned from Renato Betti's biography of Lobacevskij that early 19th century series didn't "converge" but "annihilated". As for Jean Benabou, I would pay more attention to his views on fibred category theory if he HAD carved them on tablets of stone (or preferably paper). Or if he paid more professional respect to those (Peter Johnstone, Thomas Streicher and several others) who, in the absence of the book that he promised 30 years ago, have reported and developed the subject in the meantime. Terminology, notation and proofs (should) evolve. Of notation, Riemann said that when you have the right one, you're half way to solving the problem, whilst Eilenberg taught us how category theory eliminates subscripts. It's sad how often new textbooks copy out old and clumsy proofs parrot-fashion - this is why I'm not enthusiastic about mechanising them. Given that category theory unifies older disciplines, it necessarily selects amongst conflicting terminologies - or completely replaces them, with frivolous words like "pushout". For me there are three guiding principles for choosing names for ideas: (1) certain words and qualifiers (such as regular, normal, semi, weak, quasi-, pre-) are already worn out though over-use, and should not be used again; (2) mathematics needs to make more imaginative use of human language; and (3) an ordinary dictionary should, wherever possible, be able to point the student in vaguely the right direction, especially in complicated abstract subjects like fibred category theory. The word "cartesian" fails every one of these principles. Rule (3) is my mitigation for two other offences that I committed in my book, replacing "indiscrete" with "indiscriminate" and "proof irrelevant" with "proof anonymous". Eduardo Dubuc put my rule (2) very nicely: > "strange," "charm," "beauty" and even "quark" itself are beautiful > and poetic names to refer to objects or concepts which precisely we > do not want to associate any precise meaning in everyday language, > and on the other hand, the objects or concepts are introduced with > those names. However, he didn't consider that "prone/supine" fall under it, because they "reflect in everyday language just one aspect of an existing concept". Presumably he has the geometrical aspect of these words in mind. But it was not me who introduced the vertical/horizontal idea into fibred categories: these words are in Benabou's lengthy posting. (I'm not impressed by Benabou's distinction between "cartesian" and "horizontal". As he notes, it does not apply to the subject in question, namely FIBRATIONS of categories. If he had ever written his textbook on the subject, he would have realised that this is just the kind of footnote that prevents students from grasping the key ideas.) "Vertical" and "horizontal" would be fine, apart from the fact that the fibrations that we find in categorical type theory, modules over rings and other subjects are also op-fibrations. This means that there are two different kinds of horizontality. But we are lucky: in the English language there happen to exist two different words for "horizontal". Even more luckily, they happen to be related by rotation from the vertical in exactly the right way, as Peter Johnstone noted very concisely four weeks ago. Nikita Danilov says that we should choose our vocabulary from Latin, so (applying rule (3)) let's look these words up in Cassell's (1959) Dictionary: > pronus, -a, -um: inclined forward, stooping forward. > ... Transferred meaning: ... well disposed, favourable > supinus, -a, -um (from "sub", cf Greek hyptios): > lying on the back, face upwards. > ... Transferred meaning: ... careless, negligent, lazy. As Toby Bartels has pointed out, les memes mots existent aussi en francais, ed anche in italiano, y sin embargo in espanol tambien, pero mi diccionario es pequeno. QED You may be wondering how all this fuss started. Ronnie Brown asked for my comments on a small fragment of the book he's writing about generalisations of the van Kampen theorem. He was using fibrations to construct colimits in the category of groupoids, which I said was a sledgehammer to crack a nut. However, I also told him that he is the best qualified person I could think of to explain how "canonical" isomorphisms conspire to form non-trivial groups, and so why fibred categories are needed in "semantic" subjects in place of indexed ones. In "syntactic" subjects (categorical type theory) there really are canonical isomorphisms, not just arbitrary choices of them, and indexed categories are appropriate. In my opinion, however, both indexed and fibred categories obfuscate categorical logic. I spent ten years scratching my head, trying to work out why people used them. Eventually, I learned something from Bart Jacobs: indexations arise because predicates depend on variables that range over a set, but not vice versa. Hence the way I treated indexed category theory in Section 9.2 of "Practical Foundations". Chapters VIII and IX develop dependent type theory in the way in which I think it should be done, using "display maps" and not fibrations or hyperdoctrines. In particular, - dependent sums, existential quantifiers and colimits are treated using factorisation systems - or almost, since not every map needs to factorise; and - dependent products, universal quantifiers, exponentials and limits are reduced to partial products. I would invite Jean Benabou to read these two chapters of the book that I HAVE written, and only THEN form a judgement on whether I have "made a major contribution to the field of fibred categories". Paul Taylor www.cs.man.ac.uk/~pt/book PS I drafted this text this morning, and had some friendly private discussions about it with Eduardo Dubuc. We agree on many things, but he maintains that established terminology shouldn't be changed. As I have said, I believe terminology does and should evolve. Also, it seems that I misunderstood the second bit that I quoted from him, for which I apologise, but as Bob says, it's time to bring the subject to a close.