Re: are fibrations evil?

[Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com>]

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
> 
>     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.

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