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