From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/4047 Path: news.gmane.org!not-for-mail From: JeanBenabou Newsgroups: gmane.science.mathematics.categories Subject: Re: Historical terminology,.. and a few other things. Date: Wed, 31 Oct 2007 23:53:07 +0100 Message-ID: NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 (Apple Message framework v752.2) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241019687 11472 80.91.229.2 (29 Apr 2009 15:41:27 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:41:27 +0000 (UTC) To: Paul B Levy Original-X-From: rrosebru@mta.ca Thu Nov 1 10:42:16 2007 -0300 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Thu, 01 Nov 2007 10:42:16 -0300 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1InaHS-00031w-JU for categories-list@mta.ca; Thu, 01 Nov 2007 10:40:18 -0300 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 106 Original-Lines: 87 Xref: news.gmane.org gmane.science.mathematics.categories:4047 Archived-At: 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 >