* Historical terminology,.. and a few other things.
@ 2007-10-30 9:02 JeanBenabou
0 siblings, 0 replies; 2+ messages in thread
From: JeanBenabou @ 2007-10-30 9:02 UTC (permalink / raw)
To: Categories
Historical terminology,.. and a few other things.
0. Prologue
0.1. I want to thank all the colleagues who answered my questions on
"historical terminology". I shall try to answer all of them, and
shall greatly appreciate any remarks or comments about the present mail
0.2. I type very slowly, all the more so because I decided to
respect the constraints of "Outypo" in this mail.(See the appendix
for the meaning of this word). These constraints explain the unusual
presentation of this text
0.3. I shall abbreviate by (c), (cc),(lcc) and (lcct) the
following properties of categories: "cartesian", "cartesian closed",
"locally cartesian closed" , and "locally cartesian closed with a
terminal object".
0.4. I shall denote by El the book of P. Johnstone: Sketches of an
Elephant, Vol.1 and, and for references I shall use the monumental
bibliography of El in the following manner:
(i) If the reference is there, I use El then the number, in bold
face between brackets, e.g.(El 911) means :
S.C. Nistor and I. Tofan, On the category ab(E) (Romanian),
Bul.Inst.Politechn. Iasi (I) (1985) 205-207 ; MR 87g:18001
(ii) If the reference is not there, I shall write the symbol (El ?)
followed by the minimum information permitting to localize it, e.g.
(El ?) P.J. Cohen, Set theory an the Continuum Hypothesis
0.5. The notations shall be either standard or self explanatory with
the following exception: I shall abbreviate "x is an element of y" by
"x@y". For example in the following definition:
A category X is lcc if it satisfies: forall x (x@Ob(X) => X/x is cc)
0.6. A first draft had convinced me that my mail would be abnormally
long, so I have decided to break it in two parts. The first, almost
totally devoted to (lcc), already very long, which I send
immediately. I shall then wait a few days for the second part,
devoted to (c) and (cc). This will permit me to receive any remarks
or comments you would want to make about this first part, and to
answer them as well as I can in the second part.
I hope I won't be too boring, and apologize in advance if I am
1. Locally cartesian closed categories (lcc)
From Prof. Peter Johnstone's answer to the question: Why did he
impose a terminal object in his definition of lcc, I quote:
"I did that because it seemed the appropriate convention to adopt in the
context of topos theory. I wasn't trying to dictate to the rest of the
world what the convention should be. On the other hand, there seem to
be remarkably few `naturally occurring' examples of locally cartesian
closed categories which lack terminal objects: the category of spaces
(or locales) and local homeomorphisms is almost the only one I can
think of."
Since "he can think" only of very few or almost only one "naturally
occurring" lcc's which lack terminal objects, let me provide "a lot"
more ones.
1.1 First examples of categories which are l.c.c but have no
terminal object
(i) The smallest "I can think of" namely O, the empty category.
(ii) A little bit bigger, but not too big: 1+1, the discrete category
with two objects.
(iii) Any discrete category ( except 1 of course)
(iv) Any group (again except 1).
(v) Any groupoïd (non trivial, i.e. non equivalent to 1).
The reason for (v) is the following characterization of groupoids,
which does not seem to have found its way in standard texts on
category theory:
A category X is a groupoid iff all its slices are equivalent to 1
Moreover, if X is a groupoid, the following are equivalent :
(a) X has a terminal object
(b) X is non empty and has binary products
(c) X is equivalent to 1
Since (i), to (v) are groupoids, I shall count the whole previous
list as one single type of example, and give others which don't fit
in this pattern.
(vi) The ordered set Omega of natural numbers.
(viI) More generally any limit ordinal .
(viii) The ordered category On of all ordinals.
(ix) Any coproduct of l.c.c. (Even if they all have terminal objects,
provided there is more than one such category)
(x) Any rooted tree, with the canonical ordering obtained by taking
the root as smallest element. In particular the binary tree. And of
course, by (ix) any "planted forest", i.e. coproduct of rooted trees.
(xi) the ordered set R_+ of non negative real numbers.
(xii) A little bit bigger than Omega, but still countable namely: the
category with objects the finite cardinals and maps the injections.
(xiii) The following one might be "handy" for logical purposes:
If C is a topos, the category Mono(C) having the same objects, and
as maps the monos of C is lcc without terminal object.
Question: Which, among the previous list, is so "unnaturally"
occurring" that it should be "banned" from category theory? And
moreover at the cost of a "linguistic violation" of the commonly
adopted meaning of "local"?
1.2. First "stability" results
The following theorems "explain" and generalize many of the previous
examples, and permit to construct many more important lcc's without
terminal objects.
1.2.1 Theorem If C is a lcc category, so is Mono(C).
1.2.2 Theorem Let P: D-->C be a discrete fibration, if C is l.c.c.
so is D
1.2.3 Corollary Let C be a category and D be a sieve of C. If
C is lcc so is D.
I shall leave to your "fertile brains" (Preface of El , p.viii) the
pleasure to use 1.2.1 and 1.2.2 to construct lcc's without terminal
objects, and I shall use only the much weaker 1.2.3 to give more
examples. They all fit in the following general pattern: Start with a
C which is lcc, and may or may not have a terminal object. Suppose is
is equipped with a notion of "boundedness",and take for D the sieve
of bounded objects. Here are a few important examples:
(xiv) Take for C an elementary topos, and call an object of C
bounded if it is contained in a (Kuratowski)-finite object.
(xv) Let A be any small category. Take for C the category A^ of
presheaves over A and call a presheaf bounded if it is contained in a
representable one.
(xvi) Let X be a metric space. Take C=Opn(X) , the locale of its open
subsets, and call an open set U bounded if it is contained in a sphere.
(xvii) Let X be a topological space, and again C=Opn(X), and call U
bounded if it is contained in a compact.
(xviii) one can "sheafify" (xvi) and get the lcc of sheaves with
compact support.
How many more examples does one need?
Let me mention that the direct "proof" of 1.2.3 is so simple you
could cry: If D is a sieve of C, all its slices are slices of C, thus
any local property, not only lcc, satisfied by C will be shared by D.
But, even if C has a terminal object, D does not need to have one.
1.2.4 Remarks "en vrac"
1- Even if we assume in the previous results that C has a terminal
object, neither Mono(C) nor D need have one. Thus (lcc) has many more
"stability properties" than (lcct). See also 1.1 (ix)
2- It is even possible to have an lcc category , with binary
products but no terminal object. This is the case in the examples
(xv), (xvi) and (xvii) if the whole space X is not
"bounded" (partial answer to Dubuc)
3- There even exits an lcc which has binary products and is not
connected, namely 0 . (Dubuc again)
4 - There are much stronger " stability results" than the previous
ones permitting to construct lcc's but it would take too much space
to build the the "set up" where they can all be stated, let alone
proved. I shall say a few words about parts of this set up in the
next section, and show how it can be used for "general" local
properties, not just lcc.
Question: What important theorems hold for (lcct), but not for (lcc)?
If you ask the question in the other direction my answer is easy: All
the stability theorems I mentioned
Remark: In the theory of fibered categories we work with fibers and
slices and the introduction of unneeded terminal objects weakens the
results or confuses some issues, and sometimes does even both.
1.2.5 Terminology again. There is by now an unwritten but (almost)
unanimous "linguistic consensus" on the following terminology: If P
is a "property" of categories, a category satisfies P locally iff all
its slices satisfy P.
I do not want to "dictate" anything to anybody, but I think we could
all easily agree on this "unifying" terminology and, if for some
mathematically imperative reason, we need a different notion, we
should use our imagination to give it another name.
There is already an unfortunate exception, namely: locally small
categories, which I never liked, (I would have preferred something
like: piecewise small). But "locally small" has been used by
countless mathematicians in countless texts, and in such a case I am
not very prone to change the terminology, even if I don't like it.
2 . Local properties of functors
We extend the previous definitions to properties of functors in the
following manner.
2.1 Basic definitions
2.1.1. If F: X-->Y is a functor, and x is an object of X, the
slice of F at x is the obvious functor F/x: X/x-->Y/Fx induced by F
We remark that, for G: Y-->Z , we have: (GF)/x = (G/F(x))(F/x) .
2.1.2. A property (of functors) is a class P of functors satisfying:
Every iso F: X-->Y is in P, and P is stable under composition
2.1.3. If P is a property, a functor is locally in P if all its
slices are in P , thus we get a new property called the localized
of P and denoted by L(P)
2.1.4. If P is a property we say that a category X is in P if the
functor X-->1 is . In that case every category isomorphic to X is
also in P.
2.1.5. Properties are ordered by inclusion, we shall write P=>P'
for " P is contained in P' ". This implies L(P)=>L(P')
2.2 Remarks, again "en vrac"
1- One can define more general notions of "localness" than those I
gave in 2.1, but I shall not mention them in this mail
2- From a categorical point of view the definitions I gave are
"natural" . They are also very simple and, because of this
simplicity, one might think that not much can be derived from them.
That it need not be so, comes from the fact that very simple
properties may have much "richer" localizations.
3- Although this may seem "strange", I do not assume that:
if F: X-->Y is in P, and F': X-->Y is isomorphic to F, then F'
is in P,
let alone that every equivalence functor is in P. e.g. P could very
well be the property of functors which are surjective on objects.
.2.3 Local Iso's
I denote by Iso the smallest property: the only functors in it are
iso's, the functors in its localized are thus local iso's. Quite
"surprisingly" we have:
2.3.1 Theorem A functor F: D-->C is a local iso iff it is a
discrete fibration
As a consequence we have following "ubiquity" of discrete fibrations,
if F: D-->C is such a fibration, then for any property P, F is in
L(P). In particular, If C is in L(P) is in L(P) so is D.
Since for any category X the functor 0-->X is a discrete
fibration, it will be be in L(P), and in particular so will be the
initial category 0.
More than 2/3 of the examples of §1 follow from the previous remarks
applied to the very special case of lcc's
2.4 Local surjective equivalences
The smallest property "I can think of", after Iso of course, is SEq ,
surjective equivalences, which I define as:functors which are
full,faithful and surjective on objects. (They are also surjective on
maps). Thus its localization L(SEq) is defined. Even more
"surprisingly", we have:
2.4.1 Theorem Let F: D-->C be a functor. The following are equivalent :
(i) F is locally a surjective equivalence, i.e. F is in L(SEq) .
(ii) Every map of D is F-Cartesian, and F is a fibration.
(iii) F reflects isos and F is a fibration.
(iv) F is a groupoid - fibration (i.e. a fibration where all the
fibers are groupoids.
Almost every property P contains all equivalences, and in particular
the surjective ones.
Thus we get an "almost ubiquity" of groupoid fibrations :For any
such P we have:
(i) Every groupoid fibration F: D-->C is in L(P). In particular:
(ii) If C is in L(P) so is D
(iii) If G is a is a groupoid it is in L(P)
This explains, and considerably generalizes 1.1 (iv), and it might
interest Ronnie Brown.
2.4.2 Remarks
Surjective equivalences are much better than mere equivalences because :
(i) They are stable under pull backs whereas equivalences are not,
and they can even be characterized as the only equivalences stable
under pull-backs.
(ii) They are fibrations and, as fibrations , they have simple
characterizations, namely:
Let F be a fibration:
F is an equivalence <=> each fiber is equivalent to 1 <=> F is in SEq
(iii) They can be internalized in any regular category, and "behave"
there as well as one might want.
(iv) I don't know who observed first that equivalences are not stable
under pull-backs. It is mentioned explicitly in Grothendieck's first
paper on fibrations, together with the fact that, for fibrations,
they are stable:
(El ?) A. Grothendieck , Categories fibrees et descente; SGA 1961
.
(v) Much later, Freyd and Scedrov (loc. cit. 1.361 p.19) have
considered surjective equivalences under the name of inflations, but
they were mainly interested, as most people, in "mere" equivalences
and the inflations served only to decompose equivalence functors.
In particular they never mentioned that inflations were fibrations,
nor that they were stable under pull-backs, both facts which are
important to me.
2.5. The local game
Given time and space,I could have added to 2.3. and 2.4 a very long
list of localized properties, I shall just give an idea of the "local
game" I have been playing, with interruptions,for more than 25 years.
Chose simple properties P and find out what L(P) is. In the other
direction, chose some important (for you at least) property Q and
try to see if it is of the form L(P) for some P . Such a P need not
be unique, so try to find one "as simple as possible".
2.5.1. Example If P is the property of functors which are surjective
on objects and have a right adjoint, we have: A functor is in L(P)
iff it is a fibration.
Thus, if F:X-->Y is a fibration, for every property Q such that
P=>Q , we have:
If G:Y-->Z is in L(Q) so is GF, and in particular, if Y is in L(Q)
so is X.
2.5.2. The "game" can be made more complex, and more difficult, by
imposing further "constraints" (see appendix) of the kind:
For which P's is L(P) stable under pull-backs, or pseudo pull backs,
or has "adapted" calculus of fractions, etc.
Before I got used to the game, I had many "surprises". Each of them
brought a new result or at least a better understanding of old ones.
3. A few comments on the answers I received
3.1 General picture
There seems to be a general agreement in all the mails about the fact
that (lcc) should not include terminal objects, except of course for
Prof. Peter Johnstone, but I have already made long comments about
his mail, and if he is not convinced by my purely mathematical
arguments, I'd greatly appreciate if he could tell me why he isn't.
Of course again: only for mathematical reasons.
The mails which agreed with my definition explained this agreement
by two kind of arguments:
(i) Purely linguistic and coherent use of "local". This includes Fred
Linton, Eduardo Dubuc and Phil Scott's second mail. As I totally
agree with them on this basis I shall make no more comments
(ii) Arguments coming from "logical systems" such as dependent
types, lambda calculus, etc. This includes Phil Scott, Vaughan
Pratt,and Paul Taylor. I must confess i am not convinced by these
types of arguments, and I shall explain why. I expect strong
reactions to some of my statements, and I shall be very happy to to
hear them, and try to answer them.
3.2. First comments
I'm absolutely sure, even if I don't know some of them very well,
that the "logical systems" mentioned in the previous sub-section,
provide very important examples of lcc or lcct categories.
Nevertheless I'm tempted to say So What?
I won't say it because some people might think there are limits to
heresy, but very deep in my mind I'll continue to think it. Why?
3.2.1. Other important examples can arise from different domains of
Category Theory or more generally from mathematics.
I gave a long list in §1 , which I could easily have made much
longer, and even if someone could prove that, say, Omega , R_+ , any
groupoid, sheaves with compact support , could be described in terms
of "dependent types" or "lambda-calculus" I would still not be
convinced!
Because each description would require a different ad-hoc "logical
system", which would certainly appear artificial to the specialists
of the domain, whereas for a categoricist these examples are all easy
and meaningful. In particular I ask the question:
Which of the previous examples has ever appeared in the context of
such logical systems?
3.2.2. I shall go a bit further. Even If someone did come up with a
(meta) theorem of the kind: "Every lcc category can be described as a
suitable model of such a forma system" , (Which is probably true,
and probably easy to prove), even in that case, I would still not be
convinced!
Because: How would one interpret the various stability theorems I
mentioned? For example: Suppose I know that a specific lcc category
C is a model of some formal system (F). By 1.2.1 and the, yet
unproved, meta-theorem I alluded to, I shall know that Mono(C) is a
model of another formal system of the same kind, say (F'). But then
how do I deduce syntactically (F') from (F) ?
I contend that Category Theory by asking such natural questions,
might inspire some interesting formal constructions in various
"logical systems"
3.2.3. Category Theory is "irrigated" by many mathematical fields. An
important one is so called "categorical logic", but it is not the
only important one. And if we are tempted to think that some axioms
we assume on categories make them "the embodiments" of some kind of
logical system, they are almost never only that e.g. :
Think of a topos as "semantics for intuitionistic formal
systems" (El. Preface) what is the "syntactic counterpart" of the
following well known and important result:
If C is an internal category of a topos E, the category E^C is a
topos.
Such a syntactic description could perhaps be given, but at what
cost? And would it clarify or obscure this basic result?
3.2.4. There is yet another question to specialists of "logical
systems" Any category with a terminal object is connected as a
category. lcct categories are connected. Now an elementary topos or a
locale are lcct categories , where there is another important notion
of connectedness, namely 1 is a connected object (I apologize for
such trivialities). Here is the question:
Is there a similar notion of connectedness for the kind of "logical
systems" I mentioned earlier?
3.2.5. Suppose E is an elementary topos.(the assumption is much too
strong, but I make it to be on the safe side) One might want to
define internal categories in E which are lcc. Incidentally I did
it . It was easy. And in order to do it, I didn't have to
"internalize" (whatever that might mean) "Dependent Type Theory", or
any other logical system.
3.3. The main objection
3.3.1 I have given in 3.2. many reasons why arguments coming
exclusively from "categorical logic" did not convince me, but there
is a fundamental one, namely:
Viewing some categories as embodiments of "logical systems", most of
the time does not give any indication about what the morphisms
between such categories ought to be, and sometimes even suggest wrong
directions. When we need these morphims,and in general we do need
them, the ultimate choice comes from mathematics, not logics.
3.3.2. First examples
(i) What is the notion of morphism, if any, suggested by formal
systems such as : "Dependent Type Theory", or "Typed Lambda calculus" ?
(ii) Has anybody defined a notion of morphism between
"Hyperdoctrines", and, if nobody has, why not?
(iii) In §2.5. of their very nice book (El 381) Freyd and Scedrov
define the notion of congruence on an Allegory. This a natural
definition of "syntactic type". But very quickly
they restrict their attention to "amenable congruences" which are no
longer "syntactic". This is a typical illustration of the fact that
"ultimately, the choice comes from mathematics". (I shall come back
to this notion of congruence in the second mail)
3.3.3. A morphism of toposes is ...?
In the preface of El one can find a very illuminating list of
"descriptions" beginning by "A topos is.." and numbered from (i) to
(xiii). I shall use the same numbering if I want to refer to some of
them. I was very much impressed, especially since it took more than
20 years to complete that list, and the contribution of, I quote:
"the category-theory community", and, "the theoretical computer
scientists" .
Since there was not a single description of geometric morphisms, I
studied carefully that list, in the light of 3.3.1, to see which of
the 13 descriptions were most suitable to give indications about how
to describe these morphisms. Obviously (v) and (viii) are too
"sophisticated" and require too much preliminary knowledge of Topos
Theory, and many other domains, to serve my purpose, so I dropped
them and concentrated on the 11 remaining descriptions.
And there, I had a big "surprise" : I am no linguist, and moreover
English is not my mother language, but I remarked that the "A" in "A
topos is" had different meanings, e.g.
1. In (xii) "A topos is" means "some toposes are".
2. In (i), (vi) and (xi) "A topos is" means "every Grothendieck
topos is"
3. In (ii),(iii), (iv),(vii),(ix),(x) and (xiii) "A topos is" means
"every topos is"
I shall not insist on this "logical ambiguity",but obviously, if we
seek a general description of morphisms of toposes, we won't find it
in 1 because only "some" toposes fit in this description.
In the "sublist" 3, (iii), (iv), (vii), and (xiii) come from various
logical systems. I have tried to figure out, thinking only in terms
of such systems, what a morphism should be. I confess I couldn't find
a natural definition of such morphisms between, say: two "..
(embodiments of) an intuitionistic higher-oder theory" , (iii), let
alone between one such embodiment and "..a setting for synthetic
domain theory" (xiii). I'm sure a helpful colleague will supply a
"bridge" between the two. The best I could do was to "describe", very
vaguely, logical morphisms between two toposes, and only when their
two "descriptions" were given by the same number on the list.
When the "fertile brain" of Grothendieck (El preface, p.viii) gave
the definition of geometric morphism, he knew only (i) in "the
list", because he happened to have invented it. The definition was
given for purely mathematical reasons. And as all very deep
mathematical definitions, it has resisted time. It has even
anticipated time, because it is suitable for elementary toposes which
didn't even exist when he gave his definition!
There is much more one can say about based toposes than about "mere"
toposes, and I'd be curious to know how specialists of "logical
systems" or "computer scientists" would have, even in a "descriptive"
manner, answered the question: A based topos is ... ?
I have some comments, questions, and even a few answers, about "La
Lista", which is supposedly the fruit of: the category-theory
community and the theoretical computer scientists. But I shall
postpone them until "better times"
3.3.4. Logical categories and categorical logic
I think that the scope of "categorical logic" should be much wider
than the mere study of the categories which "embody logical systems",
which I propose to call by the "generic" name of logical categories.
(But of course I would never dream of trying "to dictate" anything
to anybody, let alone to "the rest of the world")
It could include in particular:
(i) the study of "local properties" , a "flavor" of which has ben
given in §2,
(ii) Calculus of fractions, adapted to various "properties" of
categories and functors , a first part of which, with clear
motivations, can be found my paper (El 103) . But that was in 1989,
almost prehistory. Some of you may have doubts about the relevance of
this calculus of fractions to "categorical logic". In the second
part, if I don't have to answer too many questions or objections
about the present mail, in the same spirit as in §2 I shall give a
few mathematical results to try to convince them
(iii) abstract notions of homotopies in categories but also of
categories, i.e. in Cat, as defined by Grothendieck in his "Pursuing
stacks". A group of mathematicians, mostly French, are developing
his ideas, and for those who might be interested, apart from their
numerous papers, I recommend volumes 301 and 308 of "Asterique" :
G. Maltsinotis, La theorie de l'homotopie de Grothendieck
D.C. Cisinski, Les prefaisceaux comme modeles de l'homotopie
This list is very far from complete, and I'm sure that many of you
have in mind some important parts of category theory which could be
added to it
3.3.5. I have worked, on and off, for more than 20 years, on some
aspects of this "categorical logic". I have talked two or three times
about my ideas and my very very first results, but I met only "polite
but indifferent" reactions. Maybe my work didn't deserve much more.
I don't care. Because, if you allow me to be a bit "personal", this
work has given me a lot of pleasure. In particular because it has
permitted to deepen my relation with old and dear friends such as
fibered categories, cartesian maps and functors, categories of
fractions, etc, and to improve my understanding, and knowledge, of
their "qualities". And, last but not least, to prove new mathematical
results about them.
3.4. The special case of Mr. Paul Taylor
The answer to Paul Taylor deserves a special treatment. Although I
deeply regret it, it will not be only mathematical, but such a choice
was his to begin with. I quote his mail:
"I am sorry to say that I have seen papers emanating from respectable
universities in which the authors have appeared to believe that this
is the definition. (One of the papers that I have in mind cites
many eminent categorists, who may perhaps have an opinion about
having their names appear alongside a lot of complete nonsense.)"
3.3.1- Why?
Why such petty and spiteful attacks on unnamed mathematicians,
without any proof or justification, in a purely "historical", non
polemic discussion? (c.f. The answers of all the other participants)
Why didn't anybody react to such attacks, or to previous ones, by the
same "Mr" Taylor? Does he enjoy some "special status", or shall we
have to consider in the future such behaviors as "normal"?
I quote him again:
"My footnote refers to "other authors" who said that LCCCs should
have binary products; I think I may have had Thomas Streicher in
mind, but I don't recall what he may have said or in what paper."
3.3.2- Streicher &... others?
Why mention Thomas Streicher without at least trying to find out what
he said or wrote precisely on the question?
Why not mention P. Johnstone's "Elephant" where this is precisely
written, long after Taylor's world famous "footnote" was published.
Lack of courage? Fear for future promotions?
Why not mention two other " eminent categorists" who made the same
mistake in a published paper that he certainly knew, namely Phil
Scott and...Paul taylor himself who wrote in their joint paper (El.
977) at the very first page in the fist proposition:
"Let C be a locally cartesian closed category( that is, C has finite
limits and for each object X in C, the slice category category C/X is
cartesian closed)..."
Lack of memory? Lack, again, of elementary courage or decency to
"confess past errors"?
When was Mr. Taylor "struck by the light" ?
When did he abandon the finite limits before writing "his footnote",
and as all new zealots, started condemning very strongly his former
"sinning colleagues"? Except the powerful ones, of course!
3.3.3- "Consensus"?
I quote him again:
"I confess that I'm a bit surprised to find that the consensus agrees
with me, so to set matters straight I should also point out that my
argument applies equally to elementary toposes and other familiar
structures of categorical logic."
I am greatly honored to find that I agree with Mr. Paul Taylor's
footnote in "his book", which I have not read, and have no intention
to read, about matters I had completely settled more than 20 years
before "the" book was published !
Mr. Taylor was answering me. Thus I very gratefully thank him for
teaching me a few things that presumably I didn't know such as:
"The simplest formulation is that an LCCC is a category every slice of
which is a CCC. In particular, every slice has binary products,
which are pullbacks in the whole category."
"Objects of an LCCC and the slices that they define correspond to
objects of a base category and the fibres over them in a fibred or
indexed formulation of logic,"
I certainly do agree, except on a "minor detail": I do not like the
idea that my name could be in any manner whatsoever associated with
"indexed categories". I never used the term, I said and wrote
countless times that I considered the notion as wrong. Maybe I am
wrong, the future will decide. But I want no part of responsibility
in the propagation of this notion. This is my choice as a
mathematician. Incidentally, I am in very good company, most
mathematicians, some of them outstanding use fibrations. Of course, I
am quite ready, if I am asked, to give,once again, purely
mathematical reasons for this choice. But I'm afraid it will, again,
be in vain, because : "Il n'est pire sourd que qui ne veut entendre".
4. Appendix: Outypo
(for my friend Jacques Roubaud, a poet, a mathematician and an
innocent victim)
4.1 Many of you have probably heard of "Oulipo", Ouvroir de
Literature Potentielle, a literary group created in 1960 by Raymond
Queneau and Francois Le Lionnais. It proposed to create literary
texts submitted to well chosen but otherwise arbitrary
"constraints" , of various nature: linguistic, syntactic,
combinatorial, and even topological. (One of the best known examples
is due to Georges Perec who managed to write a whole,and good, novel
without ever using the letter "e" which is by far the most frequently
used in French).
Jacques Roubaud, a member since 1966, has invented dozens of such
constraints, some of them quite sophisticated, using e.g non trivial
groups of permutations or topology "a la" Moebius strip or Klein
bottle. He is world wide known as the author of more than a dozen
novels, many thousands poems, and one of the best specialists of the
sonnet.
(For more details, you can consult Wikipedia, about two "items":
Oulipo, and Jacques Roubaud)
4.2. In all my life I have written only three joint papers. The
first was:
( El ? ) J.Benabou, J.Roubaud, Monades et descente
4.3. Oulipo has "swarmed" from literature to many other domains :
painting, music, photography,etc. New groups have been created, all
over the world, in these domains. And, to "remember their
filiation", they have chosen their name according to the following
"constraint " : Ou X po , i.e; three syllables, the first "Ou", the
last "po", the "X" in the central one being an abbreviation of the
name of their domain. e.g. in the domain of painting, "peinture" in
french, there has existed for almost 20 years now "Oupeintpo" as:
Ouvroir de peinture potentielle.
Before formally adopting "Outypo", I have consulted my "expert",
J.Roubaud who confirmed that the name was correctly formed, and that
my constraints were genuinely of "oulipian" nature.
4.4. Easy "oulipian" questions
(i) Complete the reference of our joint paper
(ii) Why, and of whom is Jacques Roubaud a victim?
(iii) What does "Outypo" stand for, and what are its constraints ?
^ permalink raw reply [flat|nested] 2+ messages in thread
* Re: Historical terminology,.. and a few other things.
@ 2007-10-31 22:53 JeanBenabou
0 siblings, 0 replies; 2+ messages in thread
From: JeanBenabou @ 2007-10-31 22:53 UTC (permalink / raw)
To: Paul B Levy
Dear Paul,
There are unfortunately TWO conflicting uses of "locally" in category
theory, which have nothing to do with each other:
One means "slicewise", which I was referring to, and the other means
"homwise", coming from enriched categories. When we say lccc, we
obviously refer to the first one. It was in order not to introduce
further ambiguities in the FIRST notion that I wanted to get a
"consensus" about IT.
As for "indexed" versus "fibered" I have many times mentioned the
PURELY MATHEMATICAL reasons of my preference. Here is a "test" for
you. It is a well known easy and important fact that: the composite
of two fibrations is a fibration.
I am ready to pay two bottles of GOOD champagne to anyone who can
state this result using only indexed categories, and SIX bottles to
anyone who can state, and prove, the same result
>
> Dear Jean,
>
>> 1.2.5 Terminology again. There is by now an unwritten but
>> (almost) =20
>> unanimous "linguistic consensus" on the following terminology: If
>> P =20
>> is a "property" of categories, a category satisfies P locally iff
>> all =20=
>>
>> its slices satisfy P.
>
> Unfortunately, I was given to understand that there was a different
> consensus: that "locally P" means the homsets satisfy P.
>
> So "locally small" means "with small homsets". and "locally
> ordered" means "Poset-enriched".
>
> I have also heard it said that "V-enriched" was once upon a time
> called "locally V-internal".
>
> For several years I have been writing "locally C-indexed" to mean
> "enriched in [C^op,Set]". Equivalently, a locally C-indexed
> category D is a strictly C-indexed category where all the fibres
> have the same objects ob D, and all the reindexing functors are
> identity-on-objects.
>
> Given that you dislike indexed categories for some reason that you
> do not specify (is it only *strict* indexed categories that you
> object to?) this usage will probably horrify you...
>
>
>> I quote him again:
>>
>> "My footnote refers to "other authors" who said that LCCCs should =20
>> have binary products; I think I may have had Thomas Streicher in =20
>> mind, but I don't recall what he may have said or in what paper."
>>
>> 3.3.2- Streicher &... others?
>> Why mention Thomas Streicher without at least trying to find out
>> what =20=
>>
>> he said or wrote precisely on the question?
>> Why not mention P. Johnstone's "Elephant" where this is precisely
>> =20
>> written, long after Taylor's world famous "footnote" was
>> published. =20
>> Lack of courage? Fear for future promotions?
>
> That's unlikely. Paul Taylor generally says what he thinks to
> everyone. I imagine that, when he wrote the footnote, he'd just
> read some paper of Thomas Streicher that irked him for some reason.
>
> BTW, contrary to some of your correspondents, I would argue that
> modelling dependent type theory requires a lccct (with extensive
> coproducts) rather than a lccc. That is because the contexts of
> the type theory are introduced by two rules: empty context and
> context extension. If you don't have a terminal object to model
> the empty context, surely you don't have a model of dependent type
> theory.
>
> regards
> Paul
>
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2007-10-31 22:53 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2007-10-30 9:02 Historical terminology,.. and a few other things JeanBenabou
2007-10-31 22:53 JeanBenabou
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).