Thomas Streicher wrote at last:
BTW under a regime which identifies equality with being isomorphic (or weakly equivalent) it looks tempting to use functors from B^\op to Cat. These should capture the pseudo-functors since equality and isomorphism are identified. But writing down functoriality in type theory using \Sigma for existence amounts to choosing a lot of not at all canonical "canonical isomorphisms". Actually, one would get something even more general than pseudo-functors because one wouldn't write down the coherence conditions (actually one couldn't even since there is no honest for good equality!).
Yes, you can write the coherence conditions down (although I agree that it would be easy to forget them). What you need is that a functor (pseudofunctor) P: B^\op -> Cat is not just the following data: * for each object x of B, a category P_x, * for each object x, object y, and morphism f: x -> y, a functor P_f: P_x -> P_y, * functoriality structure (and maybe coherence conditions); but in fact the following data: * for each object x of B, a category P_x, * for each object x, object y, and morphism f: x -> y, a functor P_f: P_y -> P_x, * for each object x, object y, and equal morphisms f = g: x -> y, a natural isomorphism P_{f=g}: P_f => P_g, * functoriality structure and coherence conditions. For example, given f: w -> x, g: x -> y, and h: y -> z in B, we want to compare (P_f . P_g) . P_h with P_f . (P_g . P_h). In a "kosher" treatment of category theory, these aren't equal (that would be meaningless), but there is an associator between them. As a coherence condition, we want to demand that this associator is equal (and this does have meaning) to a natural isomorphism built out of the functoriality structure isomorphisms and their inverses. As we do this, we need to compare P_{(f;g);h} and P_{f;(g;h)}. Again, it's not meaningful (much less true) that these are equal, but P_{(f;g);h = f;(g;h)} is a natural isomorphism between them. So we can write down this coherence condition after all. --Toby [For admin and other information see: http://www.mta.ca/~cat-dist/ ]