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

[JeanBenabou <jean.benabou@wanadoo.fr>]

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
>