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