Re: Not invariant but good

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

Dear Mike,

> I'm not sure what you mean here.  The notion of fibration in a
> 2-category can be defined as a property if you like: a morphism E -->
> B in a 2-category K is a fibration if all the induced functors K(X,E)
> --> K(X,B) are fibrations and all commutative squares induced by
> morphisms X --> X' are morphisms of fibrations (preserve cartesian
> arrows).  This is equivalent to giving some structure on E --> B, but
> that structure is unique up to unique isomorphism when it exists.

The definition you give entails that a "generalised" fibration is actually
a Grothendieck fibration (since Cat(1,E) is isomorphic to E). This way you
don't get closure under precomposition by equivalences. I also don't see why
cartesiannness of the functors induced by X --> X' should amount to a choice
of structure (cartesiannness of a functor is a property and not additional
structure). Moreover, this requirement is a property of Grothendieck fibrations
which can be established when having strong choice available.

I was rather alluding to the notion of fibration in 2-cats as can be found
in part B of the Elephant where a fibration is defined as a 1-arrow together
with additional structure.

The definition you gave above (which is not more general) is the obvious thing
to do in case K is not wellpointed enough (as Cat is).

Moreover, your definition of fibration in a 2-category is based on Grothendieck
fibrations and thus employs equality of 1-cells. Since 1-cells are objects of
a category it should be "evil" to speak about their equality. Not that it were
a problem to me...

Thomas

PS  Your definition of fibration in a 2-cat looks much simpler than what I
could find in the papers by Street and Johnstone. That's nothing to complain
about but where is it from? It seems to me the appropriate one when generalising
from Cat to more general 2-cats.


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