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