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