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/ ]