Re: are fibrations evil?

["Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>]

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