From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6180 Path: news.gmane.org!not-for-mail From: "Prof. Peter Johnstone" Newsgroups: gmane.science.mathematics.categories Subject: Re: are fibrations evil? Date: Thu, 16 Sep 2010 11:00:54 +0100 (BST) Message-ID: References: Reply-To: "Prof. Peter Johnstone" NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Trace: dough.gmane.org 1284689181 17457 80.91.229.12 (17 Sep 2010 02:06:21 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Fri, 17 Sep 2010 02:06:21 +0000 (UTC) Cc: categories@mta.ca To: Thomas Streicher Original-X-From: majordomo@mlist.mta.ca Fri Sep 17 04:06:19 2010 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpy.mta.ca ([138.73.1.139]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1OwQL9-0004Br-Om for gsmc-categories@m.gmane.org; Fri, 17 Sep 2010 04:06:16 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:42663) by smtpy.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1OwQJw-0002ow-3C; Thu, 16 Sep 2010 23:05:00 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1OwQJp-0002jW-Sq for categories-list@mlist.mta.ca; Thu, 16 Sep 2010 23:04:54 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6180 Archived-At: Yes, fibrations in the original sense of Grothendieck are "evil" (sorry, Jean!), as is shown by the fact that an equivalence of categories is not in general a fibration. There is a weaker notion of fibration in which one replaces the equality "P\phi = u" by a (specified) isomorphism PY -> J making the obvious triangle commute. But every fibration in this sense factors as an equivalence followed by a fibration in Grothendieck's sense, so it's not such an important notion. Peter Johnstone On Wed, 15 Sep 2010, Thomas Streicher wrote: > On the occasion of the discussion about "evil" I want to point out an example > where speaking about equality of objects seems to be indispensible. > If P : XX -> BB is a functor and one wants to say that it is a fibration > then one is inclined to formulate this as follows > > if u : J -> I is a map in BB and PX = I then there exists a morphism > \phi : Y -> X with P\phi = u and \phi cartesian, i.e. ... > > I don't see how to avoid reference to equality of objects in this formulation. > > This already happens if XX and BB are groupoids where P : XX -> BB is a > fibration iff for all u : J -> I in BB and PX = I there is a map \phi : Y -> X > with P\phi = u. > > Ironically the category of groupoids and fibrations of groupoids as families > of types was the first example of a model of type theory where equality may > be interpreted as being isomorphic. > > So my conclusion is that equality of objects is sometimes absolutely > necessary. Avoiding reference to equality is also not a question of using > dependent types as some people implicitly seem to say. Even in intensional > type theory there is a notion of equality. But it is sometimes inconvenient > to use. As pointed out by Ahrens one can and should use extensional type theory > whenever convenient. > Intensional type theory allows one to interpret equality as being isomorphic, > a kind of reward for the inconvenience of using intensional identity types. > > Thomas > [For admin and other information see: http://www.mta.ca/~cat-dist/ ]