Dear Michael,
Does this clarify what I meant?
Yes, indeed that has been very helpful.
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.
Well, but then we can work with categories with a chosen structure, e.g. chosen products; that's what is recommended in the Elephant and it looks to me as close to practice; it's very unlikely to have a nonconstructive proof of existence of products. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]