From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6176 Path: news.gmane.org!not-for-mail From: Peter LeFanu Lumsdaine Newsgroups: gmane.science.mathematics.categories Subject: Re: are fibrations evil? Date: Wed, 15 Sep 2010 22:14:52 -0300 Message-ID: References: Reply-To: Peter LeFanu Lumsdaine NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 (Apple Message framework v1081) Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1284688809 16376 80.91.229.12 (17 Sep 2010 02:00:09 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Fri, 17 Sep 2010 02:00:09 +0000 (UTC) To: categories list Original-X-From: majordomo@mlist.mta.ca Fri Sep 17 04:00:08 2010 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpx.mta.ca ([138.73.1.138]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1OwQFD-0001jp-O9 for gsmc-categories@m.gmane.org; Fri, 17 Sep 2010 04:00:08 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:58646) by smtpx.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1OwQDl-0001w6-OB; Thu, 16 Sep 2010 22:58:37 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1OwQDh-0002aU-Rs for categories-list@mlist.mta.ca; Thu, 16 Sep 2010 22:58:34 -0300 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6176 Archived-At: On 15 Sep 2010, at 08:43, 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 >=20 > if u : J -> I is a map in BB and PX =3D I then there exists a = morphism > \phi : Y -> X with P\phi =3D u and \phi cartesian, i.e. ... >=20 > I don't see how to avoid reference to equality of objects in this = formulation. If one tries to define fibrationhood as a property of functors, "P : XX = --> BB is a fibration", then indeed talking about equality of objects = seems unavoidable. The problem is exactly turning the object part F : = ob XX ---> ob BB into a function ob BB ---> Sets. But if instead we define a set of "fibrations over BB", then we can do = it: a fibration over BB is a function ob BB ---> Sets, together with etc. = etc. (I gave more details in a post on June 2, answering a similar = question.) Now, in classical foundations, this is (1-)equivalent to the usual = definition. Within a dependent type theory foundation, they are only = rather more weakly equivalent; and in that case I'd hazard that = something along these lines is a more natural/fruitful definition. Digressing a little further, a similar situation arises for many other = classes of maps that are viewed as "fibrations" or some sort: in a = dependently-typed foundation, it's often more natural to consider a type = of "fibrations over B", which then have "total spaces" that are maps = into B, rather than defining "f is a fibration" as a property of maps. = The most fundamental case is just in Sets, with (classically) "all maps = are fibrations": in a dependent system, a "fibration over B" is a = function B --> Sets, which may not be quite the same as a map E --> B. -p.= [For admin and other information see: http://www.mta.ca/~cat-dist/ ]