An account of "functors defined up to isomorphism" of the kind that David Benson suggested was given by Michael Makkai in "Avoiding the axiom of choice in category theory", JPAA 108 (1996) 109--73, under the name "anafunctors". This theory is one to which the quotation attributed to Voltaire is applicable: I disapprove of what Makkai says, but would defend to the death his right to say it (or at least give him a pat on the back for having the stamina to work it out). One reason for disapproval is being accused of using Choice. For definiteness, suppose that the functors that interest us are product and function-space, and that the objects of our category are topological spaces. Then if I say that a certain category of spaces is cartesian closed, I am allegedly invoking Choice to make a once-and-for-all assignment of the manner of construction of the products and function-spaces of all pairs of spaces. Whilst it is correct to observe that these constructions are defined (by their universal properties) only up to unique isomorphism, the same observation needs to be taken a step further: the category of spaces is only defined up to equivalence, and therefore we may freely replace the God- or ZF-given category by one that is more convenient for us! The root of the dispute between those that consider (objects and) functors to be defined "on the nose" or only up to isomorphism is the cultural dichotomy between syntax (computer science) and semantics (mathematics). Having recognised that dichotomy, we can bridge it. Much as mathematicians enjoy the conceit that they're manipulating genuine (often infinite) objects, in reality ALL that we can ever do is to push around symbols. In particular, when I write XxY or X->Y, that is ALL that I do: I don't treat God as an odd-job man and make Him shift uncountable tangles of curly brackets and Choose things for me! More prosaically, the given category of spaces provides the base types and constant terms in a calculus, and each expression XxY or X->Y is just that - an expression in the calculus. These type- and term- expressions are the objects and morphisms of another category, which is equivalent to the original one, but has the useful property of carrying an assignment of products and function-spaces. In fact, there is a functor from the original "semantic" category to the new "syntactic" one that (under suitable conditions) is full, faithful and essentially surjective, ie a weak equivalence. It has a pseudo-inverse (making it a strong equivalence) iff the original category has an assignment of products and function-spaces: this is where the Choice comes in - or may be avoided. The construction of syntax from semantics is written up in Section 7.6 of my book, "Practical Foundations of Mathematics" (CUP, 1999) http://www.dcs.qmul.ac.uk/~pt/Practical_Foundations/html/s76.html where the word "canonical" is adopted from sheaf theory, and there is an example of a situation where proving naturality of a certain family of maps is the crux of an argument. Paul Taylor (no academic affiliation). 11-Feb-2002 17:32:23 -0400,9780;000000000000-00000000