Dear Thomas, I did not intend to "generalize" anything, only to restate the definition. There are at least four equivalent definitions of fibration in a 2-category that I know of: - the "representable" one which I gave, - having an adjoint one-sided inverse to a certain morphism between comma objects - being an algebra for a certain monad on a slice 2-category - the one in the Elephant All the definitions have two versions: a "strict" one a la Grothendieck (which only makes sense in a strict 2-category) and a "weak" one a la Street (which makes sense in any bicategory). All the strict notions are equivalent to each other, and all the weak notions are equivalent to each other. The idea of the equivalence of the first three is essentially contained in Richard's remark, while a proof of the equivalence of the Elephant's version with the representable one can be found in Peter Johnstone's article "Fibrations and partial products in a 2-category." Weak fibrations are closed under composition with equivalences, while strict ones are not. In Cat and probably other well-behaved 2-categories, being a weak fibration is the same as being the composite of a strict fibration and an equivalence, and so it ought to surprise no one that in such cases it is sufficient to consider strict fibrations. It's generally only in the bicategorical world that weak fibrations become important. All the definitions can also be described either as "properties" (such-and-such thing exists) or as "structure" (equipped with such-and-such thing), since in all cases the such-and-such is unique up to unique isomorphism when it exists. This is the situation also referred to as "property-like structure." But perhaps you were originally referring instead to the structure required on the 2-category itself? It's true that the latter three definitions require existence of some limits in the 2-category, while the representable version does not. Finally, in Cat with choice, the strict notions are all equivalent to the usual Grothendieck fibrations, while the weak ones are equivalent to Street's. (Street actually originally gave his definition in a general bicategory, and only later specialized it to Cat.) Does this clarify what I meant?
Nothing against anafunctors but it is an exaggeration to say that in absence of choice the usual notion of functor is not well-behaved.
Perhaps "not well-behaved" was a poor choice of words since it implies a value judgement, but I think it is correct to say that in the absence of choice, category theory becomes very unfamiliar unless we replace functors with anafunctors. For instance, if we insist on using only functors, then a category with finite products does not necessarily become a monoidal category, as there is no "product" functor from A×A to A. Also, without choice the 2-category Cat using functors is not even a regular 2-category, let alone a 2-topos. Since the defining characteristics of Set include that it is a well-pointed 1-topos, it seems unlikely to me that one will be able to get much of anywhere with a version of Cat that is not a 2-topos. Mike [For admin and other information see: http://www.mta.ca/~cat-dist/ ]