prone and supine

[Paul Taylor <pt@cs.man.ac.uk>]

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.