Re: are fibrations evil?

[Michael Shulman <shulman@math.uchicago.edu>]

The usual notion of (Grothendieck) fibration is indeed non-kosher, but
there is a variant due to Ross Street which is not.  This variant is
reproduced at

http://ncatlab.org/nlab/show/Grothendieck+fibration#StreetFibration

As remarked there, almost any fibration which arises in practice
indeed satisfies the stronger non-kosher condition, and a functor is a
Street fibration iff it factors as an equivalence of categories
followed by a Grothendieck fibration.  However, when working
internally to a bicategory where the non-kosher version doesn't even
make sense, Street's version is essential.

Regarding groupoids, it's easy to see that every functor between
groupoids is a Street fibration.  Grothendieck fibrations between
groupoids can be identified with "isofibrations," which are the
fibrations in the canonical model structure on Gpd.  It seems to me
that the use of groupoid fibrations in the groupoid model of type
theory is really an artifact of the desire to describe that model
treating Gpd as a 1-category, rather than a 2-category.  If one
defined the identity types and pullbacks using limits in Gpd in the
kosher 2-categorical sense, then it seems to me that one should be
able to define an equivalent model using arbitrary functors between
groupoids to represent the dependent types, rather than merely the
fibrations.

Similarly, in homotopical models of type theory where the dependent
types are represented by the fibrations in some model structure, it
seems that one should equivalently be able to work with the
oo-category presented by that model structure and use arbitrary maps,
but with all the structure defined using kosher oo-categorical limits.
  The non-kosher version using a model structure on a 1-category and
fibrations may certainly be *easier* to describe and work with, and
there is no reason not to do so in practice -- but just as is usually
the case in homotopy theory, it seems to me that one should regard
this as merely a convenient way to "present" the "real" underlying
structure, which is higher-categorical and kosher.

Mike

On Wed, Sep 15, 2010 at 4:43 AM, Thomas Streicher
<streicher@mathematik.tu-darmstadt.de> 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/ ]
>


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]