Re: Historical terminology,.. and a few other things.

Re: Historical terminology,.. and a few other things.

[JeanBenabou]

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
>

Historical terminology,.. and a few other things.

[JeanBenabou]

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 ?